Merge branch 'checks-constFold-overflow' into dash-dev

Author: karoliineh

goblint.opam

@@ -102,7 +102,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#2edc807cfc8ce80e74e932a8d84a809a44ec0c3d" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

goblint.opam.locked

@@ -148,7 +148,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.9"
-    "git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712"
+    "git+https://github.com/goblint/cil.git#2edc807cfc8ce80e74e932a8d84a809a44ec0c3d"
   ]
   [
     "apron.v0.9.15"

goblint.opam.template

@@ -3,7 +3,7 @@
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#2edc807cfc8ce80e74e932a8d84a809a44ec0c3d" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

src/analyses/base.ml

@@ -821,21 +821,22 @@ struct
     in
     let r =
       (* query functions were no help ... now try with values*)
-      match constFold true exp with
+      match exp with (* TODO: support all cases from [constFold true] directly *)
       (* Integer literals *)
       (* seems like constFold already converts CChr to CInt *)
       | Const (CChr x) -> eval_rv ~man st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)
       | Const (CInt (num,ikind,str)) -> Int (IntDomain.of_const (num,ikind,str)) (* no cast to ikind needed: CIL ensures that the literal fits ikind, either by silently truncating it (!) or having an explicit CastE around this *)
+      | Const (CEnum (v, _, _)) -> eval_rv ~man st v (* based on [Cil.constFold true] *)
       | Const (CReal (_,fkind, Some str)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
       | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) && num = 0.0 -> Float (FD.of_const fkind num) (* constant 0 is ok, CIL creates these for zero-initializers; it is safe across float types *)
       | Const (CReal (_, fkind, None)) when not (Cilfacade.isComplexFKind fkind) ->  assert false (* Cil does not create other CReal without string representation *)
       (* String literals *)
+      | Const (CReal _) -> VD.top ()
       | Const (CStr (x,_)) -> Address (AD.of_string x) (* normal 8-bit strings, type: char* *)
       | Const (CWStr (xs,_) as c) -> (* wide character strings, type: wchar_t* *)
         let x = CilType.Constant.show c in (* escapes, see impl. of d_const in cil.ml *)
         let x = String.sub x 2 (String.length x - 3) in (* remove surrounding quotes: L"foo" -> foo *)
         Address (AD.of_string x) (* Address (AD.str_ptr ()) *)
-      | Const _ -> VD.top ()
       (* Variables and address expressions *)
       | Lval lv ->
         eval_rv_base_lval ~eval_lv ~man st exp lv
@@ -945,12 +946,27 @@ struct
         Address (AD.map array_start (eval_lv ~man st lval))
       | CastE (_, t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
       | CastE (kind, t, exp) ->
-        let v = eval_rv ~man st exp in
+        let v: VD.t = match exp with
+          | AddrOf (Mem (CastE (_, TPtr (bt, _), z)), off) when isZero z -> (* offsetof hack, based on [Cil.constFold true] *)
+            begin match Cilfacade.bytesOffsetOnly bt off with
+              | bytes_offset -> Int (ID.of_int !kindOfSizeOf (Z.of_int bytes_offset))
+              | exception SizeOfError _ -> eval_rv ~man st exp (* TODO: does this ever happen? *)
+            end
+          | _ -> eval_rv ~man st exp
+        in
         VD.cast ~kind t v
-      | SizeOf _
+      | SizeOf t -> (* based on [Cil.constFold true] *)
+        begin match Cilfacade.bytesSizeOf t with
+          | bytes -> Int (ID.of_int !Cil.kindOfSizeOf (Z.of_int bytes))
+          | exception SizeOfError _ -> Int (ID.top_of !Cil.kindOfSizeOf) (* TODO: does this ever happen? *)
+        end
+      | SizeOfE e -> (* based on [Cil.constFold true] and inlined SizeOf *)
+        begin match Cilfacade.bytesSizeOf (Cilfacade.typeOf e) with
+          | bytes -> Int (ID.of_int !Cil.kindOfSizeOf (Z.of_int bytes))
+          | exception SizeOfError _ -> Int (ID.top_of !Cil.kindOfSizeOf) (* TODO: does this ever happen? *)
+        end
       | Real _
       | Imag _
-      | SizeOfE _
       | SizeOfStr _
       | AlignOf _
       | AlignOfE _

src/common/util/cilfacade.ml

@@ -85,7 +85,7 @@ let init () =
   initCIL ();
   removeBranchingOnConstants := false;
   addReturnOnNoreturnFallthrough := true;
-  lowerConstants := true;
+  lowerConstants := false; (* disabled to prevent CIL from constFold-ing constant expressions which still need to be checked (e.g. for overflows) *) (* TODO: lowering enum constants, etc should be separate from general constFold in CIL *)
   Mergecil.ignore_merge_conflicts := true;
   (* lineDirectiveStyle := None; *)
   RmUnused.keepUnused := true;
@@ -405,11 +405,13 @@ let typeSigBlendAttributes baseAttrs =
   typeSigAddAttrs contageous
 
 
+(** @raise SizeOfError *)
 let bytesSizeOf t =
   let bits = bitsSizeOf t in
   assert (bits mod 8 = 0);
   bits / 8
 
+(** @raise SizeOfError *)
 let bytesOffsetOnly t o =
   let bits_offset, _ = bitsOffset t o in
   assert (bits_offset mod 8 = 0);

tests/regression/70-transform/03-deadcode-globals.t

@@ -20,11 +20,11 @@
 
 
     {
-    return ((int )(x->field1 + 1));
+    return ((int )(x->field1 + (int const   )1));
   }
   }
   int const   global1  =    (int const   )1;
-  int const   global2  =    global1 + 7;
+  int const   global2  =    global1 + (int const   )7;
   int main(void) 
   { 
     struct1_named1 x ;