From af781ed684c538cfa98ef0d35a9d258fec62e495 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jun 2024 12:56:40 +0300 Subject: [PATCH 01/36] Enable ana.float.evaluate_math_functions in svcomp24 and svcomp confs This is needed for sv-benchmarks Juliet no-overflow tasks involving sqrt. We used this at SV-COMP 2024, before the option existed. --- conf/svcomp.json | 3 ++- conf/svcomp24-validate.json | 3 ++- conf/svcomp24.json | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/conf/svcomp.json b/conf/svcomp.json index 467d294bdd..d2bea96040 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -10,7 +10,8 @@ "interval": true }, "float": { - "interval": true + "interval": true, + "evaluate_math_functions": true }, "activated": [ "base", diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json index 7832ffa6af..d83b1767a4 100644 --- a/conf/svcomp24-validate.json +++ b/conf/svcomp24-validate.json @@ -10,7 +10,8 @@ "interval": true }, "float": { - "interval": true + "interval": true, + "evaluate_math_functions": true }, "activated": [ "base", diff --git a/conf/svcomp24.json b/conf/svcomp24.json index 7e30554ceb..1c60f84920 100644 --- a/conf/svcomp24.json +++ b/conf/svcomp24.json @@ -10,7 +10,8 @@ "interval": true }, "float": { - "interval": true + "interval": true, + "evaluate_math_functions": true }, "activated": [ "base", From 3ff00aea295c6e7386323efc88f38d1a046cbdbc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jun 2024 13:00:36 +0300 Subject: [PATCH 02/36] Add tests for imaxabs --- .../39-signed-overflows/11-imaxabs.c | 24 +++++++++++++++++++ .../39-signed-overflows/12-imaxabs-sqrt.c | 12 ++++++++++ 2 files changed, 36 insertions(+) create mode 100644 tests/regression/39-signed-overflows/11-imaxabs.c create mode 100644 tests/regression/39-signed-overflows/12-imaxabs-sqrt.c diff --git a/tests/regression/39-signed-overflows/11-imaxabs.c b/tests/regression/39-signed-overflows/11-imaxabs.c new file mode 100644 index 0000000000..dce200a146 --- /dev/null +++ b/tests/regression/39-signed-overflows/11-imaxabs.c @@ -0,0 +1,24 @@ +//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial +#include +#include +#include +int main() { + int64_t data; + if (data > (-0x7fffffffffffffff - 1)) + { + if (imaxabs(data) < 100) + { + __goblint_check(data < 100); // TODO + __goblint_check(-100 < data); // TODO + int64_t result = data * data; // TODO NOWARN + } + + if(imaxabs(data) <= 100) + { + __goblint_check(data <= 100); // TODO + __goblint_check(-100 <= data); // TODO + int64_t result = data * data; // TODO NOWARN + } + } + return 8; +} diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c new file mode 100644 index 0000000000..b121645b27 --- /dev/null +++ b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c @@ -0,0 +1,12 @@ +//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.evaluate_math_functions --set ana.activated[+] tmpSpecial +#include +#include +#include +int main() { + int64_t data; + if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL)) + { + int64_t result = data * data; // TODO NOWARN + } + return 8; +} From 2653e2ea22dd9d012a10e008f3189e1061d2c344 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jun 2024 13:02:26 +0300 Subject: [PATCH 03/36] Add hacky imaxabs support --- src/util/library/libraryFunctions.ml | 2 +- tests/regression/39-signed-overflows/11-imaxabs.c | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index e7ff2a4d04..df90339c65 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -139,7 +139,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) }); ("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) }); ("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) }); - ("imaxabs", unknown [drop "j" []]); + ("imaxabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) }); (* TODO: look up intmax_t ikind from CIL file *) ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]); ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]); ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *) diff --git a/tests/regression/39-signed-overflows/11-imaxabs.c b/tests/regression/39-signed-overflows/11-imaxabs.c index dce200a146..47bd26569f 100644 --- a/tests/regression/39-signed-overflows/11-imaxabs.c +++ b/tests/regression/39-signed-overflows/11-imaxabs.c @@ -8,16 +8,16 @@ int main() { { if (imaxabs(data) < 100) { - __goblint_check(data < 100); // TODO - __goblint_check(-100 < data); // TODO - int64_t result = data * data; // TODO NOWARN + __goblint_check(data < 100); + __goblint_check(-100 < data); + int64_t result = data * data; // NOWARN } if(imaxabs(data) <= 100) { - __goblint_check(data <= 100); // TODO - __goblint_check(-100 <= data); // TODO - int64_t result = data * data; // TODO NOWARN + __goblint_check(data <= 100); + __goblint_check(-100 <= data); + int64_t result = data * data; // NOWARN } } return 8; From f9765da81d64a99f77c385835c6c0a5c3db419da Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jun 2024 13:05:26 +0300 Subject: [PATCH 04/36] Add hacky imaxabs sqrt refine support --- src/analyses/baseInvariant.ml | 3 ++- tests/regression/39-signed-overflows/12-imaxabs-sqrt.c | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 51a27e19f8..d5b65a95f4 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -785,7 +785,8 @@ struct | TFloat (fk, _), FLongDouble | TFloat (FDouble as fk, _), FDouble | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st - | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st) + | TInt (ik, _), _ -> inv_exp (Int (FD.to_int ik c)) e st (* TODO: is this cast refinement correct? *) + | t, fk -> fallback (fun () -> Pretty.dprintf "CastE: incompatible types %a and %a" CilType.Typ.pretty t CilType.Fkind.pretty fk) st) | CastE ((TInt (ik, _)) as t, e), Int c | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *) (match eval e st with diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c index b121645b27..46512aed21 100644 --- a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c +++ b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c @@ -6,7 +6,7 @@ int main() { int64_t data; if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL)) { - int64_t result = data * data; // TODO NOWARN + int64_t result = data * data; // NOWARN } return 8; } From a1f0b35703e34da0eda8f3f27ea260a58fd2c85d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jun 2024 13:15:01 +0300 Subject: [PATCH 05/36] Find intmax_t for imaxabs from program --- src/util/library/libraryFunctions.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index df90339c65..689eb17126 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -6,6 +6,16 @@ open GobConfig module M = Messages +let intmax_t = lazy ( + let res = ref None in + GoblintCil.iterGlobals !Cilfacade.current_file (function + | GType ({tname = "intmax_t"; ttype; _}, _) -> + res := Some ttype; + | _ -> () + ); + !res +) + (** C standard library functions. These are specified by the C standard. *) let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -139,7 +149,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) }); ("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) }); ("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) }); - ("imaxabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) }); (* TODO: look up intmax_t ikind from CIL file *) + ("imaxabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (Cilfacade.get_ikind (Option.get (Lazy.force intmax_t)), j)) }); ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]); ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]); ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *) From 67f8fe9195d3c6a96b01a0a5ceddf05a81fb1ff6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 9 Oct 2024 10:28:06 +0300 Subject: [PATCH 06/36] Add test for invariant_set widening tokens (issue #1299) --- .../56-witness/64-apron-unassume-set-tokens.c | 18 ++++++ .../64-apron-unassume-set-tokens.yml | 59 +++++++++++++++++++ tests/regression/56-witness/dune | 3 +- 3 files changed, 79 insertions(+), 1 deletion(-) create mode 100644 tests/regression/56-witness/64-apron-unassume-set-tokens.c create mode 100644 tests/regression/56-witness/64-apron-unassume-set-tokens.yml diff --git a/tests/regression/56-witness/64-apron-unassume-set-tokens.c b/tests/regression/56-witness/64-apron-unassume-set-tokens.c new file mode 100644 index 0000000000..75a6b5eee5 --- /dev/null +++ b/tests/regression/56-witness/64-apron-unassume-set-tokens.c @@ -0,0 +1,18 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 64-apron-unassume-set-tokens.yml --set ana.apron.domain polyhedra --enable ana.widen.tokens +#include +// Uses polyhedra instead of octagon such that widening tokens are actually needed by test instead of narrowing. +// Copied & extended from 56-witness/12-apron-unassume-branch. +int main() { + int i = 0; + while (i < 100) { + i++; + } + assert(i == 100); + + int j = 0; + while (j < 100) { + j++; + } + assert(j == 100); + return 0; +} diff --git a/tests/regression/56-witness/64-apron-unassume-set-tokens.yml b/tests/regression/56-witness/64-apron-unassume-set-tokens.yml new file mode 100644 index 0000000000..8411ed045f --- /dev/null +++ b/tests/regression/56-witness/64-apron-unassume-set-tokens.yml @@ -0,0 +1,59 @@ +- entry_type: invariant_set + metadata: + format_version: "0.1" + uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e + creation_time: 2022-07-26T09:11:03Z + producer: + name: Goblint + version: heads/yaml-witness-unassume-0-g48503c690-dirty + command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' + ''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled'' + ''64-apron-unassume-set-tokens.c''' + task: + input_files: + - 64-apron-unassume-set-tokens.c + input_file_hashes: + 64-apron-unassume-set-tokens.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 + data_model: LP64 + language: C + content: + - invariant: + type: location_invariant + location: + file_name: 64-apron-unassume-set-tokens.c + file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 + line: 8 + column: 3 + function: main + value: 99LL - (long long )i >= 0LL + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 64-apron-unassume-set-tokens.c + file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 + line: 8 + column: 3 + function: main + value: (long long )i >= 0LL + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 64-apron-unassume-set-tokens.c + file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 + line: 14 + column: 3 + function: main + value: 99LL - (long long )j >= 0LL + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 64-apron-unassume-set-tokens.c + file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 + line: 14 + column: 3 + function: main + value: (long long )j >= 0LL + format: c_expression diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune index 215e47deb2..f6694c60ec 100644 --- a/tests/regression/56-witness/dune +++ b/tests/regression/56-witness/dune @@ -21,7 +21,8 @@ (run %{update_suite} hh-ex3 -q) (run %{update_suite} bh-ex1-poly -q) (run %{update_suite} apron-unassume-precheck -q) - (run %{update_suite} apron-tracked-global-annot -q))))) + (run %{update_suite} apron-tracked-global-annot -q) + (run %{update_suite} apron-unassume-set-tokens -q))))) (cram (deps (glob_files *.c) (glob_files ??-*.yml))) From 7ec6b0578b6da2996114c8f9a60a75cb056fa231 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 8 Oct 2024 17:50:41 +0300 Subject: [PATCH 07/36] Add optional int indices to widening tokens --- src/analyses/apron/relationAnalysis.apron.ml | 4 ++-- src/analyses/base.ml | 4 ++-- src/analyses/unassumeAnalysis.ml | 12 ++++++------ src/domains/events.ml | 4 ++-- src/lifters/wideningTokens.ml | 3 +-- src/lifters/wideningTokens0.ml | 6 ++++++ 6 files changed, 19 insertions(+), 14 deletions(-) create mode 100644 src/lifters/wideningTokens0.ml diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index da14dfff1d..f82bd37e33 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -701,7 +701,7 @@ struct Priv.escape ctx.node (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st escaped | Assert exp -> assert_fn ctx exp true - | Events.Unassume {exp = e; uuids} -> + | Events.Unassume {exp = e; tokens} -> let e_orig = e in let ask = Analyses.ask_of_ctx ctx in let e = replace_deref_exps ctx.ask e in @@ -737,7 +737,7 @@ struct (* TODO: parallel write_global? *) let st = - WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () -> + WideningTokens.with_side_tokens (WideningTokens.TS.of_list tokens) (fun () -> VH.fold (fun v v_in st -> (* TODO: is this sideg fine? *) write_global ask ctx.global ctx.sideg st v v_in diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 1699108394..a5a9fc150e 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -3091,8 +3091,8 @@ struct set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid)) | Events.Assert exp -> assert_fn ctx exp true - | Events.Unassume {exp; uuids} -> - Timing.wrap "base unassume" (unassume ctx exp) uuids + | Events.Unassume {exp; tokens} -> + Timing.wrap "base unassume" (unassume ctx exp) tokens | Events.Longjmped {lval} -> begin match lval with | Some lval -> diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 8f8892b8be..348215993b 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -29,7 +29,7 @@ struct type inv = { exp: Cil.exp; - uuid: string; + token: WideningTokens.Token.t; } let invs: inv NH.t = NH.create 100 @@ -101,7 +101,7 @@ struct match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with | Ok inv_exp -> M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp; - NH.add invs n {exp = inv_exp; uuid} + NH.add invs n {exp = inv_exp; token = (uuid, None)} (* TODO: Some *) | Error e -> M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv; M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv @@ -154,7 +154,7 @@ struct M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp; if not (NH.mem pre_invs n) then NH.replace pre_invs n (EH.create 10); - EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; uuid} + EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)} (* TODO: Some *) | Error e -> M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv; M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv @@ -262,9 +262,9 @@ struct M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e; if not !AnalysisState.postsolving then ( if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (ctx.ask (EvalInt e)) = Some false) then ( - let uuids = x.uuid :: List.map (fun {uuid; _} -> uuid) xs in - ctx.emit (Unassume {exp = e; uuids}); - List.iter WideningTokens.add uuids + let tokens = x.token :: List.map (fun {token; _} -> token) xs in + ctx.emit (Unassume {exp = e; tokens}); + List.iter WideningTokens.add tokens ) ); ctx.local diff --git a/src/domains/events.ml b/src/domains/events.ml index b194847bac..b3054b8416 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -14,7 +14,7 @@ type t = | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *) | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *) | Assert of exp - | Unassume of {exp: CilType.Exp.t; uuids: string list} + | Unassume of {exp: CilType.Exp.t; tokens: WideningTokens0.Token.t list} | Longjmped of {lval: CilType.Lval.t option} (** Should event be emitted after transfer function raises [Deadcode]? *) @@ -45,5 +45,5 @@ let pretty () = function | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp | Assert exp -> dprintf "Assert %a" d_exp exp - | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids + | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningTokens0.Token.pretty) tokens | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval diff --git a/src/lifters/wideningTokens.ml b/src/lifters/wideningTokens.ml index 41bb5d8477..4d60099d7e 100644 --- a/src/lifters/wideningTokens.ml +++ b/src/lifters/wideningTokens.ml @@ -6,8 +6,7 @@ @see Mihaila, B., Sepp, A. & Simon, A. Widening as Abstract Domain. *) -(** Widening token. *) -module Token = Basetype.RawStrings (* Change to variant type if need other tokens than witness UUIDs. *) +include WideningTokens0 (** Widening token set. *) module TS = SetDomain.ToppedSet (Token) (struct let topname = "Top" end) diff --git a/src/lifters/wideningTokens0.ml b/src/lifters/wideningTokens0.ml new file mode 100644 index 0000000000..dcbf77424e --- /dev/null +++ b/src/lifters/wideningTokens0.ml @@ -0,0 +1,6 @@ +(** Widening token. *) +module Token = +struct + (* Change to variant type if need other tokens than witness UUIDs. *) + include Printable.Prod (Basetype.RawStrings) (Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end)) +end From 21c000c71bfae7e31fbc18d83d61a802dd854c03 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 8 Oct 2024 17:55:02 +0300 Subject: [PATCH 08/36] Add invariant_set index to widening token --- src/analyses/unassumeAnalysis.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 348215993b..6b5b495233 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -90,7 +90,7 @@ struct let uuid = entry.metadata.uuid in let target_type = YamlWitnessType.EntryType.entry_type entry.entry_type in - let unassume_nodes_invariant ~loc ~nodes inv = + let unassume_nodes_invariant ~loc ~nodes ?i inv = let msgLoc: M.Location.t = CilLocation loc in match InvariantParser.parse_cabs inv with | Ok inv_cabs -> @@ -101,7 +101,7 @@ struct match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with | Ok inv_exp -> M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp; - NH.add invs n {exp = inv_exp; token = (uuid, None)} (* TODO: Some *) + NH.add invs n {exp = inv_exp; token = (uuid, i)} | Error e -> M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv; M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv @@ -154,7 +154,7 @@ struct M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp; if not (NH.mem pre_invs n) then NH.replace pre_invs n (EH.create 10); - EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)} (* TODO: Some *) + EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)} | Error e -> M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv; M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv @@ -189,42 +189,42 @@ struct let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) = - let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) = + let unassume_location_invariant ~i (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) = let loc = YamlWitness.loc_of_location location_invariant.location in let inv = location_invariant.value in let msgLoc: M.Location.t = CilLocation loc in match Locator.find_opt location_locator loc with | Some nodes -> - unassume_nodes_invariant ~loc ~nodes inv + unassume_nodes_invariant ~loc ~nodes ~i inv | None -> M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv in - let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) = + let unassume_loop_invariant ~i (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) = let loc = YamlWitness.loc_of_location loop_invariant.location in let inv = loop_invariant.value in let msgLoc: M.Location.t = CilLocation loc in match Locator.find_opt loop_locator loc with | Some nodes -> - unassume_nodes_invariant ~loc ~nodes inv + unassume_nodes_invariant ~loc ~nodes ~i inv | None -> M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv in - let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) = + let validate_invariant i (invariant: YamlWitnessType.InvariantSet.Invariant.t) = let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in match YamlWitness.invariant_type_enabled target_type, invariant.invariant_type with | true, LocationInvariant x -> - unassume_location_invariant x + unassume_location_invariant ~i x | true, LoopInvariant x -> - unassume_loop_invariant x + unassume_loop_invariant ~i x | false, (LocationInvariant _ | LoopInvariant _) -> M.info_noloc ~category:Witness "disabled invariant of type %s" target_type in - List.iter validate_invariant invariant_set.content + List.iteri validate_invariant invariant_set.content in match YamlWitness.entry_type_enabled target_type, entry.entry_type with From 57a044713a03cd28d199fb16cd4c9b332b31f32d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 9 Oct 2024 10:35:11 +0300 Subject: [PATCH 09/36] Rename widening token modules --- src/analyses/apron/relationAnalysis.apron.ml | 6 +++--- src/analyses/base.ml | 6 +++--- src/analyses/mCP.ml | 12 ++++++------ src/analyses/unassumeAnalysis.ml | 4 ++-- src/domains/events.ml | 4 ++-- src/framework/control.ml | 2 +- src/goblint_lib.ml | 3 ++- src/lifters/wideningToken.ml | 4 ++++ .../{wideningTokens.ml => wideningTokenLifter.ml} | 2 +- src/lifters/wideningTokens0.ml | 6 ------ 10 files changed, 24 insertions(+), 25 deletions(-) create mode 100644 src/lifters/wideningToken.ml rename src/lifters/{wideningTokens.ml => wideningTokenLifter.ml} (99%) delete mode 100644 src/lifters/wideningTokens0.ml diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index f82bd37e33..28e365bd97 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -690,7 +690,7 @@ struct Priv.lock ask ctx.global st m ) st addr | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) - WideningTokens.with_local_side_tokens (fun () -> + WideningTokenLifter.with_local_side_tokens (fun () -> CommonPriv.lift_unlock ask (fun st m -> Priv.unlock ask ctx.global ctx.sideg st m ) st addr @@ -737,7 +737,7 @@ struct (* TODO: parallel write_global? *) let st = - WideningTokens.with_side_tokens (WideningTokens.TS.of_list tokens) (fun () -> + WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list tokens) (fun () -> VH.fold (fun v v_in st -> (* TODO: is this sideg fine? *) write_global ask ctx.global ctx.sideg st v v_in @@ -771,7 +771,7 @@ struct let new_value = RD.join old_value st in PCU.RH.replace results ctx.node new_value; end; - WideningTokens.with_local_side_tokens (fun () -> + WideningTokenLifter.with_local_side_tokens (fun () -> Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread]) ) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index a5a9fc150e..fcf720e5eb 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -447,7 +447,7 @@ struct in if M.tracing then M.tracel "sync" "sync multi=%B earlyglobs=%B" multi !earlyglobs; if !earlyglobs || multi then - WideningTokens.with_local_side_tokens (fun () -> + WideningTokenLifter.with_local_side_tokens (fun () -> Priv.sync (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) ctx.local reason ) else @@ -3058,7 +3058,7 @@ struct (* Perform actual [set]-s with final unassumed values. This invokes [Priv.write_global], which was suppressed above. *) let e_d' = - WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () -> + WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list uuids) (fun () -> CPA.fold (fun x v acc -> let addr: AD.t = AD.of_mval (x, `NoOffset) in set ~ctx ~invariant:false acc addr x.vtype v @@ -3077,7 +3077,7 @@ struct Priv.lock ask (priv_getg ctx.global) st m ) st addr | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) - WideningTokens.with_local_side_tokens (fun () -> + WideningTokenLifter.with_local_side_tokens (fun () -> CommonPriv.lift_unlock ask (fun st m -> Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st m ) st addr diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 6212b6de90..742e796fbd 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -156,20 +156,20 @@ struct else iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs - let do_sideg ctx (xs:(V.t * (WideningTokens.TS.t * G.t)) list) = + let do_sideg ctx (xs:(V.t * (WideningTokenLifter.TS.t * G.t)) list) = let side_one v dts = let side_one_ts ts d = (* Do side effects with the tokens that were active at the time. Transfer functions have exited the with_side_token wrappers by now. *) - let old_side_tokens = !WideningTokens.side_tokens in - WideningTokens.side_tokens := ts; + let old_side_tokens = !WideningTokenLifter.side_tokens in + WideningTokenLifter.side_tokens := ts; Fun.protect (fun () -> ctx.sideg v @@ fold_left G.join (G.bot ()) d ) ~finally:(fun () -> - WideningTokens.side_tokens := old_side_tokens + WideningTokenLifter.side_tokens := old_side_tokens ) in - iter (uncurry side_one_ts) @@ group_assoc_eq WideningTokens.TS.equal dts + iter (uncurry side_one_ts) @@ group_assoc_eq WideningTokenLifter.TS.equal dts in iter (uncurry side_one) @@ group_assoc_eq V.equal xs @@ -355,7 +355,7 @@ struct | None -> (fun ?(multiple=false) v d -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context.")) in let sideg = match sides with - | Some sides -> (fun v g -> sides := (v, (!WideningTokens.side_tokens, g)) :: !sides) + | Some sides -> (fun v g -> sides := (v, (!WideningTokenLifter.side_tokens, g)) :: !sides) | None -> (fun v g -> failwith ("Cannot \"sideg\" in " ^ tfname ^ " context.")) in let emit = match emits with diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 6b5b495233..615dbd3266 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -29,7 +29,7 @@ struct type inv = { exp: Cil.exp; - token: WideningTokens.Token.t; + token: WideningToken.t; } let invs: inv NH.t = NH.create 100 @@ -264,7 +264,7 @@ struct if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (ctx.ask (EvalInt e)) = Some false) then ( let tokens = x.token :: List.map (fun {token; _} -> token) xs in ctx.emit (Unassume {exp = e; tokens}); - List.iter WideningTokens.add tokens + List.iter WideningTokenLifter.add tokens ) ); ctx.local diff --git a/src/domains/events.ml b/src/domains/events.ml index b3054b8416..cf12900c98 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -14,7 +14,7 @@ type t = | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *) | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *) | Assert of exp - | Unassume of {exp: CilType.Exp.t; tokens: WideningTokens0.Token.t list} + | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list} | Longjmped of {lval: CilType.Lval.t option} (** Should event be emitted after transfer function raises [Deadcode]? *) @@ -45,5 +45,5 @@ let pretty () = function | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp | Assert exp -> dprintf "Assert %a" d_exp exp - | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningTokens0.Token.pretty) tokens + | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval diff --git a/src/framework/control.ml b/src/framework/control.ml index 1d0ebb869b..2566939817 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -39,7 +39,7 @@ let spec_module: (module Spec) Lazy.t = lazy ( |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter) (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens. Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *) - |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter) + |> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter) |> lift true (module LongjmpLifter.Lifter) |> lift termination_enabled (module RecursionTermLifter.Lifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*) ) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 91f9837419..d8fd408151 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -180,7 +180,8 @@ module SpecLifters = SpecLifters module LongjmpLifter = LongjmpLifter module RecursionTermLifter = RecursionTermLifter module ContextGasLifter = ContextGasLifter -module WideningTokens = WideningTokens +module WideningToken = WideningToken +module WideningTokenLifter = WideningTokenLifter module WitnessConstraints = WitnessConstraints diff --git a/src/lifters/wideningToken.ml b/src/lifters/wideningToken.ml new file mode 100644 index 0000000000..d780c4e793 --- /dev/null +++ b/src/lifters/wideningToken.ml @@ -0,0 +1,4 @@ +(** Widening token for {!WideningTokenLifter}. *) + +(* Change to variant type if need other tokens than witness UUIDs. *) +include Printable.Prod (Basetype.RawStrings) (Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end)) diff --git a/src/lifters/wideningTokens.ml b/src/lifters/wideningTokenLifter.ml similarity index 99% rename from src/lifters/wideningTokens.ml rename to src/lifters/wideningTokenLifter.ml index 4d60099d7e..634468a9ca 100644 --- a/src/lifters/wideningTokens.ml +++ b/src/lifters/wideningTokenLifter.ml @@ -6,7 +6,7 @@ @see Mihaila, B., Sepp, A. & Simon, A. Widening as Abstract Domain. *) -include WideningTokens0 +module Token = WideningToken (** Widening token set. *) module TS = SetDomain.ToppedSet (Token) (struct let topname = "Top" end) diff --git a/src/lifters/wideningTokens0.ml b/src/lifters/wideningTokens0.ml deleted file mode 100644 index dcbf77424e..0000000000 --- a/src/lifters/wideningTokens0.ml +++ /dev/null @@ -1,6 +0,0 @@ -(** Widening token. *) -module Token = -struct - (* Change to variant type if need other tokens than witness UUIDs. *) - include Printable.Prod (Basetype.RawStrings) (Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end)) -end From a2817445e67768d30ef86b2ece90b5f00d3ffee5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 9 Oct 2024 10:38:14 +0300 Subject: [PATCH 10/36] Improve widening token output --- src/lifters/wideningToken.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/lifters/wideningToken.ml b/src/lifters/wideningToken.ml index d780c4e793..0639521038 100644 --- a/src/lifters/wideningToken.ml +++ b/src/lifters/wideningToken.ml @@ -1,4 +1,16 @@ (** Widening token for {!WideningTokenLifter}. *) +module Uuid = +struct + include Basetype.RawStrings + let name () = "uuid" +end + +module Index = +struct + include Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end) + let name () = "index" +end + (* Change to variant type if need other tokens than witness UUIDs. *) -include Printable.Prod (Basetype.RawStrings) (Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end)) +include Printable.Prod (Uuid) (Index) From 2f5b50fa9081abda073a33b393ef33c282c1ebc4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 16 Oct 2024 16:51:40 +0300 Subject: [PATCH 11/36] Revert "Add hacky imaxabs sqrt refine support" This reverts commit f9765da81d64a99f77c385835c6c0a5c3db419da. --- src/analyses/baseInvariant.ml | 3 +-- tests/regression/39-signed-overflows/12-imaxabs-sqrt.c | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index d5b65a95f4..51a27e19f8 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -785,8 +785,7 @@ struct | TFloat (fk, _), FLongDouble | TFloat (FDouble as fk, _), FDouble | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st - | TInt (ik, _), _ -> inv_exp (Int (FD.to_int ik c)) e st (* TODO: is this cast refinement correct? *) - | t, fk -> fallback (fun () -> Pretty.dprintf "CastE: incompatible types %a and %a" CilType.Typ.pretty t CilType.Fkind.pretty fk) st) + | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st) | CastE ((TInt (ik, _)) as t, e), Int c | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *) (match eval e st with diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c index 46512aed21..b121645b27 100644 --- a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c +++ b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c @@ -6,7 +6,7 @@ int main() { int64_t data; if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL)) { - int64_t result = data * data; // NOWARN + int64_t result = data * data; // TODO NOWARN } return 8; } From f7a5afa966d6dc4b62748fdb1738f2b2aef2f844 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 16 Oct 2024 17:39:07 +0300 Subject: [PATCH 12/36] Add 39-signed-overflows/13-imaxabs-macos test --- .../39-signed-overflows/13-imaxabs-macos.c | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 tests/regression/39-signed-overflows/13-imaxabs-macos.c diff --git a/tests/regression/39-signed-overflows/13-imaxabs-macos.c b/tests/regression/39-signed-overflows/13-imaxabs-macos.c new file mode 100644 index 0000000000..745d5b74c4 --- /dev/null +++ b/tests/regression/39-signed-overflows/13-imaxabs-macos.c @@ -0,0 +1,25 @@ +//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial +// 39-signed-overflows/11-imaxabs, but with long long as int64_t instead (https://github.com/goblint/analyzer/pull/1519#issuecomment-2417032186). +#include +#include +#include +int main() { + long long data; + if (data > (-0x7fffffffffffffff - 1)) + { + if (imaxabs(data) < 100) + { + __goblint_check(data < 100); + __goblint_check(-100 < data); + long long result = data * data; // NOWARN + } + + if(imaxabs(data) <= 100) + { + __goblint_check(data <= 100); + __goblint_check(-100 <= data); + long long result = data * data; // NOWARN + } + } + return 8; +} From 62834684764e5e1bc88705f19c54fa22a0d35d64 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 16 Oct 2024 17:55:20 +0300 Subject: [PATCH 13/36] Unroll cast type in BaseInvariant --- src/analyses/baseInvariant.ml | 58 +++++++++++++++++++---------------- 1 file changed, 31 insertions(+), 27 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 51a27e19f8..52f0888d3f 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -777,33 +777,37 @@ struct | _ -> assert false end | Const _ , _ -> st (* nothing to do *) - | CastE ((TFloat (_, _)), e), Float c -> - (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with - | TFloat (FLongDouble as fk, _), FFloat - | TFloat (FDouble as fk, _), FFloat - | TFloat (FLongDouble as fk, _), FDouble - | TFloat (fk, _), FLongDouble - | TFloat (FDouble as fk, _), FDouble - | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st - | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st) - | CastE ((TInt (ik, _)) as t, e), Int c - | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *) - (match eval e st with - | Int i -> - (match unrollType (Cilfacade.typeOf e) with - | (TInt(ik_e, _) as t') - | (TEnum ({ekind = ik_e; _ }, _) as t') -> - if VD.is_dynamically_safe_cast t t' (Int i) then - (* let c' = ID.cast_to ik_e c in *) - (* Suppressing overflow warnings as this is not a computation that comes from the program *) - let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in - let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *) - if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c'; - inv_exp (Int c') e st - else - fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st - | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st) - | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st) + | CastE (t, e), c_typed -> + begin match Cil.unrollType t, c_typed with + | TFloat (_, _), Float c -> + (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with + | TFloat (FLongDouble as fk, _), FFloat + | TFloat (FDouble as fk, _), FFloat + | TFloat (FLongDouble as fk, _), FDouble + | TFloat (fk, _), FLongDouble + | TFloat (FDouble as fk, _), FDouble + | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st + | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st) + | (TInt (ik, _) as t), Int c + | (TEnum ({ekind = ik; _ }, _) as t), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *) + (match eval e st with + | Int i -> + (match unrollType (Cilfacade.typeOf e) with + | (TInt(ik_e, _) as t') + | (TEnum ({ekind = ik_e; _ }, _) as t') -> + if VD.is_dynamically_safe_cast t t' (Int i) then + (* let c' = ID.cast_to ik_e c in *) + (* Suppressing overflow warnings as this is not a computation that comes from the program *) + let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in + let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *) + if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c'; + inv_exp (Int c') e st + else + fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st + | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st) + | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st) + | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (t, e))) st + end | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st in if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *) From e12d6df901069f353c7a2a9ff08dfd6130a6507b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 17 Oct 2024 15:26:28 +0300 Subject: [PATCH 14/36] Copy svcomp confs to svcomp25 --- conf/svcomp25-validate.json | 122 ++++++++++++++++++++++++++++++++++++ conf/svcomp25.json | 117 ++++++++++++++++++++++++++++++++++ 2 files changed, 239 insertions(+) create mode 100644 conf/svcomp25-validate.json create mode 100644 conf/svcomp25.json diff --git a/conf/svcomp25-validate.json b/conf/svcomp25-validate.json new file mode 100644 index 0000000000..f0e99057d1 --- /dev/null +++ b/conf/svcomp25-validate.json @@ -0,0 +1,122 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "unassume" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "termination", + "tmpSpecialAnalysis" + ] + }, + "widen": { + "tokens": true + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": false + }, + "yaml": { + "enabled": false, + "strict": true, + "format-version": "2.0", + "entry-types": [ + "location_invariant", + "loop_invariant", + "invariant_set", + "violation_sequence" + ], + "invariant-types": [ + "location_invariant", + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": true, + "other": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/svcomp25.json b/conf/svcomp25.json new file mode 100644 index 0000000000..aa3f625da9 --- /dev/null +++ b/conf/svcomp25.json @@ -0,0 +1,117 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} From 6a973802a229367f7112637c0b37d5e979560a8d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 17 Oct 2024 15:28:42 +0300 Subject: [PATCH 15/36] Update sv-comp/archive.sh for 2025 --- scripts/sv-comp/archive.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/sv-comp/archive.sh b/scripts/sv-comp/archive.sh index 37fa2758d9..aefac8f769 100755 --- a/scripts/sv-comp/archive.sh +++ b/scripts/sv-comp/archive.sh @@ -4,7 +4,7 @@ make clean -git tag -m "SV-COMP 2024" svcomp24 +git tag -m "SV-COMP 2025" svcomp25 dune build --profile=release src/goblint.exe rm -f goblint @@ -32,8 +32,8 @@ zip goblint/scripts/sv-comp/goblint.zip \ goblint/lib/libboxD.so \ goblint/lib/libpolkaMPQ.so \ goblint/lib/LICENSE.APRON \ - goblint/conf/svcomp24.json \ - goblint/conf/svcomp24-validate.json \ + goblint/conf/svcomp25.json \ + goblint/conf/svcomp25-validate.json \ goblint/lib/libc/stub/include/assert.h \ goblint/lib/goblint/runtime/include/goblint.h \ goblint/lib/libc/stub/src/stdlib.c \ From d3c5d353cec4b9b875c5a3f12bc09647f4c03bcf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 18 Oct 2024 12:20:55 +0300 Subject: [PATCH 16/36] Document SV-COMP bench-defs MR --- docs/developer-guide/releasing.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md index 7530d9ad20..aca0749eb9 100644 --- a/docs/developer-guide/releasing.md +++ b/docs/developer-guide/releasing.md @@ -77,6 +77,8 @@ This includes: git tag name, git tag message and zipped conf file. +5. Open MR with conf file name to the [bench-defs](https://gitlab.com/sosy-lab/sv-comp/bench-defs) repository. + ### For each prerun 1. Update opam pins: From b1095fbd71b7360e1a6d7a7d8b9bcc3b790b3bef Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Nov 2024 11:32:06 +0200 Subject: [PATCH 17/36] Add more precise YAML witness generation summary --- src/witness/yamlWitness.ml | 13 ++++++++++++ .../03-practical/35-base-mutex-macos.t | 3 +++ tests/regression/13-privatized/01-priv_nr.t | 9 ++++++++ .../regression/36-apron/12-traces-min-rpb1.t | 3 +++ tests/regression/36-apron/52-queuesize.t | 6 ++++++ .../11-unrolled-loop-invariant.t | 3 +++ tests/regression/56-witness/05-prec-problem.t | 3 +++ .../56-witness/08-witness-all-locals.t | 6 ++++++ .../56-witness/46-top-bool-invariant.t | 21 +++++++++++++++++++ .../56-witness/47-top-int-invariant.t | 21 +++++++++++++++++++ tests/regression/cfg/foo.t/run.t | 3 +++ tests/regression/cfg/issue-1356.t/run.t | 3 +++ tests/regression/cfg/loops.t/run.t | 3 +++ tests/regression/cfg/pr-758.t/run.t | 3 +++ tests/regression/witness/int.t/run.t | 3 +++ tests/regression/witness/typedef.t/run.t | 6 ++++++ 16 files changed, 109 insertions(+) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 2bdd2ced4c..bc31797688 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -249,6 +249,11 @@ struct let entries = [] in + let cnt_loop_invariant = ref 0 in + let cnt_location_invariant = ref 0 in + let cnt_flow_insensitive_invariant = ref 0 in + (* TODO: precondition invariants? *) + (* Generate location invariants (without precondition) *) let entries = if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then ( @@ -268,6 +273,7 @@ struct List.fold_left (fun acc inv -> let invariant = Entry.invariant (CilType.Exp.show inv) in let entry = Entry.location_invariant ~task ~location ~invariant in + incr cnt_location_invariant; entry :: acc ) acc invs | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) @@ -297,6 +303,7 @@ struct List.fold_left (fun acc inv -> let invariant = Entry.invariant (CilType.Exp.show inv) in let entry = Entry.loop_invariant ~task ~location ~invariant in + incr cnt_loop_invariant; entry :: acc ) acc invs | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) @@ -322,6 +329,7 @@ struct List.fold_left (fun acc inv -> let invariant = Entry.invariant (CilType.Exp.show inv) in let entry = Entry.flow_insensitive_invariant ~task ~invariant in + incr cnt_flow_insensitive_invariant; entry :: acc ) acc invs | `Bot | `Top -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *) @@ -459,6 +467,7 @@ struct List.fold_left (fun acc inv -> let invariant = CilType.Exp.show inv in let invariant = Entry.location_invariant' ~location ~invariant in + incr cnt_location_invariant; invariant :: acc ) acc invs | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) @@ -488,6 +497,7 @@ struct List.fold_left (fun acc inv -> let invariant = CilType.Exp.show inv in let invariant = Entry.loop_invariant' ~location ~invariant in + incr cnt_loop_invariant; invariant :: acc ) acc invs | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) @@ -512,6 +522,9 @@ struct let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *) M.msg_group Info ~category:Witness "witness generation summary" [ + (Pretty.dprintf "location invariants: %d" !cnt_location_invariant, None); + (Pretty.dprintf "loop invariants: %d" !cnt_loop_invariant, None); + (Pretty.dprintf "flow-insensitive invariants: %d" !cnt_flow_insensitive_invariant, None); (Pretty.dprintf "total generation entries: %d" (List.length yaml_entries), None); ]; diff --git a/tests/regression/03-practical/35-base-mutex-macos.t b/tests/regression/03-practical/35-base-mutex-macos.t index 9e5f36d337..1d8a184d4c 100644 --- a/tests/regression/03-practical/35-base-mutex-macos.t +++ b/tests/regression/03-practical/35-base-mutex-macos.t @@ -4,6 +4,9 @@ dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 1 There should be no invariants about __sig. diff --git a/tests/regression/13-privatized/01-priv_nr.t b/tests/regression/13-privatized/01-priv_nr.t index bbc285098a..0186709027 100644 --- a/tests/regression/13-privatized/01-priv_nr.t +++ b/tests/regression/13-privatized/01-priv_nr.t @@ -10,6 +10,9 @@ dead: 0 total lines: 19 [Info][Witness] witness generation summary: + location invariants: 3 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 3 [Info][Race] Memory locations race summary: safe: 1 @@ -64,6 +67,9 @@ dead: 0 total lines: 19 [Info][Witness] witness generation summary: + location invariants: 3 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 3 [Info][Race] Memory locations race summary: safe: 1 @@ -118,6 +124,9 @@ dead: 0 total lines: 19 [Info][Witness] witness generation summary: + location invariants: 3 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 3 [Info][Race] Memory locations race summary: safe: 1 diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t index 5060f505d9..d0cebd6d1c 100644 --- a/tests/regression/36-apron/12-traces-min-rpb1.t +++ b/tests/regression/36-apron/12-traces-min-rpb1.t @@ -13,6 +13,9 @@ write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:14:3-14:8) read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:27:3-27:26) [Info][Witness] witness generation summary: + location invariants: 3 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 3 [Info][Race] Memory locations race summary: safe: 0 diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t index 62851f2ec9..f0a977891a 100644 --- a/tests/regression/36-apron/52-queuesize.t +++ b/tests/regression/36-apron/52-queuesize.t @@ -37,6 +37,9 @@ Without diff-box: [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:56:10-56:11) [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:78:12-78:13) [Info][Witness] witness generation summary: + location invariants: 8 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 8 [Info][Race] Memory locations race summary: safe: 3 @@ -173,6 +176,9 @@ With diff-box: [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:56:10-56:11) [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:78:12-78:13) [Info][Witness] witness generation summary: + location invariants: 6 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 6 [Info][Race] Memory locations race summary: safe: 3 diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t index 3a3b7c43cf..860ffae3bd 100644 --- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -211,6 +211,9 @@ [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:9:12-9:19) [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:10-8:16) [Info][Witness] witness generation summary: + location invariants: 11 + loop invariants: 5 + flow-insensitive invariants: 0 total generation entries: 16 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t index 733f16269e..51f92ca203 100644 --- a/tests/regression/56-witness/05-prec-problem.t +++ b/tests/regression/56-witness/05-prec-problem.t @@ -6,6 +6,9 @@ total lines: 13 [Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (05-prec-problem.c:13:12-13:13) [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 6 TODO: Don't generate duplicate entries from each context: should have generated just 3. diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t index fc4462201d..fe6aefefbd 100644 --- a/tests/regression/56-witness/08-witness-all-locals.t +++ b/tests/regression/56-witness/08-witness-all-locals.t @@ -4,6 +4,9 @@ dead: 0 total lines: 4 [Info][Witness] witness generation summary: + location invariants: 3 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 3 $ yamlWitnessStrip < witness.yml @@ -50,6 +53,9 @@ Fewer entries are emitted if locals from nested block scopes are excluded: dead: 0 total lines: 4 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/56-witness/46-top-bool-invariant.t b/tests/regression/56-witness/46-top-bool-invariant.t index 741b00966f..be41ef58f2 100644 --- a/tests/regression/56-witness/46-top-bool-invariant.t +++ b/tests/regression/56-witness/46-top-bool-invariant.t @@ -6,6 +6,9 @@ def_exc only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml @@ -40,6 +43,9 @@ interval only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml @@ -74,6 +80,9 @@ enums only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 1 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 1 $ yamlWitnessStrip < witness.yml @@ -97,6 +106,9 @@ congruence only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 0 $ yamlWitnessStrip < witness.yml @@ -110,6 +122,9 @@ interval_set only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml @@ -144,6 +159,9 @@ all: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 1 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 1 $ yamlWitnessStrip < witness.yml @@ -167,6 +185,9 @@ all without inexact-type-bounds: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 0 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/56-witness/47-top-int-invariant.t b/tests/regression/56-witness/47-top-int-invariant.t index cdfe65673f..35d5978c00 100644 --- a/tests/regression/56-witness/47-top-int-invariant.t +++ b/tests/regression/56-witness/47-top-int-invariant.t @@ -6,6 +6,9 @@ def_exc only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml @@ -40,6 +43,9 @@ interval only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml @@ -74,6 +80,9 @@ enums only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml @@ -108,6 +117,9 @@ congruence only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 0 $ yamlWitnessStrip < witness.yml @@ -121,6 +133,9 @@ interval_set only: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml @@ -155,6 +170,9 @@ all: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 2 $ yamlWitnessStrip < witness.yml @@ -189,6 +207,9 @@ all without inexact-type-bounds: dead: 0 total lines: 2 [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 0 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index cd890b7a19..19873d7540 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -67,6 +67,9 @@ total lines: 6 [Warning][Deadcode][CWE-571] condition 'a > 0' (possibly inserted by CIL) is always true (foo.c:3:10-3:20) [Info][Witness] witness generation summary: + location invariants: 8 + loop invariants: 2 + flow-insensitive invariants: 0 total generation entries: 10 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t index aee9456b61..d1fcb3c7ef 100644 --- a/tests/regression/cfg/issue-1356.t/run.t +++ b/tests/regression/cfg/issue-1356.t/run.t @@ -99,6 +99,9 @@ dead: 0 total lines: 13 [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 0 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t index 6596e7b4a4..1fd19b41fe 100644 --- a/tests/regression/cfg/loops.t/run.t +++ b/tests/regression/cfg/loops.t/run.t @@ -219,6 +219,9 @@ dead: 0 total lines: 20 [Info][Witness] witness generation summary: + location invariants: 32 + loop invariants: 21 + flow-insensitive invariants: 0 total generation entries: 53 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t index 58bbb88ce4..082c63e860 100644 --- a/tests/regression/cfg/pr-758.t/run.t +++ b/tests/regression/cfg/pr-758.t/run.t @@ -93,6 +93,9 @@ dead: 0 total lines: 6 [Info][Witness] witness generation summary: + location invariants: 10 + loop invariants: 2 + flow-insensitive invariants: 0 total generation entries: 12 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/witness/int.t/run.t b/tests/regression/witness/int.t/run.t index 6b4784ce32..9448ac7855 100644 --- a/tests/regression/witness/int.t/run.t +++ b/tests/regression/witness/int.t/run.t @@ -7,6 +7,9 @@ dead: 0 total lines: 10 [Info][Witness] witness generation summary: + location invariants: 3 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 3 $ yamlWitnessStrip < witness.yml diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t index 55dcc1f911..f9fac0c743 100644 --- a/tests/regression/witness/typedef.t/run.t +++ b/tests/regression/witness/typedef.t/run.t @@ -4,6 +4,9 @@ dead: 0 total lines: 6 [Info][Witness] witness generation summary: + location invariants: 13 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 13 $ yamlWitnessStrip < witness.yml @@ -157,6 +160,9 @@ dead: 0 total lines: 6 [Info][Witness] witness generation summary: + location invariants: 14 + loop invariants: 0 + flow-insensitive invariants: 0 total generation entries: 14 $ yamlWitnessStrip < witness.yml From 77190828a810819b5b607c59d1553fc713b1be9d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Nov 2024 11:45:13 +0200 Subject: [PATCH 18/36] Add witness.yaml.strict option description --- src/config/options.schema.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 447290b44d..9c1f9e1e76 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2659,7 +2659,7 @@ }, "strict": { "title": "witness.yaml.strict", - "description": "", + "description": "Fail YAML witness validation if there's an error/unsupported/disabled entry.", "type": "boolean", "default": false }, From 546a8d04ede0d6646e1d5b20095c0ae5e2f0a78b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Nov 2024 11:49:17 +0200 Subject: [PATCH 19/36] Update YAML witness validation result for refutation under new scoring schema --- src/witness/yamlWitness.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index bc31797688..1a8c536da5 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -892,7 +892,9 @@ struct | true when !cnt_disabled > 0 -> Error "witness disabled" | _ when !cnt_refuted > 0 -> - Ok (Svcomp.Result.False None) + (* Refuted only when assuming the invariant is reachable. *) + (* Ok (Svcomp.Result.False None) *) (* Wasn't a problem because valid*->correctness->false gave 0 points under old validator track scoring schema: https://doi.org/10.1007/978-3-031-22308-2_8. *) + Ok Svcomp.Result.Unknown (* Now valid*->correctness->false gives 1p (negative) points under new validator track scoring schema: https://doi.org/10.1007/978-3-031-57256-2_15. *) | _ when !cnt_unconfirmed > 0 -> Ok Unknown | _ -> From 2048122f114dd24acaa0ff8b4fbd431d92c291f8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Nov 2024 11:57:42 +0200 Subject: [PATCH 20/36] Fix YAML witness validate/unassume error with empty (unparsable) path Raised an obscure Invalid_argument exception instead. --- src/analyses/unassumeAnalysis.ml | 2 +- src/witness/yamlWitness.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 615dbd3266..707e0f4820 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -71,7 +71,7 @@ struct | _ -> () ); - let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with + let yaml = match GobResult.Syntax.(Fpath.of_string (GobConfig.get_string "witness.yaml.unassume") >>= Yaml_unix.of_file) with | Ok yaml -> yaml | Error (`Msg m) -> Logs.error "Yaml_unix.of_file: %s" m; diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 1a8c536da5..06e355068e 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -608,7 +608,7 @@ struct let inv_parser = InvariantParser.create FileCfg.file in - let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate")) with + let yaml = match GobResult.Syntax.(Fpath.of_string (GobConfig.get_string "witness.yaml.validate") >>= Yaml_unix.of_file) with | Ok yaml -> yaml | Error (`Msg m) -> Logs.error "Yaml_unix.of_file: %s" m; From 8d8b6752af3d23260a9c5ab080eb26bdf740006d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Nov 2024 17:40:49 +0200 Subject: [PATCH 21/36] Remove outdated comments about new __VERIFIER_nondet functions --- lib/sv-comp/stub/src/sv-comp.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/sv-comp/stub/src/sv-comp.c b/lib/sv-comp/stub/src/sv-comp.c index 12c04125d6..469a641e73 100644 --- a/lib/sv-comp/stub/src/sv-comp.c +++ b/lib/sv-comp/stub/src/sv-comp.c @@ -35,10 +35,10 @@ __VERIFIER_nondet2(unsigned int, u32) __VERIFIER_nondet2(unsigned short int, u16) // not in rules __VERIFIER_nondet2(unsigned char, u8) // not in rules __VERIFIER_nondet2(unsigned char, unsigned_char) // not in rules -__VERIFIER_nondet2(long long, longlong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341) -__VERIFIER_nondet2(unsigned long long, ulonglong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341) -__VERIFIER_nondet2(__uint128_t, uint128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341) -__VERIFIER_nondet2(__int128_t, int128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341) +__VERIFIER_nondet2(long long, longlong) +__VERIFIER_nondet2(unsigned long long, ulonglong) +__VERIFIER_nondet2(__uint128_t, uint128) +__VERIFIER_nondet2(__int128_t, int128) __VERIFIER_nondet2(unsigned char, uchar) __VERIFIER_nondet2(unsigned int, uint) __VERIFIER_nondet2(unsigned long, ulong) From 6a05022657c9da91e90cea46c0c420650a77fb16 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 18 Nov 2024 13:37:44 +0200 Subject: [PATCH 22/36] Add initial CHANGELOG for SV-COMP 2025 --- CHANGELOG.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 420cc7145e..6e9fe29306 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,17 @@ +## v2.5.0 (unreleased) +Functionally equivalent to Goblint in SV-COMP 2025. + +### SV-COMP 2025 +* Improve invariants (#1361, #1362, #1375, #1328, #1493, #1356). +* Simplify invariants (#1436, #1517). +* Improve YAML witness locations (#1355, #1372, #1400, #1403). +* Improve autotuner (#1469, #1450, #1612, #1604, #1181). +* Loop unrolling (#1582, #1583, #1584, #1516, #1590, #1595, #1599). +* Add abortUnless to svcomp (#1464). +* Fix spurious overflow warnings (#1511). +* Add primitive YAML violation witness rejection (#1301, #1512). +* Machdep support (#54, #1574). + ## v2.4.0 * Remove unmaintained analyses: spec, file (#1281). * Add linear two-variable equalities analysis (#1297, #1412, #1466). From 152ebb633d32275d8cb9924fd54541c2ac64917b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 18 Nov 2024 13:51:22 +0200 Subject: [PATCH 23/36] Add initial CHANGELOG for v2.5.0 --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6e9fe29306..aec84573cf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,10 @@ ## v2.5.0 (unreleased) Functionally equivalent to Goblint in SV-COMP 2025. +* Cleanup (#1095, #1523, #1554, #1575, #1588, #1597, #1614). +* Reduce hash collisions (#1594, #1602). +* Context gas per function (#1569, #1570, #1598). + ### SV-COMP 2025 * Improve invariants (#1361, #1362, #1375, #1328, #1493, #1356). * Simplify invariants (#1436, #1517). From 64981452f455f42cef61de0ab044f3131497db6d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 18 Nov 2024 14:08:10 +0200 Subject: [PATCH 24/36] Add CHANGELOG for v2.5.0 --- CHANGELOG.md | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index aec84573cf..cf6a8aa781 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,20 +1,13 @@ ## v2.5.0 (unreleased) Functionally equivalent to Goblint in SV-COMP 2025. -* Cleanup (#1095, #1523, #1554, #1575, #1588, #1597, #1614). -* Reduce hash collisions (#1594, #1602). -* Context gas per function (#1569, #1570, #1598). - -### SV-COMP 2025 -* Improve invariants (#1361, #1362, #1375, #1328, #1493, #1356). -* Simplify invariants (#1436, #1517). -* Improve YAML witness locations (#1355, #1372, #1400, #1403). -* Improve autotuner (#1469, #1450, #1612, #1604, #1181). -* Loop unrolling (#1582, #1583, #1584, #1516, #1590, #1595, #1599). -* Add abortUnless to svcomp (#1464). -* Fix spurious overflow warnings (#1511). -* Add primitive YAML violation witness rejection (#1301, #1512). -* Machdep support (#54, #1574). +* Add 32bit vs 64bit architecture support (#54, #1574). +* Add per-function context gas analysis (#1569, #1570, #1598). +* Adapt automatic static loop unrolling (#1516, #1582, #1583, #1584, #1590, #1595, #1599). +* Adapt automatic configuration tuning (#1450, #1612, #1181, #1604). +* Simplify non-relational integer invariants in witnesses (#1517). +* Fix excessive hash collisions (#1594, #1602). +* Clean up various code (#1095, #1523, #1554, #1575, #1588, #1597, #1614). ## v2.4.0 * Remove unmaintained analyses: spec, file (#1281). @@ -28,7 +21,7 @@ Functionally equivalent to Goblint in SV-COMP 2025. * Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510). * Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407). * Improve narrowing operators (#1502, #1540, #1543). -* Extract automatic configuration tuning for soundness (#1369). +* Extract automatic configuration tuning for soundness (#1469). * Fix many locations in witnesses (#1355, #1372, #1400, #1403). * Improve output readability (#1294, #1312, #1405, #1497). * Refactor logging (#1117). From aeb2376811f30d6d9b7f814b685d04643ede5190 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Nov 2024 15:31:39 +0200 Subject: [PATCH 25/36] Clean up Z_mlgmpidl usages --- src/cdomains/apron/apronDomain.apron.ml | 2 +- src/cdomains/apron/gobApron.apron.ml | 2 ++ src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 2 +- src/cdomains/apron/sharedFunctions.apron.ml | 4 ++-- 4 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 03ac3ed3f0..043b728799 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -19,7 +19,7 @@ module M = Messages let widening_thresholds_apron = ResettableLazy.from_fun (fun () -> let t = if GobConfig.get_string "ana.apron.threshold_widening_constants" = "comparisons" then WideningThresholds.octagon_thresholds () else WideningThresholds.thresholds_incl_mul2 () in - let r = List.map (fun x -> Apron.Scalar.of_mpqf @@ Mpqf.of_mpz @@ Z_mlgmpidl.mpz_of_z x) t in + let r = List.map Scalar.of_z t in Array.of_list r ) diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml index fbb1fe9ec5..327e43e321 100644 --- a/src/cdomains/apron/gobApron.apron.ml +++ b/src/cdomains/apron/gobApron.apron.ml @@ -12,6 +12,8 @@ struct let pp = pp end ) + + let of_z z = of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z)) end module Coeff = diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index c1ca3661a5..6af7030a51 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -790,7 +790,7 @@ struct let of_coeff xi coeffs o = let typ = (Option.get @@ V.to_cil_varinfo xi).vtype in let ikind = Cilfacade.get_ikind typ in - let cst = Coeff.s_of_mpqf @@ Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z @@ IntDomain.Size.cast ikind o) in + let cst = Coeff.s_of_z (IntDomain.Size.cast ikind o) in let lincons = Lincons1.make (Linexpr1.make t.env) Lincons1.EQ in Lincons1.set_list lincons coeffs (Some cst); lincons diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 86b5f2770f..b9d93bfd99 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -133,7 +133,7 @@ struct else failwith "texpr1_expr_of_cil_exp: globals must be replaced with temporary locals" | Const (CInt (i, _, _)) -> - Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z i))) + Cst (Coeff.s_of_z i) | exp -> match Cilfacade.get_ikind_exp exp with | ik -> @@ -175,7 +175,7 @@ struct (* convert response to a constant *) let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res in match const with - | Some c -> Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z c))) (* Got a constant value -> use it straight away *) + | Some c -> Cst (Coeff.s_of_z c) (* Got a constant value -> use it straight away *) (* I gotten top, we can not guarantee injectivity *) | None -> if IntDomain.IntDomTuple.is_top_of t_ik res then raise (Unsupported_CilExp (Cast_not_injective t)) else ( (* Got a ranged value different from top, so let's check bounds manually *) From 0ca1bb30f50d12bec84198ae404994c510e37431 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 22 Nov 2024 11:11:34 +0200 Subject: [PATCH 26/36] Add parsing of integer constraints in YAML violation_sequence-s --- src/util/std/gobYaml.ml | 2 ++ src/witness/yamlWitnessType.ml | 26 +++++++++++++++++++++++--- 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/util/std/gobYaml.ml b/src/util/std/gobYaml.ml index 624cdbf1fa..4c8576ade2 100644 --- a/src/util/std/gobYaml.ml +++ b/src/util/std/gobYaml.ml @@ -44,3 +44,5 @@ let list = function let entries = function | `O assoc -> Ok assoc | _ -> Error (`Msg "Failed to get entries from non-object value") + +let int i = float (float_of_int i) diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index 4fc2029801..c77fadad4c 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -447,15 +447,35 @@ struct module Constraint = struct + + module Value = + struct + type t = + | String of string + | Int of int (* Why doesn't format consider ints (for switch branches) as strings here, like everywhere else? *) + [@@deriving ord] + + let to_yaml = function + | String s -> GobYaml.string s + | Int i -> GobYaml.int i + + let of_yaml y = + let open GobYaml in + match y with + | `String s -> Ok (String s) + | `Float f -> Ok (Int (int_of_float f)) + | _ -> Error (`Msg "Expected a string or integer value") + end + type t = { - value: string; + value: Value.t; format: string option; } [@@deriving ord] let to_yaml {value; format} = `O ([ - ("value", `String value); + ("value", Value.to_yaml value); ] @ (match format with | Some format -> [ ("format", `String format); @@ -466,7 +486,7 @@ struct let of_yaml y = let open GobYaml in - let+ value = y |> find "value" >>= to_string + let+ value = y |> find "value" >>= Value.of_yaml and+ format = y |> Yaml.Util.find "format" >>= option_map to_string in {value; format} end From d7074f1e9526c0df5f146d267c35038b2bb65770 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 27 Nov 2024 13:44:50 +0200 Subject: [PATCH 27/36] Add Karoliine's email to opam maintainer field opam-repository CI now demands this. Co-authored-by: Karoliine Holter --- dune-project | 2 +- goblint.opam | 2 +- goblint.opam.locked | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/dune-project b/dune-project index 54915cf964..f2f87b3c58 100644 --- a/dune-project +++ b/dune-project @@ -16,7 +16,7 @@ (homepage "https://goblint.in.tum.de") (documentation "https://goblint.readthedocs.io/en/latest/") (authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff -(maintainers "Simmo Saan " "Michael Schwarz " "Karoliine Holter") +(maintainers "Simmo Saan " "Michael Schwarz " "Karoliine Holter ") (license MIT) (package diff --git a/goblint.opam b/goblint.opam index 44e5ccd2c2..f74ffab8c4 100644 --- a/goblint.opam +++ b/goblint.opam @@ -9,7 +9,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e maintainer: [ "Simmo Saan " "Michael Schwarz " - "Karoliine Holter" + "Karoliine Holter " ] authors: [ "Simmo Saan" diff --git a/goblint.opam.locked b/goblint.opam.locked index 9fbee1e02b..cedb4088b8 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -5,7 +5,7 @@ synopsis: "Static analysis framework for C" maintainer: [ "Simmo Saan " "Michael Schwarz " - "Karoliine Holter" + "Karoliine Holter " ] authors: [ "Simmo Saan" From 65ddbbb7d06236e2a266ef2967f58c59528a48c6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Nov 2024 10:27:35 +0200 Subject: [PATCH 28/36] Finalize CHANGELOG for v2.5.0 --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index cf6a8aa781..1fb07a7dc2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,4 +1,4 @@ -## v2.5.0 (unreleased) +## v2.5.0 Functionally equivalent to Goblint in SV-COMP 2025. * Add 32bit vs 64bit architecture support (#54, #1574). From 629cd493201c133e284f45437816ab82fe305742 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Nov 2024 10:34:13 +0200 Subject: [PATCH 29/36] Replace goblint-cil pin with published 2.0.5 --- dune-project | 2 +- goblint.opam | 5 +++-- goblint.opam.locked | 6 +----- goblint.opam.template | 3 ++- 4 files changed, 7 insertions(+), 9 deletions(-) diff --git a/dune-project b/dune-project index f2f87b3c58..9a1d958484 100644 --- a/dune-project +++ b/dune-project @@ -37,7 +37,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e "concurrency")) (depends (ocaml (>= 4.14)) - (goblint-cil (>= 2.0.4)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint. + (goblint-cil (>= 2.0.5)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint. (batteries (>= 3.5.1)) (zarith (>= 1.10)) (yojson (>= 2.0.0)) diff --git a/goblint.opam b/goblint.opam index f74ffab8c4..9fa877d54f 100644 --- a/goblint.opam +++ b/goblint.opam @@ -37,7 +37,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues" depends: [ "dune" {>= "3.7"} "ocaml" {>= "4.14"} - "goblint-cil" {>= "2.0.4"} + "goblint-cil" {>= "2.0.5"} "batteries" {>= "3.5.1"} "zarith" {>= "1.10"} "yojson" {>= "2.0.0"} @@ -97,7 +97,8 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") pin-depends: [ - [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ] + # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed + # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release diff --git a/goblint.opam.locked b/goblint.opam.locked index cedb4088b8..081731a9a3 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -64,7 +64,7 @@ depends: [ "fileutils" {= "0.6.4"} "fmt" {= "0.9.0"} "fpath" {= "0.7.3"} - "goblint-cil" {= "2.0.4"} + "goblint-cil" {= "2.0.5"} "hex" {= "1.5.0"} "integers" {= "0.7.0"} "json-data-encoding" {= "1.0.1"} @@ -138,10 +138,6 @@ post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] pin-depends: [ - [ - "goblint-cil.2.0.4" - "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" - ] [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" diff --git a/goblint.opam.template b/goblint.opam.template index 0a517fbfa0..d05a0af61d 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -2,7 +2,8 @@ # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") pin-depends: [ - [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ] + # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed + # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release From d066c8dd711317ae969639d45285aa5664767daa Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Nov 2024 10:35:32 +0200 Subject: [PATCH 30/36] Disable pins for v2.5.0 release --- goblint.opam | 8 ++++---- goblint.opam.locked | 10 ---------- goblint.opam.template | 8 ++++---- 3 files changed, 8 insertions(+), 18 deletions(-) diff --git a/goblint.opam b/goblint.opam index 9fa877d54f..9f2b874ff6 100644 --- a/goblint.opam +++ b/goblint.opam @@ -96,14 +96,14 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") -pin-depends: [ +# pin-depends: [ # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release - [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] + # [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] # 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" ] -] + # [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ] +# ] depexts: [ ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} ] diff --git a/goblint.opam.locked b/goblint.opam.locked index 081731a9a3..3a7bb1bfa5 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -137,16 +137,6 @@ conflicts: [ post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] -pin-depends: [ - [ - "camlidl.1.12" - "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" - ] - [ - "apron.v0.9.15" - "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" - ] -] depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} description: """\ Goblint is a sound static analysis framework for C programs using abstract interpretation. diff --git a/goblint.opam.template b/goblint.opam.template index d05a0af61d..8766a89df2 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -1,14 +1,14 @@ # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") -pin-depends: [ +# pin-depends: [ # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release - [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] + # [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] # 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" ] -] + # [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ] +# ] depexts: [ ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} ] From 0df4d8647afbfd2d65043c13f89047ecc3a2219b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Nov 2024 13:36:28 +0200 Subject: [PATCH 31/36] Update goblint-cil to 2.0.5 in Gobview lock file --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index 76e42c34d3..8e1b755ebc 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 76e42c34d36bd2ab6900efd661a972ba4824f065 +Subproject commit 8e1b755ebc5fb479095fb4dcc30305fe02501e47 From eb9ee513ba2cb1811750d58fd10370f31c21dda1 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Nov 2024 14:52:54 +0200 Subject: [PATCH 32/36] Make 29-svcomp/36-svcomp-arch multilib detection more precise Also handles missing gcc-multilib on Linux, e.g. in opam docker. There's no conf-* package for gcc-multilib. --- tests/regression/29-svcomp/dune | 2 +- tests/util/dune | 7 ++++++- tests/util/multilibConfigure.ml | 4 ++++ 3 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 tests/util/multilibConfigure.ml diff --git a/tests/regression/29-svcomp/dune b/tests/regression/29-svcomp/dune index 95ac66a5ec..9b2396b313 100644 --- a/tests/regression/29-svcomp/dune +++ b/tests/regression/29-svcomp/dune @@ -17,4 +17,4 @@ (cram (applies_to 36-svcomp-arch) - (enabled_if (<> %{system} macosx))) ; https://dune.readthedocs.io/en/stable/reference/boolean-language.html + (enabled_if %{read:../../util/multilibAvailable})) ; https://dune.readthedocs.io/en/stable/reference/boolean-language.html diff --git a/tests/util/dune b/tests/util/dune index 0e32304d4f..e43d21c25d 100644 --- a/tests/util/dune +++ b/tests/util/dune @@ -1,7 +1,8 @@ (executables - (names yamlWitnessStrip yamlWitnessStripDiff) + (names yamlWitnessStrip yamlWitnessStripDiff multilibConfigure) (libraries batteries.unthreaded + goblint-cil goblint_std goblint_lib yaml @@ -9,3 +10,7 @@ goblint.build-info.dune) (flags :standard -open Goblint_std) (preprocess (pps ppx_deriving.std))) + +(rule + (target multilibAvailable) + (action (with-stdout-to %{target} (run ./multilibConfigure.exe)))) diff --git a/tests/util/multilibConfigure.ml b/tests/util/multilibConfigure.ml new file mode 100644 index 0000000000..cf59e04416 --- /dev/null +++ b/tests/util/multilibConfigure.ml @@ -0,0 +1,4 @@ +open GoblintCil + +let () = + Printf.printf "%B" (Option.is_some GoblintCil.Machdep.gcc32 && Option.is_some GoblintCil.Machdep.gcc64) From 7170d9a8944706a1adc0acaeb81a4fc6d914af7b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Nov 2024 15:00:16 +0200 Subject: [PATCH 33/36] Fix unused open in multilibConfigure --- tests/util/multilibConfigure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/util/multilibConfigure.ml b/tests/util/multilibConfigure.ml index cf59e04416..96cf9a706a 100644 --- a/tests/util/multilibConfigure.ml +++ b/tests/util/multilibConfigure.ml @@ -1,4 +1,4 @@ open GoblintCil let () = - Printf.printf "%B" (Option.is_some GoblintCil.Machdep.gcc32 && Option.is_some GoblintCil.Machdep.gcc64) + Printf.printf "%B" (Option.is_some Machdep.gcc32 && Option.is_some Machdep.gcc64) From 4f83ce8369977071c5a749ad50cf5ebba7aa4f75 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 29 Nov 2024 10:51:02 +0200 Subject: [PATCH 34/36] Revert "Disable pins for v2.5.0 release" This reverts commit d066c8dd711317ae969639d45285aa5664767daa. --- goblint.opam | 8 ++++---- goblint.opam.locked | 10 ++++++++++ goblint.opam.template | 8 ++++---- 3 files changed, 18 insertions(+), 8 deletions(-) diff --git a/goblint.opam b/goblint.opam index 9f2b874ff6..9fa877d54f 100644 --- a/goblint.opam +++ b/goblint.opam @@ -96,14 +96,14 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") -# pin-depends: [ +pin-depends: [ # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release - # [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] + [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] # 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" ] -# ] + [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ] +] depexts: [ ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} ] diff --git a/goblint.opam.locked b/goblint.opam.locked index 3a7bb1bfa5..081731a9a3 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -137,6 +137,16 @@ conflicts: [ post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] +pin-depends: [ + [ + "camlidl.1.12" + "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" + ] + [ + "apron.v0.9.15" + "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" + ] +] depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} description: """\ Goblint is a sound static analysis framework for C programs using abstract interpretation. diff --git a/goblint.opam.template b/goblint.opam.template index 8766a89df2..d05a0af61d 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -1,14 +1,14 @@ # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") -# pin-depends: [ +pin-depends: [ # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release - # [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] + [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] # 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" ] -# ] + [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ] +] depexts: [ ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} ] From 77acd917865a4385c160155740d20615c0e87f2a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 29 Nov 2024 10:58:11 +0200 Subject: [PATCH 35/36] Pin released goblint-cil.2.0.5 for reproducibility --- goblint.opam | 4 ++-- goblint.opam.locked | 4 ++++ goblint.opam.template | 4 ++-- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/goblint.opam b/goblint.opam index 9fa877d54f..219c67d011 100644 --- a/goblint.opam +++ b/goblint.opam @@ -97,8 +97,8 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") pin-depends: [ - # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed - # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] + # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility + [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release diff --git a/goblint.opam.locked b/goblint.opam.locked index 081731a9a3..2594aea288 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -138,6 +138,10 @@ post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] pin-depends: [ + [ + "oblint-cil.2.0.5" + "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" + ] [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" diff --git a/goblint.opam.template b/goblint.opam.template index d05a0af61d..84dcc24d8d 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -2,8 +2,8 @@ # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") pin-depends: [ - # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed - # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] + # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility + [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release From 68cd95237ebbb2023f6c9f7e59dc5f2d33d8ad45 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 29 Nov 2024 11:30:41 +0200 Subject: [PATCH 36/36] Fix goblint-cil typo in opam lock file --- goblint.opam.locked | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/goblint.opam.locked b/goblint.opam.locked index 2594aea288..e5176b9007 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -139,7 +139,7 @@ post-messages: [ ] pin-depends: [ [ - "oblint-cil.2.0.5" + "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ] [