Hi,
On Fri, Oct 28, 2011 at 12:39:41AM +0400, Pavel Shved wrote:
> The patch adds --no-convert-field-offsets option for --dosimplify
> extension. This option makes CIL not convert structure field access "x-
> >p" to, essentially, "(int*)( (int*)x + 8), where "8" (or any other
> similar number) is a machine-dependent offset of a field relative to the
> beginning of the structure. However, other memory access
> simplifications still work.
Looks interesting. A few comments below:
> @@ -722,6 +737,13 @@ let feature : featureDescr =
> ("--no-convert-direct-calls", Arg.Clear convertDirectCalls,
> " do not convert direct function calls to function
> pointer \
> calls if the address of the function was taken");
> + ("--no-convert-field-offsets", Arg.Unit ( fun () ->
> + convertFieldOffsets := false;
> + (* do not split structs in function calls *)
> + splitStructs := false
> + ),
> + " do not convert field offsets to offsets by integer,
> and \
> + do not split structures into fields in function calls");
> ];
> fd_doit = (function f -> iterGlobals f doGlobal);
> fd_post_check = true;
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?).
> @@ -116,6 +122,10 @@ let rec makeThreeAddress
> if not(!simplAddrOf) then e else
> match simplifyLval setTemp lv with
> Mem a, NoOffset -> if !simpleMem then a else AddrOf(Mem a, NoOffset)
> + (* Do not change addrof if we do not convert field offsets *)
> + | Mem a, off when not !convertFieldOffsets -> AddrOf(Mem a, off)
> + (* Do not change addrof if we do not convert field offsets *)
> + | Var v, off when not !convertFieldOffsets -> AddrOf(Var v, off)
> | _ -> (* This is impossible, because we are taking the address
> * of v and simplifyLval should turn it into a Mem, except if the
> * sizeof has failed. *)
Looks sensible.
> @@ -214,7 +224,7 @@ and simplifyLval
> | Field(fi, _) -> E.s (bug "bug in offsetToInt")
> in
> match lv with
> - Mem a, off ->
> + Mem a, off when !convertFieldOffsets ->
> let offidx, restoff = offsetToInt (typeOfLval (Mem a, NoOffset)) off in
> let a' =
> if offidx <> zero then
Agreed.
> @@ -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.
> + let a' = if !simpleMem then makeBasic setTemp a else a in
> + Mem a', off
Looks good.
> (* 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:
> | Var v, off when v.vaddrof && (!convertDirectCalls || not (isFunctionType
> (typeOfLval lv) )) ->
if not !convertFieldOffsets then Var v, off else
> let offidx, restoff = offsetToInt v.vtype off in
> (* We cannot call makeBasic recursively here, so we must do it
Final answers:
> 1) could anyone give me a hint how to fix this?
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.
> 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.
Best regards,
--
Gabriel
------------------------------------------------------------------------------
The demand for IT networking professionals continues to grow, and the
demand for specialized networking skills is growing even more rapidly.
Take a complimentary Learning@Cisco Self-Assessment and learn
about Cisco certifications, training, and career opportunities.
http://p.sf.net/sfu/cisco-dev2dev
_______________________________________________
CIL-users mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/cil-users
