Re: [CIL users] Simplifying --dosimplify, continued

[Pavel S. <pav...@gm...>]

Thank you for the comments, I'll take them into account and form a new 
patch.

On Friday, October 28, 2011 16:55:56 you wrote:
> Why does --no-convert-field-offsets imply --no-split-structs? 
> Shouldn't the user be to enable them separately?
> 
> > @@ -89,6 +89,12 @@ let simplAddrOf = ref true
> > 
> >   * has been taken somewhere. *)
> >  
> >  let convertDirectCalls = ref true
> > 
> > +(* Whether to convert field offsets to offsets by integer.
> > + * Static source code verifiers do not need such a conversion *)
> > +let convertFieldOffsets = ref true
> > +(* WARN: splitStructs should be set to false, as it won't find
> > the usage of  *) +
> > +
> > 
> >  let onlyVariableBasics = ref false
> >  let noStringConstantsBasics = ref false
> 
> This looks like an explanation, but I'm afraid I don't understand it
> ("the usage of"...  what?).

It turns out that I started to write an explanation, and switched to 
something else forgetting to complete it.  I'll figure it out.

Anyway, splitting structures in function calls isn't very useful for a 
static verification tool that supports C structures, which is the 
"target audience" for this patch.

> > @@ -224,8 +234,13 @@ and simplifyLval
> > 
> >        in
> >        let a' = if !simpleMem then makeBasic setTemp a'
> >        else a' in
> >        Mem (mkCast a' (typeForCast restoff)), restoff
> > 
> > +  | Mem a, off when not !convertFieldOffsets ->
> 
> I'd rather remove the "when" here, since it's the complement of the
> previous case and could confuse exhaustiveness analysis (did not try
> to compile it in fact) --- and maybe put this case before the
> previous one, in fact.

Yeah, you're probably right.

> >    (* We are taking this variable's address; but suppress
> >    simplification if it's a simple function>    
> >     * call in no-convert mode*)
> > 
> > +  | Var v, off when v.vaddrof && (not !convertFieldOffsets) &&
> > (!convertDirectCalls || not (isFunctionType (typeOfLval lv) )) 
> > -> +      (Var v, off)
> 
> The "when" part is very complex, why not make your change an "if" in 
the next case:

Okay, but it may fail to make the code less complex.

> Will try to look at it in more depth next week.  Since your patch is
> not very invasive, I guess the issue is its interaction with other
> simplification steps.

Thanks.

> > 2) could this patch be added to upstream nevertheless?  I think
> > that the benefits to the verification tools, for which the
> > options is useful, are much greater than the very rarely
> > encountered issue with "very volatile" structs with array fields.
> >  Besides, the behavior without this command- line option is
> > retained.
> 
> I do not like the idea of adding bugs on purpose, but I see your
> point.  Need to think a bit more about it.

I do not approach this as "adding a bug on purpose".  Rather, I think 
it's adding a feature that is useful but doesn't work in all cases.  
Moreover, problematic cases may be inserted into the test system as 
"should fail at compilation" tests; does the test system employed 
support that?

-- 
Pavel Shved
website: http://coldattic.info/
e-mail: pav...@gm...