From 67f8fe9195d3c6a96b01a0a5ceddf05a81fb1ff6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 9 Oct 2024 10:28:06 +0300 Subject: [PATCH 1/5] 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 2/5] 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 3/5] 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 4/5] 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 5/5] 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)