From 6932adc53a0fb0bc0912b0f87e05e7a2e4678458 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 28 Jan 2026 15:33:29 +0200 Subject: [PATCH 1/7] Disable Cil.lowerConstants to not miss checks in constant expressions --- src/common/util/cilfacade.ml | 2 +- tests/regression/70-transform/03-deadcode-globals.t | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index da17d1fff6..05fa485ea0 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; 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 ; From 3aabda0f927596c5ca606f9466205830ac851d47 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 28 Jan 2026 15:51:49 +0200 Subject: [PATCH 2/7] Fold constant conditional expressions in CIL, even without lowerConstants Needed to parse some Linux kernel headers in regression tests which use ternary operator in enum value definition. --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) 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" ] ] From a81a94c52d9ceb80ef908c8c983f38b5aba9d151 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 28 Jan 2026 15:55:21 +0200 Subject: [PATCH 3/7] Disable Cil.constFold in base to not miss checks in constant expressions --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9aa421dc54..0df7f68612 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -821,7 +821,7 @@ 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 *) From fc15bcd305f210c3fc93f99796b4d72bccf21c60 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 28 Jan 2026 20:24:04 +0200 Subject: [PATCH 4/7] Implement SizeOf in eval_rv_base --- src/analyses/base.ml | 6 +++++- src/common/util/cilfacade.ml | 1 + 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 0df7f68612..56e3415d61 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -947,7 +947,11 @@ struct | CastE (kind, t, exp) -> let v = 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 | Real _ | Imag _ | SizeOfE _ diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 05fa485ea0..a4ce40dee1 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -405,6 +405,7 @@ let typeSigBlendAttributes baseAttrs = typeSigAddAttrs contageous +(** @raise SizeOfError *) let bytesSizeOf t = let bits = bitsSizeOf t in assert (bits mod 8 = 0); From 6c63c909a45ccc770551fad2482c87ba08bcfb6e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 28 Jan 2026 20:29:56 +0200 Subject: [PATCH 5/7] Implement Const CEnum in eval_rv_base --- src/analyses/base.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 56e3415d61..c984b5bcc1 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -826,16 +826,17 @@ struct (* 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 From 2466d25896d37a3c3877f7661c64295941618ec9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 28 Jan 2026 20:50:33 +0200 Subject: [PATCH 6/7] Implement offsetof hack in eval_rv_base --- src/analyses/base.ml | 9 ++++++++- src/common/util/cilfacade.ml | 1 + 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c984b5bcc1..717fc43388 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -946,7 +946,14 @@ 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 t -> (* based on [Cil.constFold true] *) begin match Cilfacade.bytesSizeOf t with diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index a4ce40dee1..e3503c5e56 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -411,6 +411,7 @@ let bytesSizeOf t = 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); From da7ab8c0218a403a17ca4436de48f6cf1c9df5f0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 28 Jan 2026 20:57:54 +0200 Subject: [PATCH 7/7] Implement SizeOfE in eval_rv_base --- src/analyses/base.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 717fc43388..b161a22bf5 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -960,9 +960,13 @@ struct | 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 _