diff --git a/goblint.opam b/goblint.opam index a9761e2c8e..18058d787c 100644 --- a/goblint.opam +++ b/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" ] ] diff --git a/goblint.opam.locked b/goblint.opam.locked index 461ed08fba..7eec37c243 100644 --- a/goblint.opam.locked +++ b/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" diff --git a/goblint.opam.template b/goblint.opam.template index 7cb4e0eb82..9423915d3c 100644 --- a/goblint.opam.template +++ b/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" ] ] diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9aa421dc54..b161a22bf5 100644 --- a/src/analyses/base.ml +++ b/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 _ diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index da17d1fff6..e3503c5e56 100644 --- a/src/common/util/cilfacade.ml +++ b/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); diff --git a/tests/regression/70-transform/03-deadcode-globals.t b/tests/regression/70-transform/03-deadcode-globals.t index ee3fae2c80..ddfb64e052 100644 --- a/tests/regression/70-transform/03-deadcode-globals.t +++ b/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 ;