As a follow-up to one of my previous patch, here's another patch that
will make --dosimplify more suitable for generating code, better suited
for software verification.
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.
Sample file that had this problem is attached as "mem.c". Try it as
cilly.asm.exe --printCilAsIs --domakeCFG --dosimplify --no-convert-
field-offsets mem.c
However, in rare cases, there is a problem with arrays and their
modifiers. The option requires CIL to generate temporary variables with
more complex types than previously, and the resultant code is not always
compilable. Consider the following file (volatile_fail.c):
struct M {
unsigned char volatile completed[46U] ;
} volatile *m;
int main()
{
return &m->completed;
}
The result of the conversion is:
struct M {
unsigned char volatile completed[46U] ;
};
struct M volatile *m ;
int main(void)
{
// Compile error here:
unsigned char volatile ( volatile (*__cil_tmp1))[46U] ;
__cil_tmp1 = (unsigned char volatile ( volatile (*))[46U])m;
return ((int )__cil_tmp1);
}
So,
1) could anyone give me a hint how to fix this?
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.
--
Pavel Shved
website: http://coldattic.info/
e-mail: pavel.sh...@gmail.com>From 6c3e51e7ae4882beae61e9600b6803414d9c9e23 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
Field offsets (expressions of the form "&a->f") were converted to
dereference of a's address plus offset in bytes. This option suppresses
such conversion. However, certain code will be non-compileable (arrays
of volatile items inside volatile structs).
The aim of this option is to make --dosimplify-generated code better
verifiable by static code checking tools.
---
src/ext/simplify.ml | 24 +++++++++++++++++++++++-
1 files changed, 23 insertions(+), 1 deletions(-)
diff --git a/src/ext/simplify.ml b/src/ext/simplify.ml
index 0e3de67..fbb9727 100644
--- a/src/ext/simplify.ml
+++ b/src/ext/simplify.ml
@@ -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
@@ -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. *)
@@ -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
@@ -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 ->
+ let a' = if !simpleMem then makeBasic setTemp a else a in
+ Mem a', off
(* 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)
| Var v, off when v.vaddrof && (!convertDirectCalls || not (isFunctionType (typeOfLval lv) )) ->
let offidx, restoff = offsetToInt v.vtype off in
(* We cannot call makeBasic recursively here, so we must do it
@@ -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;
--
1.7.3.4
struct X{
int dummy;
struct {
int q;
} *p;
};
int main()
{
struct X *r;
return r->p->q;
}
struct M {
unsigned char volatile completed[46U] ;
} volatile *m;
int main()
{
return &m->completed;
}
------------------------------------------------------------------------------
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
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
