Thanks, Gabriel! After implementing your suggestions, the patch looks
much more concise. Attached.
Using simplification of structs with --no-convert-field offsets yeilds
an assertion failure ("Cannot find component .foo of bar"). Could it be
the result of contradiction between splitting structures and attempts to
keep the structural information instead of relying to a low-level memory
model?
Assume that the code (the original or an "intermediate" version) looks
like this.
struct A {int x; int y;};
struct B {struct A a;};
int some_function(struct A *ptr) { return ptr->y; }
int main()
{
struct B b;
some_function(&b.a);
}
I do not really understand the intent of split structus, but could it,
under some circumstances, result in something like this:
in main()
{
int x_in_a, y_in_a;
some_function(&x_in_a);
}
The converted some_function then won't have any access to y_in_a,
because all expressions like ((*int)(&x_in_a) + 4) should not appear in
the generated code, and there's no other way to reach y_in_a in the
fixed code. If such situation may appear with split structures, then
splitting structures should be suppressed when using --no-convert-field-
offsets, like it is in the patch.
However, I do not really understand in what cases splitting structures
happens. Is the situation like the one above feasible?
--
Pavel Shved
website: http://coldattic.info/
e-mail: pavel.sh...@gmail.com>From ea6aece8d2dd3e7a04b6dbef5bc754491bceb224 Mon Sep 17 00:00:00 2001
From: Pavel Shved <sh...@ispras.ru>
Date: Fri, 30 Sep 2011 17:00:46 +0400
Subject: [PATCH] Add --no-convert-field-offset to dosimplify
By default, if --dosimplify is used, field offsets (expressions of the
form "&a->f") are converted to dereference of a's address plus offset in
bytes. The new option suppresses such conversion, and keeps other
simplifications.
The aim of this option is to make --dosimplify-generated code better
verifiable by static code checking tools.
---
src/ext/simplify.ml | 39 +++++++++++++++++++++++++++++++++++++--
1 files changed, 37 insertions(+), 2 deletions(-)
diff --git a/src/ext/simplify.ml b/src/ext/simplify.ml
index 0e3de67..3f2aa75 100644
--- a/src/ext/simplify.ml
+++ b/src/ext/simplify.ml
@@ -89,6 +89,25 @@ let simplAddrOf = ref true
* has been taken somewhere. *)
let convertDirectCalls = ref true
+(* Whether to convert field offsets to offsets by integer.
+ * This conversion makes the generated code analysis simpler for static source
+ * code verifiers. *)
+let convertFieldOffsets = ref true
+(* WARN: splitStructs should be set to false if field offsets are not
+ * converted. Otherwise, the connection between a pointer to a structure and
+ * its fields is sometimes lost, and is harder to analyze statically. If a
+ * structure inside a structure (say, "struct A{struct B b} a;" is split into
+ * fields, then, instead of a pointer to the enclosed structure (in "&a.b"), a
+ * pointer to its first member might be used. This will make the rest of the
+ * structure pointed to by "&a.b" be accessed through the (possibly
+ * non-structure) pointer to its first element, which is harder to analyze
+ * statically.
+ *
+ * Last, but not least, this inconsistency will trigger "Cannot find
+ * component .foo of bar" error if you turn splitting structure on and take an
+ * address of bar.foo, where foo is a field of a structure type. :-)
+*)
+
let onlyVariableBasics = ref false
let noStringConstantsBasics = ref false
@@ -116,6 +135,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. *)
@@ -214,7 +237,10 @@ and simplifyLval
| Field(fi, _) -> E.s (bug "bug in offsetToInt")
in
match lv with
- Mem a, off ->
+ Mem a, off when not !convertFieldOffsets ->
+ let a' = if !simpleMem then makeBasic setTemp a else a in
+ Mem a', off
+ | Mem a, off ->
let offidx, restoff = offsetToInt (typeOfLval (Mem a, NoOffset)) off in
let a' =
if offidx <> zero then
@@ -225,8 +251,9 @@ and simplifyLval
let a' = if !simpleMem then makeBasic setTemp a' else a' in
Mem (mkCast a' (typeForCast restoff)), restoff
(* We are taking this variable's address; but suppress simplification if it's a simple function
- * call in no-convert mode*)
+ * call in no-convert-function-calls mode*)
| 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
* ourselves *)
@@ -722,6 +749,14 @@ 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. \
+ Implies --no-split-structs. To be used by static code \
+ verification tools.");
];
fd_doit = (function f -> iterGlobals f doGlobal);
fd_post_check = true;
--
1.7.3.4
------------------------------------------------------------------------------
Get your Android app more play: Bring it to the BlackBerry PlayBook
in minutes. BlackBerry App World™ now supports Android™ Apps
for the BlackBerry® PlayBook™. Discover just how easy and simple
it is! http://p.sf.net/sfu/android-dev2dev
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
