diff --git a/conf/svcomp.json b/conf/svcomp.json index 7e30554ceb..97bdf89cd3 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -84,7 +84,6 @@ "congruence", "octagon", "wideningThresholds", - "loopUnrollHeuristic", "memsafetySpecification", "termination", "tmpSpecialAnalysis" diff --git a/goblint.opam b/goblint.opam index d7724aad34..15c27fe403 100644 --- a/goblint.opam +++ b/goblint.opam @@ -78,7 +78,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed - [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ] + [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#079b426b5cf6ebeade55f11de0b33d6e63ab50b6" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] diff --git a/goblint.opam.locked b/goblint.opam.locked index 2bb831d6ba..69721093cc 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -134,7 +134,7 @@ post-messages: [ pin-depends: [ [ "goblint-cil.2.0.3" - "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" + "git+https://github.com/goblint/cil.git#079b426b5cf6ebeade55f11de0b33d6e63ab50b6" ] [ "ppx_deriving.5.2.1" diff --git a/goblint.opam.template b/goblint.opam.template index 1364586310..abd21204c9 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -3,7 +3,7 @@ available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed - [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ] + [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#079b426b5cf6ebeade55f11de0b33d6e63ab50b6" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] diff --git a/gobview b/gobview index 74e2958708..b33fd0b389 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 74e295870848c66885fa446970b0c59617a242a7 +Subproject commit b33fd0b3894d455a0a65791f4cfdf50f4426f863 diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 9ec69727c0..8fd0a37b62 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -27,7 +27,7 @@ struct module Locator = WitnessUtil.Locator (Node) - let locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *) + let location_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *) let loop_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *) type inv = { @@ -41,26 +41,26 @@ struct let pre_invs: inv EH.t NH.t = NH.create 100 let init _ = - Locator.clear locator; + Locator.clear location_locator; Locator.clear loop_locator; let module FileCfg = struct let file = !Cilfacade.current_file module Cfg = (val !MyCFG.current_cfg) end in - let module WitnessInvariant = WitnessUtil.Invariant (FileCfg) in + let module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in (* DFS, copied from CfgTools.find_backwards_reachable *) let reachable = NH.create 100 in let rec iter_node node = if not (NH.mem reachable node) then begin NH.replace reachable node (); - (* TODO: filter synthetic? - See YamlWitness. *) - if WitnessInvariant.is_invariant_node node then - Locator.add locator (Node.location node) node; - if WitnessUtil.NH.mem WitnessInvariant.loop_heads node then - Locator.add loop_locator (Node.location node) node; + Option.iter (fun loc -> + Locator.add location_locator loc node + ) (WitnessInvariant.location_location node); + Option.iter (fun loc -> + Locator.add loop_locator loc node + ) (WitnessInvariant.loop_location node); List.iter (fun (_, prev_node) -> iter_node prev_node ) (FileCfg.Cfg.prev node) @@ -130,7 +130,7 @@ struct let inv = location_invariant.location_invariant.string in let msgLoc: M.Location.t = CilLocation loc in - match Locator.find_opt locator loc with + match Locator.find_opt location_locator loc with | Some nodes -> unassume_nodes_invariant ~loc ~nodes inv | None -> @@ -193,7 +193,7 @@ struct let inv = precondition_loop_invariant.loop_invariant.string in let msgLoc: M.Location.t = CilLocation loc in - match Locator.find_opt locator loc with + match Locator.find_opt loop_locator loc with | Some nodes -> unassume_precondition_nodes_invariant ~loc ~nodes pre inv | None -> @@ -207,7 +207,7 @@ struct let inv = location_invariant.value in let msgLoc: M.Location.t = CilLocation loc in - match Locator.find_opt locator loc with + match Locator.find_opt location_locator loc with | Some nodes -> unassume_nodes_invariant ~loc ~nodes inv | None -> diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index 6a2540fd18..a2ee2c6634 100644 --- a/src/common/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -132,13 +132,7 @@ let () = Printexc.register_printer (function | _ -> None (* for other exceptions *) ) -(** Type of CFG "edges": keyed by 'from' and 'to' nodes, - along with the list of connecting instructions. *) -module CfgEdge = struct - type t = Node.t * MyCFG.edges * Node.t [@@deriving eq, hash] -end -module CfgEdgeH = BatHashtbl.Make (CfgEdge) let createCFG (file: file) = let cfgF = H.create 113 in @@ -254,7 +248,7 @@ let createCFG (file: file) = let pseudo_return = lazy ( if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname; let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in - let newst = mkStmt (Return (None, fd_end_loc)) in + let newst = mkStmt (Return (None, fd_end_loc, locUnknown)) in newst.sid <- Cilfacade.get_pseudo_return_id fd; Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd; Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst; @@ -340,8 +334,8 @@ let createCFG (file: file) = (* CIL's xform_switch_stmt (via prepareCFG) always adds both continue and break statements to all Loops. *) failwith "MyCFG.createCFG: unprepared Loop" - | Return (exp, loc) -> - addEdge (Statement stmt) (loc, Ret (exp, fd)) (Function fd) + | Return (exp, loc, eloc) -> + addEdge (Statement stmt) (Cilfacade.eloc_fallback ~eloc ~loc, Ret (exp, fd)) (Function fd) | Goto (_, loc) -> (* Gotos are generally unnecessary and unwanted because find_real_stmt skips over these. *) @@ -608,7 +602,7 @@ let fprint_hash_dot cfg = close_out out -let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t = +let getCFG (file: file) : cfg * cfg * _ = let cfgF, cfgB, skippedByEdge = createCFG file in let cfgF, cfgB, skippedByEdge = if get_bool "exp.mincfg" then @@ -617,13 +611,11 @@ let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t = (cfgF, cfgB, skippedByEdge) in if get_bool "justcfg" then fprint_hash_dot cfgB; - (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), skippedByEdge + (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), (fun u e v -> CfgEdgeH.find skippedByEdge (u, e, v)) -let compute_cfg_skips file = +let compute_cfg file = let cfgF, cfgB, skippedByEdge = getCFG file in - (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge - -let compute_cfg file = fst (compute_cfg_skips file) + (module struct let prev = cfgB let next = cfgF let skippedByEdge = skippedByEdge end : CfgBidirSkip) let iter_fd_edges (module Cfg : CfgBackward) fd = diff --git a/src/common/framework/myCFG.ml b/src/common/framework/myCFG.ml index 76675f3c88..22b2b7d679 100644 --- a/src/common/framework/myCFG.ml +++ b/src/common/framework/myCFG.ml @@ -42,19 +42,34 @@ sig include CfgForward end +(** Type of CFG "edges": keyed by 'from' and 'to' nodes, + along with the list of connecting instructions. *) +module CfgEdge = struct + type t = Node.t * edges * Node.t [@@deriving eq, hash] +end + +module CfgEdgeH = BatHashtbl.Make (CfgEdge) + +module type CfgBidirSkip = +sig + include CfgBidir + val skippedByEdge: node -> edges -> node -> stmt list +end + module NodeH = BatHashtbl.Make (Node) let current_node = Node.current_node -let current_cfg : (module CfgBidir) ref = +let current_cfg : (module CfgBidirSkip) ref = let module Cfg = struct let next _ = raise Not_found let prev _ = raise Not_found + let skippedByEdge _ _ _ = raise Not_found end in - ref (module Cfg: CfgBidir) + ref (module Cfg: CfgBidirSkip) let unknown_exp : exp = mkString "__unknown_value__" let dummy_func = emptyFunction "__goblint_dummy_init" (* TODO get rid of this? *) @@ -64,5 +79,5 @@ let dummy_node = FunctionEntry Cil.dummyFunDec module type FileCfg = sig val file: Cil.file - module Cfg: CfgBidir + module Cfg: CfgBidirSkip end diff --git a/src/common/util/cilLocation.ml b/src/common/util/cilLocation.ml index 23c1b8df5b..5b8771d8d4 100644 --- a/src/common/util/cilLocation.ml +++ b/src/common/util/cilLocation.ml @@ -34,7 +34,7 @@ let rec get_stmtLoc stmt: locs = {loc = locUnknown; eloc = locUnknown} | Instr (hd :: _) -> get_instrLoc hd - | Return (_, loc) -> {loc; eloc = locUnknown} + | Return (_, loc, eloc) -> {loc; eloc} | Goto (_, loc) -> {loc; eloc = locUnknown} | ComputedGoto (_, loc) -> {loc; eloc = locUnknown} | Break loc -> {loc; eloc = locUnknown} diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index b5b217889f..2a4e73d588 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -494,7 +494,7 @@ class countFnVisitor = object inherit nopCilVisitor method! vstmt s = match s.skind with - | Return (_, loc) + | Return (_, loc, _) | Goto (_, loc) | ComputedGoto (_, loc) | Break loc diff --git a/src/common/util/cilfacade0.ml b/src/common/util/cilfacade0.ml index 35fd5fb706..5748d9166c 100644 --- a/src/common/util/cilfacade0.ml +++ b/src/common/util/cilfacade0.ml @@ -42,7 +42,7 @@ let rec get_stmtLoc stmt = get_labelsLoc stmt.labels | Instr (hd :: _) -> get_instrLoc hd - | Return (_, loc) -> loc + | Return (_, loc, eloc) -> eloc_fallback ~eloc ~loc | Goto (_, loc) -> loc | ComputedGoto (_, loc) -> loc | Break loc -> loc diff --git a/src/framework/control.ml b/src/framework/control.ml index 6e8e5b7fc4..e11cee9268 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -54,7 +54,7 @@ let current_node_state_json : (Node.t -> Yojson.Safe.t option) ref = ref (fun _ let current_varquery_global_state_json: (VarQuery.t option -> Yojson.Safe.t) ref = ref (fun _ -> `Null) (** Given a [Cfg], a [Spec], and an [Inc], computes the solution to [MCP.Path] *) -module AnalyzeCFG (Cfg:CfgBidir) (Spec:Spec) (Inc:Increment) = +module AnalyzeCFG (Cfg:CfgBidirSkip) (Spec:Spec) (Inc:Increment) = struct module SpecSys: SpecSys with module Spec = Spec = @@ -230,7 +230,7 @@ struct res (** The main function to preform the selected analyses. *) - let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs) skippedByEdge = + let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs) = let module FileCfg: FileCfg = struct let file = file @@ -625,13 +625,16 @@ struct let node_values = LHT.enum lh |> map (Tuple2.map1 fst) in (* drop context from key *) let hashtbl_size = if fast_count node_values then count node_values else 123 in let by_loc, by_node = Hashtbl.create hashtbl_size, NodeH.create hashtbl_size in - node_values |> iter (fun (node, v) -> - let loc = Node.location node in - (* join values once for the same location and once for the same node *) - let join = Option.some % function None -> v | Some v' -> Spec.D.join v v' in - Hashtbl.modify_opt loc join by_loc; - NodeH.modify_opt node join by_node; - ); + iter (fun (node, v) -> + let loc = match node with + | Statement s -> Cil.get_stmtLoc s.skind (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *) + | FunctionEntry _ | Function _ -> Node.location node + in + (* join values once for the same location and once for the same node *) + let join = Option.some % function None -> v | Some v' -> Spec.D.join v v' in + Hashtbl.modify_opt loc join by_loc; + NodeH.modify_opt node join by_node; + ) node_values; by_loc, by_node in @@ -656,7 +659,10 @@ struct let must_be_uncalled fd = not @@ BatSet.Int.mem fd.svar.vid calledFuns in let skipped_statements from_node edge to_node = - CfgTools.CfgEdgeH.find_default skippedByEdge (from_node, edge, to_node) [] + try + Cfg.skippedByEdge from_node edge to_node + with Not_found -> + [] in Transform.run_transformations file active_transformations @@ -793,22 +799,22 @@ end [analyze_loop] cannot reside in it anymore since each invocation of [get_spec] in the loop might/should return a different module, and we cannot swap the functor parameter from inside [AnalyzeCFG]. *) -let rec analyze_loop (module CFG : CfgBidir) file fs change_info skippedByEdge = +let rec analyze_loop (module CFG : CfgBidirSkip) file fs change_info = try let (module Spec) = get_spec () in let module A = AnalyzeCFG (CFG) (Spec) (struct let increment = change_info end) in - GobConfig.with_immutable_conf (fun () -> A.analyze file fs skippedByEdge) + GobConfig.with_immutable_conf (fun () -> A.analyze file fs) with Refinement.RestartAnalysis -> (* Tail-recursively restart the analysis again, when requested. All solving starts from scratch. Whoever raised the exception should've modified some global state to do a more precise analysis next time. *) (* TODO: do some more incremental refinement and reuse parts of solution *) - analyze_loop (module CFG) file fs change_info skippedByEdge + analyze_loop (module CFG) file fs change_info (** The main function to perform the selected analyses. *) let analyze change_info (file: file) fs = Logs.debug "Generating the control flow graph."; - let (module CFG), skippedByEdge = CfgTools.compute_cfg_skips file in + let (module CFG) = CfgTools.compute_cfg file in MyCFG.current_cfg := (module CFG); - analyze_loop (module CFG) file fs change_info skippedByEdge + analyze_loop (module CFG) file fs change_info diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index c79735c2b1..b1300b628a 100644 --- a/src/incremental/compareAST.ml +++ b/src/incremental/compareAST.ml @@ -339,8 +339,8 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s let eq_block' = fun x y ~(rename_mapping:rename_mapping) -> if cfg_comp then true, rename_mapping else eq_block (x, af) (y, bf) ~rename_mapping in match a, b with | Instr is1, Instr is2 -> forward_list_equal eq_instr is1 is2 ~rename_mapping - | Return (Some exp1, _l1), Return (Some exp2, _l2) -> eq_exp exp1 exp2 ~rename_mapping - | Return (None, _l1), Return (None, _l2) -> true, rename_mapping + | Return (Some exp1, _l1, _el1), Return (Some exp2, _l2, _el2) -> eq_exp exp1 exp2 ~rename_mapping + | Return (None, _l1, _el1), Return (None, _l2, _el2) -> true, rename_mapping | Return _, Return _ -> false, rename_mapping | Goto (st1, _l1), Goto (st2, _l2) -> eq_stmt_with_location (!st1, af) (!st2, bf), rename_mapping | Break _, Break _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true, rename_mapping diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 4b67804bb8..a887d74b5b 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -147,6 +147,8 @@ let check_arguments () = if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load"); if get_bool "exp.basic-blocks" && not (get_bool "justcil") && List.mem "assert" @@ get_string_list "trans.activated" then (set_bool "exp.basic-blocks" false; warn "The option exp.basic-blocks implicitely disabled by activating the \"assert\" tranformation."); if (not @@ get_bool "witness.invariant.all-locals") && (not @@ get_bool "cil.addNestedScopeAttr") then (set_bool "cil.addNestedScopeAttr" true; warn "Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr."); + if (get_int "exp.unrolling-factor" > 0 || AutoTune0.isActivated "loopUnrollHeuristic") && (get_bool "witness.yaml.enabled" || get_string "witness.yaml.validate" <> "" || get_string "witness.yaml.unassume" <> "") then + fail "YAML witnesses are incompatible with syntactic loop unrolling (https://github.com/goblint/analyzer/pull/1370)."; if List.mem "remove_dead_code" @@ get_string_list "trans.activated" then ( (* 'assert' transform happens before 'remove_dead_code' transform *) ignore @@ List.fold_left diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index 0cf59f0c78..88b273ab6d 100644 --- a/src/transform/expressionEvaluation.ml +++ b/src/transform/expressionEvaluation.ml @@ -68,7 +68,7 @@ struct (* Take all statements *) |> List.concat_map (fun (f : Cil.fundec) -> f.sallstmts |> List.map (fun s -> f, s)) (* Add locations *) - |> List.map (fun (f, (s : Cil.stmt)) -> (Cilfacade.get_stmtLoc s, f, s)) + |> List.map (fun (f, (s : Cil.stmt)) -> (Cil.get_stmtLoc s.skind, f, s)) (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *) (* Filter artificial ones by impossible location *) |> List.filter (fun ((l : Cil.location), _, _) -> l.line >= 0) (* Create hash table *) @@ -109,7 +109,7 @@ struct fun (s : Cil.stmt) -> succeeding_statement := Some s; (* Evaluate at (directly before) a succeeding location *) - Some(self#try_ask (Cilfacade.get_stmtLoc s) expression) + Some(self#try_ask (Cil.get_stmtLoc s.skind) expression) (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *) end statement.succs with Not_found -> None diff --git a/src/util/server.ml b/src/util/server.ml index 6f760e6856..6edcf5d69c 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -121,6 +121,10 @@ let serve serv = |> Seq.map Packet.t_of_yojson |> Seq.iter (handle_packet serv) +let is_server_node cfgnode = + let loc = UpdateCil.getLoc cfgnode in + not loc.synthetic + let arg_wrapper: (module ArgWrapper) ResettableLazy.t = ResettableLazy.from_fun (fun () -> let module Arg = (val (Option.get_exn !ArgTools.current_arg Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or arg disabled" ())))) in @@ -133,7 +137,7 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t = Arg.iter_nodes (fun n -> let cfgnode = Arg.Node.cfgnode n in let loc = UpdateCil.getLoc cfgnode in - if not loc.synthetic then + if is_server_node cfgnode then Locator.add locator loc n; StringH.replace ids (Arg.Node.to_string n) n; StringH.add cfg_nodes (Node.show_id cfgnode) n (* add for find_all *) @@ -248,7 +252,7 @@ let node_locator: Locator.t ResettableLazy.t = if not (NH.mem reachable node) then begin NH.replace reachable node (); let loc = UpdateCil.getLoc node in - if not loc.synthetic then + if is_server_node node then Locator.add locator loc node; List.iter (fun (_, prev_node) -> iter_node prev_node @@ -486,7 +490,7 @@ let () = let process { fname } serv = let fundec = Cilfacade.find_name_fundec fname in let live _ = true in (* TODO: fix this *) - let cfg = CfgTools.sprint_fundec_html_dot !MyCFG.current_cfg live fundec in + let cfg = CfgTools.sprint_fundec_html_dot (module (val !MyCFG.current_cfg: MyCFG.CfgBidirSkip): MyCFG.CfgBidir) live fundec in { cfg } end); diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index 6d22a51166..bb887e6cb1 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -7,10 +7,8 @@ module Specification = SvcompSpec module type Task = sig - val file: Cil.file + include MyCFG.FileCfg val specification: Specification.multi - - module Cfg: MyCFG.CfgBidir end let task: (module Task) option ref = ref None diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 12bc598be5..6c02546168 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -79,7 +79,61 @@ struct emit_after_lock else emit_other + + let find_syntactic_loop_head n = + let prevs = Cfg.prev n in + List.find_map (fun (edges, prev) -> + let stmts = Cfg.skippedByEdge prev edges n in + List.find_map (fun s -> + match s.GoblintCil.skind with + | Loop (_, loc, _, _, _) -> Some loc + | _ -> None + ) stmts + ) prevs +end + +module YamlInvariant (FileCfg: MyCFG.FileCfg) = +struct + include Invariant (FileCfg) + + let is_stub_node n = + let fundec = Node.find_fundec n in + Cil.hasAttribute "goblint_stub" fundec.svar.vattr + + let location_location (n : Node.t) = (* great naming... *) + match n with + | Statement s -> + let {loc; _}: CilLocation.locs = CilLocation.get_stmtLoc s in + if not loc.synthetic && is_invariant_node n && not (is_stub_node n) then (* TODO: remove is_invariant_node? *) + Some loc + else + None + | FunctionEntry _ | Function _ -> + (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *) + None + + let is_invariant_node n = Option.is_some (location_location n) + + let loop_location n = + find_syntactic_loop_head n + |> BatOption.filter (fun _loc -> not (is_stub_node n)) + + let is_loop_head_node n = Option.is_some (loop_location n) +end + +module YamlInvariantValidate (FileCfg: MyCFG.FileCfg) = +struct + include Invariant (FileCfg) + + (* TODO: filter synthetic? + + Almost all loops are transformed by CIL, so the loop constructs all get synthetic locations. Filtering them from the locator could give some odd behavior: if the location is right before the loop and all the synthetic loop head stuff is filtered, then the first non-synthetic node is already inside the loop, not outside where the location actually was. + Similarly, if synthetic locations are then filtered, witness.invariant.loop-head becomes essentially useless. + I guess at some point during testing and benchmarking I achieved better results with the filtering removed. *) + + let is_loop_head_node = NH.mem loop_heads end +[@@deprecated] module InvariantExp = struct diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index e04a4c9744..e5234bae4c 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -184,17 +184,28 @@ struct open SpecSys module NH = BatHashtbl.Make (Node) - module WitnessInvariant = WitnessUtil.Invariant (FileCfg) + module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) module FMap = BatHashtbl.Make (CilType.Fundec) module FCMap = BatHashtbl.Make (Printable.Prod (CilType.Fundec) (Spec.C)) type con_inv = {node: Node.t; context: Spec.C.t; invariant: Invariant.t; state: Spec.D.t} (* TODO: fix location hack *) module LH = BatHashtbl.Make (CilType.Location) - let location2nodes: Node.t list LH.t Lazy.t = lazy ( + let location_nodes: Node.t list LH.t Lazy.t = lazy ( let lh = LH.create 113 in NH.iter (fun n _ -> - LH.modify_def [] (Node.location n) (List.cons n) lh + Option.iter (fun loc -> + LH.modify_def [] loc (List.cons n) lh + ) (WitnessInvariant.location_location n) + ) (Lazy.force nh); + lh + ) + let loop_nodes: Node.t list LH.t Lazy.t = lazy ( + let lh = LH.create 113 in + NH.iter (fun n _ -> + Option.iter (fun loc -> + LH.modify_def [] loc (List.cons n) lh + ) (WitnessInvariant.loop_location n) ) (Lazy.force nh); lh ) @@ -212,25 +223,6 @@ struct in let task = Entry.task ~input_files ~data_model ~specification in - let is_stub_node n = - let fundec = Node.find_fundec n in - Cil.hasAttribute "goblint_stub" fundec.svar.vattr - in - - let is_invariant_node (n : Node.t) = - let loc = Node.location n in - match n with - | Statement _ -> - not loc.synthetic && WitnessInvariant.is_invariant_node n && not (is_stub_node n) - | FunctionEntry _ | Function _ -> - (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *) - false - in - - let is_loop_head_node n = - WitnessUtil.NH.mem WitnessInvariant.loop_heads n && not (is_stub_node n) - in - let local_lvals n local = if GobConfig.get_bool "witness.invariant.accessed" then ( match R.ask_local_node n ~local MayAccessed with @@ -273,30 +265,26 @@ struct let entries = if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then ( LH.fold (fun loc ns acc -> - if List.exists is_invariant_node ns then ( - let inv = List.fold_left (fun acc n -> - let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in - let lvals = local_lvals n local in - Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) - ) (Invariant.bot ()) ns - in - match inv with - | `Lifted inv -> - let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) - let location_function = fundec.svar.vname in - let location = Entry.location ~location:loc ~location_function in - let invs = WitnessUtil.InvariantExp.process_exp inv in - List.fold_left (fun acc inv -> - let invariant = Entry.invariant (CilType.Exp.show inv) in - let entry = Entry.location_invariant ~task ~location ~invariant in - entry :: acc - ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) - acc - ) - else + let inv = List.fold_left (fun acc n -> + let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in + let lvals = local_lvals n local in + Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) + ) (Invariant.bot ()) ns + in + match inv with + | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let invariant = Entry.invariant (CilType.Exp.show inv) in + let entry = Entry.location_invariant ~task ~location ~invariant in + entry :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) acc - ) (Lazy.force location2nodes) entries + ) (Lazy.force location_nodes) entries ) else entries @@ -306,7 +294,7 @@ struct let entries = if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then ( LH.fold (fun loc ns acc -> - if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then ( + if WitnessInvariant.emit_loop_head then ( (* TODO: remove double condition? *) let inv = List.fold_left (fun acc n -> let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) @@ -328,7 +316,7 @@ struct ) else acc - ) (Lazy.force location2nodes) entries + ) (Lazy.force loop_nodes) entries ) else entries @@ -384,11 +372,11 @@ struct entries in - (* Generate precondition invariants. + (* Generate precondition loop invariants. We do this in three steps: 1. Collect contexts for each function 2. For each function context, find "matching"/"weaker" contexts that may satisfy its invariant - 3. Generate precondition invariants. The postcondition is a disjunction over the invariants for matching states. *) + 3. Generate precondition loop invariants. The postcondition is a disjunction over the invariants for matching states. *) let entries = if entry_type_enabled YamlWitnessType.PreconditionLoopInvariant.entry_type then ( (* 1. Collect contexts for each function *) @@ -436,47 +424,47 @@ struct (* 3. Generate precondition invariants *) LHT.fold (fun ((n, c) as lvar) local acc -> - if is_invariant_node n then ( + match WitnessInvariant.loop_location n with + | Some loc -> let fundec = Node.find_fundec n in let pre_lvar = (Node.FunctionEntry fundec, c) in let query = Queries.Invariant Invariant.default_context in - match R.ask_local pre_lvar query with - | `Lifted c_inv -> - let loc = Node.location n in - (* Find unknowns for which the preceding start state satisfies the precondtion *) - let xs = find_matching_states lvar in - - (* Generate invariants. Give up in case one invariant could not be generated. *) - let invs = GobList.fold_while_some (fun acc local -> - let lvals = local_lvals n local in - match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with - | `Lifted c -> Some ((`Lifted c)::acc) - | `Bot | `Top -> None - ) [] xs - in - begin match invs with - | None - | Some [] -> acc - | Some (x::xs) -> - begin match List.fold_left (fun acc inv -> Invariant.(acc || inv) [@coverage off]) x xs with (* bisect_ppx cannot handle redefined (||) *) - | `Lifted inv -> - let invs = WitnessUtil.InvariantExp.process_exp inv in - let c_inv = InvariantCil.exp_replace_original_name c_inv in (* cannot be split *) - List.fold_left (fun acc inv -> - let location_function = (Node.find_fundec n).svar.vname in - let location = Entry.location ~location:loc ~location_function in - let precondition = Entry.invariant (CilType.Exp.show c_inv) in - let invariant = Entry.invariant (CilType.Exp.show inv) in - let entry = Entry.precondition_loop_invariant ~task ~location ~precondition ~invariant in - entry :: acc - ) acc invs - | `Bot | `Top -> acc - end - end - | _ -> (* Do not construct precondition invariants if we cannot express precondition *) - acc - ) - else + begin match R.ask_local pre_lvar query with + | `Lifted c_inv -> + (* Find unknowns for which the preceding start state satisfies the precondtion *) + let xs = find_matching_states lvar in + + (* Generate invariants. Give up in case one invariant could not be generated. *) + let invs = GobList.fold_while_some (fun acc local -> + let lvals = local_lvals n local in + match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with + | `Lifted c -> Some ((`Lifted c)::acc) + | `Bot | `Top -> None + ) [] xs + in + begin match invs with + | None + | Some [] -> acc + | Some (x::xs) -> + begin match List.fold_left (fun acc inv -> Invariant.(acc || inv) [@coverage off]) x xs with (* bisect_ppx cannot handle redefined (||) *) + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + let c_inv = InvariantCil.exp_replace_original_name c_inv in (* cannot be split *) + List.fold_left (fun acc inv -> + let location_function = (Node.find_fundec n).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let precondition = Entry.invariant (CilType.Exp.show c_inv) in + let invariant = Entry.invariant (CilType.Exp.show inv) in + let entry = Entry.precondition_loop_invariant ~task ~location ~precondition ~invariant in + entry :: acc + ) acc invs + | `Bot | `Top -> acc + end + end + | _ -> (* Do not construct precondition invariants if we cannot express precondition *) + acc + end + | None -> acc ) lh entries ) @@ -493,30 +481,26 @@ struct let invariants = if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then ( LH.fold (fun loc ns acc -> - if List.exists is_invariant_node ns then ( - let inv = List.fold_left (fun acc n -> - let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in - let lvals = local_lvals n local in - Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) - ) (Invariant.bot ()) ns - in - match inv with - | `Lifted inv -> - let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) - let location_function = fundec.svar.vname in - let location = Entry.location ~location:loc ~location_function in - let invs = WitnessUtil.InvariantExp.process_exp inv in - List.fold_left (fun acc inv -> - let invariant = CilType.Exp.show inv in - let invariant = Entry.location_invariant' ~location ~invariant in - invariant :: acc - ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) - acc - ) - else + let inv = List.fold_left (fun acc n -> + let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in + let lvals = local_lvals n local in + Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) + ) (Invariant.bot ()) ns + in + match inv with + | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let invariant = CilType.Exp.show inv in + let invariant = Entry.location_invariant' ~location ~invariant in + invariant :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) acc - ) (Lazy.force location2nodes) invariants + ) (Lazy.force location_nodes) invariants ) else invariants @@ -526,7 +510,7 @@ struct let invariants = if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( LH.fold (fun loc ns acc -> - if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then ( + if WitnessInvariant.emit_loop_head then ( (* TODO: remove double condition? *) let inv = List.fold_left (fun acc n -> let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) @@ -548,7 +532,7 @@ struct ) else acc - ) (Lazy.force location2nodes) invariants + ) (Lazy.force loop_nodes) invariants ) else invariants @@ -609,7 +593,7 @@ struct module Locator = WitnessUtil.Locator (EQSys.LVar) module LvarS = Locator.ES - module WitnessInvariant = WitnessUtil.Invariant (FileCfg) + module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) module InvariantParser = WitnessUtil.InvariantParser module VR = ValidationResult @@ -625,19 +609,16 @@ struct } let validate () = - let locator = Locator.create () in + let location_locator = Locator.create () in let loop_locator = Locator.create () in + (* TODO: add all CFG nodes, not just live ones from lh, like UnassumeAnalysis *) LHT.iter (fun ((n, _) as lvar) _ -> - let loc = Node.location n in - (* TODO: filter synthetic? - - Almost all loops are transformed by CIL, so the loop constructs all get synthetic locations. Filtering them from the locator could give some odd behavior: if the location is right before the loop and all the synthetic loop head stuff is filtered, then the first non-synthetic node is already inside the loop, not outside where the location actually was. - Similarly, if synthetic locations are then filtered, witness.invariant.loop-head becomes essentially useless. - I guess at some point during testing and benchmarking I achieved better results with the filtering removed. *) - if WitnessInvariant.is_invariant_node n then - Locator.add locator loc lvar; - if WitnessUtil.NH.mem WitnessInvariant.loop_heads n then - Locator.add loop_locator loc lvar + Option.iter (fun loc -> + Locator.add location_locator loc lvar + ) (WitnessInvariant.location_location n); + Option.iter (fun loc -> + Locator.add loop_locator loc lvar + ) (WitnessInvariant.loop_location n) ) lh; let inv_parser = InvariantParser.create FileCfg.file in @@ -731,7 +712,7 @@ struct None in - match Locator.find_opt locator loc with + match Locator.find_opt location_locator loc with | Some lvars -> validate_lvars_invariant ~entry_certificate ~loc ~lvars inv | None -> @@ -771,7 +752,7 @@ struct in let msgLoc: M.Location.t = CilLocation loc in - match Locator.find_opt locator loc with + match Locator.find_opt loop_locator loc with | Some lvars -> begin match InvariantParser.parse_cabs pre with | Ok pre_cabs -> @@ -822,7 +803,7 @@ struct let loc = loc_of_location location_invariant.location in let inv = location_invariant.value in - match Locator.find_opt locator loc with + match Locator.find_opt location_locator loc with | Some lvars -> ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv) | None -> diff --git a/tests/regression/00-sanity/19-if-0.t b/tests/regression/00-sanity/19-if-0.t index f847d75446..9f856c43fc 100644 --- a/tests/regression/00-sanity/19-if-0.t +++ b/tests/regression/00-sanity/19-if-0.t @@ -1,33 +1,39 @@ $ cfgDot 19-if-0.c $ graph-easy --as=boxart main.dot - ┌────────────────────────┐ - │ main() │ - └────────────────────────┘ - │ - │ (body) - ▼ - ┌────────────────────────┐ ┌────────────────────────┐ - │ 19-if-0.c:15:9-15:27 │ Neg(0) │ 19-if-0.c:9:5-16:5 │ - │ (19-if-0.c:15:9-15:27) │ ◀──────────────────── │ (19-if-0.c:9:9-9:10) │ - └────────────────────────┘ └────────────────────────┘ - │ │ - │ │ Pos(0) - │ ▼ - │ ┌────────────────────────┐ - │ │ 19-if-0.c:11:9-11:16 │ - │ │ (19-if-0.c:11:9-11:16) │ - │ └────────────────────────┘ - │ │ - │ │ stuff() - │ ▼ - │ ┌────────────────────────┐ - │ __goblint_check(1) │ 19-if-0.c:17:5-17:13 │ - └────────────────────────────────────────────▶ │ (unknown) │ - └────────────────────────┘ - │ - │ return 0 - ▼ - ┌────────────────────────┐ - │ return of main() │ - └────────────────────────┘ + ┌────────────────────────────────┐ + │ main() │ + └────────────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────────────┐ ┌────────────────────────────────┐ + │ 19-if-0.c:15:9-15:27 │ │ 19-if-0.c:9:5-16:5 │ + │ (19-if-0.c:15:9-15:27) │ │ (19-if-0.c:9:9-9:10) │ + │ YAML loc: 19-if-0.c:15:9-15:27 │ Neg(0) │ YAML loc: 19-if-0.c:9:5-16:5 │ + │ GraphML: true; server: true │ ◀──────────────────── │ GraphML: true; server: true │ + └────────────────────────────────┘ └────────────────────────────────┘ + │ │ + │ │ Pos(0) + │ ▼ + │ ┌────────────────────────────────┐ + │ │ 19-if-0.c:11:9-11:16 │ + │ │ (19-if-0.c:11:9-11:16) │ + │ │ YAML loc: 19-if-0.c:11:9-11:16 │ + │ │ GraphML: true; server: true │ + │ └────────────────────────────────┘ + │ │ + │ │ stuff() + │ ▼ + │ ┌────────────────────────────────┐ + │ │ 19-if-0.c:17:5-17:13 │ + │ │ (19-if-0.c:17:12-17:13) │ + │ __goblint_check(1) │ YAML loc: 19-if-0.c:17:5-17:13 │ + └────────────────────────────────────────────────────▶ │ GraphML: true; server: true │ + └────────────────────────────────┘ + │ + │ return 0 + ▼ + ┌────────────────────────────────┐ + │ return of main() │ + └────────────────────────────────┘ diff --git a/tests/regression/00-sanity/20-if-0-realnode.t b/tests/regression/00-sanity/20-if-0-realnode.t index 06a0bba865..32f06ecdd4 100644 --- a/tests/regression/00-sanity/20-if-0-realnode.t +++ b/tests/regression/00-sanity/20-if-0-realnode.t @@ -1,35 +1,41 @@ $ cfgDot 20-if-0-realnode.c $ graph-easy --as=boxart main.dot - ┌─────────────────────────────────┐ - │ main() │ - └─────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ main() │ + └─────────────────────────────────────────┘ │ │ (body) ▼ - ┌─────────────────────────────────┐ - │ 20-if-0-realnode.c:8:5-14:5 │ Neg(0) - │ (20-if-0-realnode.c:8:9-8:10) │ ─────────┐ - │ [20-if-0-realnode.c:7:5-8:5 │ │ - │ (unknown)] │ ◀────────┘ - └─────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ 20-if-0-realnode.c:8:5-14:5 │ + │ (20-if-0-realnode.c:8:9-8:10) │ + │ [20-if-0-realnode.c:7:5-8:5 │ Neg(0) + │ (unknown)] │ ─────────┐ + │ YAML loc: 20-if-0-realnode.c:8:5-14:5 │ │ + │ GraphML: true; server: true │ ◀────────┘ + └─────────────────────────────────────────┘ │ │ Pos(0) ▼ - ┌─────────────────────────────────┐ - │ 20-if-0-realnode.c:10:9-10:16 │ - │ (20-if-0-realnode.c:10:9-10:16) │ - └─────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ 20-if-0-realnode.c:10:9-10:16 │ + │ (20-if-0-realnode.c:10:9-10:16) │ + │ YAML loc: 20-if-0-realnode.c:10:9-10:16 │ + │ GraphML: true; server: true │ + └─────────────────────────────────────────┘ │ │ stuff() ▼ - ┌─────────────────────────────────┐ - │ 20-if-0-realnode.c:15:5-15:13 │ - │ (unknown) │ - └─────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ 20-if-0-realnode.c:15:5-15:13 │ + │ (20-if-0-realnode.c:15:12-15:13) │ + │ YAML loc: 20-if-0-realnode.c:15:5-15:13 │ + │ GraphML: true; server: true │ + └─────────────────────────────────────────┘ │ │ return 0 ▼ - ┌─────────────────────────────────┐ - │ return of main() │ - └─────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ return of main() │ + └─────────────────────────────────────────┘ diff --git a/tests/regression/00-sanity/21-empty-loops.t b/tests/regression/00-sanity/21-empty-loops.t index 202a4d1071..932a21f049 100644 --- a/tests/regression/00-sanity/21-empty-loops.t +++ b/tests/regression/00-sanity/21-empty-loops.t @@ -1,31 +1,35 @@ $ cfgDot 21-empty-loops.c $ graph-easy --as=boxart f_empty_goto_loop.dot - ┌───────────────────────────────┐ - │ f_empty_goto_loop() │ - └───────────────────────────────┘ + ┌───────────────────────────────────────┐ + │ f_empty_goto_loop() │ + └───────────────────────────────────────┘ │ │ (body) ▼ - ┌───────────────────────────────┐ - │ 21-empty-loops.c:57:3-57:31 │ skip - │ (unknown) │ ───────┐ - │ [21-empty-loops.c:56:1-57:3 │ │ - │ (unknown)] │ ◀──────┘ - └───────────────────────────────┘ + ┌───────────────────────────────────────┐ + │ 21-empty-loops.c:57:3-57:31 │ + │ (unknown) │ + │ [21-empty-loops.c:56:1-57:3 │ skip + │ (unknown)] │ ───────┐ + │ YAML loc: 21-empty-loops.c:57:3-57:31 │ │ + │ GraphML: true; server: true │ ◀──────┘ + └───────────────────────────────────────┘ │ │ Neg(1) ▼ - ┌───────────────────────────────┐ - │ 21-empty-loops.c:58:1-58:1 │ - │ (unknown) │ - └───────────────────────────────┘ + ┌───────────────────────────────────────┐ + │ 21-empty-loops.c:58:1-58:1 │ + │ (unknown) │ + │ YAML loc: 21-empty-loops.c:58:1-58:1 │ + │ GraphML: true; server: true │ + └───────────────────────────────────────┘ │ │ return ▼ - ┌───────────────────────────────┐ - │ return of f_empty_goto_loop() │ - └───────────────────────────────┘ + ┌───────────────────────────────────────┐ + │ return of f_empty_goto_loop() │ + └───────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_while_loop.dot ┌────────────────────────────────────────────┐ @@ -34,10 +38,12 @@ │ │ (body) ▼ - ┌────────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:62:3-62:14 (synthetic) │ ─────────┐ - │ (21-empty-loops.c:62:10-62:11 (synthetic)) │ │ - │ │ ◀────────┘ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:62:3-62:14 (synthetic) │ + │ (21-empty-loops.c:62:10-62:11 (synthetic)) │ Pos(1) + │ YAML loop: 21-empty-loops.c:62:3-62:14 │ ─────────┐ + │ GraphML: true; server: false │ │ + │ loop: 21-empty-loops.c:62:3-62:14 │ ◀────────┘ └────────────────────────────────────────────┘ │ │ Neg(1) @@ -45,6 +51,8 @@ ┌────────────────────────────────────────────┐ │ 21-empty-loops.c:63:1-63:1 │ │ (unknown) │ + │ YAML loc: 21-empty-loops.c:63:1-63:1 │ + │ GraphML: true; server: true │ └────────────────────────────────────────────┘ │ │ return @@ -54,35 +62,41 @@ └────────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_goto_loop_suffix.dot - ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:75:3-75:11 │ - │ (21-empty-loops.c:75:3-75:11) │ - └──────────────────────────────────────┘ + ┌───────────────────────────────────────┐ + │ 21-empty-loops.c:75:3-75:11 │ + │ (21-empty-loops.c:75:3-75:11) │ + │ YAML loc: 21-empty-loops.c:75:3-75:11 │ + │ GraphML: true; server: true │ + └───────────────────────────────────────┘ │ │ suffix() ▼ - ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:76:1-76:1 │ - │ (unknown) │ ◀┐ - └──────────────────────────────────────┘ │ - │ │ - │ return │ - ▼ │ - ┌──────────────────────────────────────┐ │ - │ return of f_empty_goto_loop_suffix() │ │ - └──────────────────────────────────────┘ │ - ┌──────────────────────────────────────┐ │ Neg(1) - │ f_empty_goto_loop_suffix() │ │ - └──────────────────────────────────────┘ │ - │ │ - │ (body) │ - ▼ │ - ┌──────────────────────────────────────┐ │ - skip │ 21-empty-loops.c:73:3-73:38 │ │ - ┌─────── │ (unknown) │ │ - │ │ [21-empty-loops.c:72:1-73:3 │ │ - └──────▶ │ (unknown)] │ ─┘ - └──────────────────────────────────────┘ + ┌───────────────────────────────────────┐ + │ 21-empty-loops.c:76:1-76:1 │ + │ (unknown) │ + │ YAML loc: 21-empty-loops.c:76:1-76:1 │ + │ GraphML: true; server: true │ ◀┐ + └───────────────────────────────────────┘ │ + │ │ + │ return │ + ▼ │ + ┌───────────────────────────────────────┐ │ + │ return of f_empty_goto_loop_suffix() │ │ + └───────────────────────────────────────┘ │ + ┌───────────────────────────────────────┐ │ Neg(1) + │ f_empty_goto_loop_suffix() │ │ + └───────────────────────────────────────┘ │ + │ │ + │ (body) │ + ▼ │ + ┌───────────────────────────────────────┐ │ + │ 21-empty-loops.c:73:3-73:38 │ │ + │ (unknown) │ │ + skip │ [21-empty-loops.c:72:1-73:3 │ │ + ┌─────── │ (unknown)] │ │ + │ │ YAML loc: 21-empty-loops.c:73:3-73:38 │ │ + └──────▶ │ GraphML: true; server: true │ ─┘ + └───────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_while_loop_suffix.dot ┌────────────────────────────────────────────┐ @@ -91,10 +105,12 @@ │ │ (body) ▼ - ┌────────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:80:3-80:14 (synthetic) │ ─────────┐ - │ (21-empty-loops.c:80:10-80:11 (synthetic)) │ │ - │ │ ◀────────┘ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:80:3-80:14 (synthetic) │ + │ (21-empty-loops.c:80:10-80:11 (synthetic)) │ Pos(1) + │ YAML loop: 21-empty-loops.c:80:3-80:14 │ ─────────┐ + │ GraphML: true; server: false │ │ + │ loop: 21-empty-loops.c:80:3-80:14 │ ◀────────┘ └────────────────────────────────────────────┘ │ │ Neg(1) @@ -102,6 +118,8 @@ ┌────────────────────────────────────────────┐ │ 21-empty-loops.c:82:3-82:11 │ │ (21-empty-loops.c:82:3-82:11) │ + │ YAML loc: 21-empty-loops.c:82:3-82:11 │ + │ GraphML: true; server: true │ └────────────────────────────────────────────┘ │ │ suffix() @@ -109,6 +127,8 @@ ┌────────────────────────────────────────────┐ │ 21-empty-loops.c:83:1-83:1 │ │ (unknown) │ + │ YAML loc: 21-empty-loops.c:83:1-83:1 │ + │ GraphML: true; server: true │ └────────────────────────────────────────────┘ │ │ return @@ -118,93 +138,107 @@ └────────────────────────────────────────────┘ $ graph-easy --as=boxart f_nonempty_goto_loop.dot - ┌──────────────────────────────────┐ - │ f_nonempty_goto_loop() │ - └──────────────────────────────────┘ + ┌──────────────────────────────────────┐ + │ f_nonempty_goto_loop() │ + └──────────────────────────────────────┘ │ │ (body) ▼ - ┌──────────────────────────────────┐ body() - │ 21-empty-loops.c:93:3-93:9 │ ─────────┐ - │ (21-empty-loops.c:93:3-93:9) │ │ - │ │ ◀────────┘ - └──────────────────────────────────┘ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:93:3-93:9 │ body() + │ (21-empty-loops.c:93:3-93:9) │ ─────────┐ + │ YAML loc: 21-empty-loops.c:93:3-93:9 │ │ + │ GraphML: true; server: true │ ◀────────┘ + └──────────────────────────────────────┘ │ │ Neg(1) ▼ - ┌──────────────────────────────────┐ - │ 21-empty-loops.c:95:1-95:1 │ - │ (unknown) │ - └──────────────────────────────────┘ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:95:1-95:1 │ + │ (unknown) │ + │ YAML loc: 21-empty-loops.c:95:1-95:1 │ + │ GraphML: true; server: true │ + └──────────────────────────────────────┘ │ │ return ▼ - ┌──────────────────────────────────┐ - │ return of f_nonempty_goto_loop() │ - └──────────────────────────────────┘ + ┌──────────────────────────────────────┐ + │ return of f_nonempty_goto_loop() │ + └──────────────────────────────────────┘ $ graph-easy --as=boxart f_nonempty_while_loop.dot - ┌───────────────────────────────────────────────────────────────────────────────────────────┐ - │ │ - │ ┌────────────────────────────────────────────┐ │ - │ │ f_nonempty_while_loop() │ │ - │ └────────────────────────────────────────────┘ │ - │ │ │ body() - │ │ (body) │ - │ ▼ │ - ┌─────────────────────────────────┐ ┌────────────────────────────────────────────┐ │ - │ 21-empty-loops.c:101:5-101:11 │ Pos(1) │ 21-empty-loops.c:99:3-102:3 (synthetic) │ │ - │ (21-empty-loops.c:101:5-101:11) │ ◀──────── │ (21-empty-loops.c:99:10-99:11 (synthetic)) │ ◀┘ - └─────────────────────────────────┘ └────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌────────────────────────────────────────────┐ - │ 21-empty-loops.c:103:1-103:1 │ - │ (unknown) │ - └────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌────────────────────────────────────────────┐ - │ return of f_nonempty_while_loop() │ - └────────────────────────────────────────────┘ + ┌───────────────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌────────────────────────────────────────────┐ │ + │ │ f_nonempty_while_loop() │ │ + │ └────────────────────────────────────────────┘ │ + │ │ │ body() + │ │ (body) │ + │ ▼ │ + ┌─────────────────────────────────────────┐ ┌────────────────────────────────────────────┐ │ + │ 21-empty-loops.c:101:5-101:11 │ │ 21-empty-loops.c:99:3-102:3 (synthetic) │ │ + │ (21-empty-loops.c:101:5-101:11) │ │ (21-empty-loops.c:99:10-99:11 (synthetic)) │ │ + │ YAML loc: 21-empty-loops.c:101:5-101:11 │ │ YAML loop: 21-empty-loops.c:99:3-102:3 │ │ + │ GraphML: true; server: true │ Pos(1) │ GraphML: true; server: false │ │ + │ │ ◀──────── │ loop: 21-empty-loops.c:99:3-102:3 │ ◀┘ + └─────────────────────────────────────────┘ └────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:103:1-103:1 │ + │ (unknown) │ + │ YAML loc: 21-empty-loops.c:103:1-103:1 │ + │ GraphML: true; server: true │ + └────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────────┐ + │ return of f_nonempty_while_loop() │ + └────────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_goto_loop_prefix.dot - ┌──────────────────────────────────────┐ - │ f_empty_goto_loop_prefix() │ - └──────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ f_empty_goto_loop_prefix() │ + └─────────────────────────────────────────┘ │ │ (body) ▼ - ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:112:3-112:11 │ - │ (21-empty-loops.c:112:3-112:11) │ - └──────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ 21-empty-loops.c:112:3-112:11 │ + │ (21-empty-loops.c:112:3-112:11) │ + │ YAML loc: 21-empty-loops.c:112:3-112:11 │ + │ GraphML: true; server: true │ + └─────────────────────────────────────────┘ │ │ prefix() ▼ - ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:115:3-115:38 │ skip - │ (unknown) │ ───────┐ - │ [21-empty-loops.c:114:1-115:3 │ │ - │ (unknown)] │ ◀──────┘ - └──────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ 21-empty-loops.c:115:3-115:38 │ + │ (unknown) │ + │ [21-empty-loops.c:114:1-115:3 │ skip + │ (unknown)] │ ───────┐ + │ YAML loc: 21-empty-loops.c:115:3-115:38 │ │ + │ GraphML: true; server: true │ ◀──────┘ + └─────────────────────────────────────────┘ │ │ Neg(1) ▼ - ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:116:1-116:1 │ - │ (unknown) │ - └──────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ 21-empty-loops.c:116:1-116:1 │ + │ (unknown) │ + │ YAML loc: 21-empty-loops.c:116:1-116:1 │ + │ GraphML: true; server: true │ + └─────────────────────────────────────────┘ │ │ return ▼ - ┌──────────────────────────────────────┐ - │ return of f_empty_goto_loop_prefix() │ - └──────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ return of f_empty_goto_loop_prefix() │ + └─────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_while_loop_prefix.dot ┌──────────────────────────────────────────────┐ @@ -216,14 +250,18 @@ ┌──────────────────────────────────────────────┐ │ 21-empty-loops.c:120:3-120:11 │ │ (21-empty-loops.c:120:3-120:11) │ + │ YAML loc: 21-empty-loops.c:120:3-120:11 │ + │ GraphML: true; server: true │ └──────────────────────────────────────────────┘ │ │ prefix() ▼ - ┌──────────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:122:3-122:14 (synthetic) │ ─────────┐ - │ (21-empty-loops.c:122:10-122:11 (synthetic)) │ │ - │ │ ◀────────┘ + ┌──────────────────────────────────────────────┐ + │ 21-empty-loops.c:122:3-122:14 (synthetic) │ + │ (21-empty-loops.c:122:10-122:11 (synthetic)) │ Pos(1) + │ YAML loop: 21-empty-loops.c:122:3-122:14 │ ─────────┐ + │ GraphML: true; server: false │ │ + │ loop: 21-empty-loops.c:122:3-122:14 │ ◀────────┘ └──────────────────────────────────────────────┘ │ │ Neg(1) @@ -231,6 +269,8 @@ ┌──────────────────────────────────────────────┐ │ 21-empty-loops.c:123:1-123:1 │ │ (unknown) │ + │ YAML loc: 21-empty-loops.c:123:1-123:1 │ + │ GraphML: true; server: true │ └──────────────────────────────────────────────┘ │ │ return @@ -247,10 +287,11 @@ │ (body) ▼ ┌─────────────────────────────────────────┐ - │ unknown │ skip - │ (unknown) │ ───────┐ - │ [21-empty-loops.c:127:1-128:3 │ │ - │ (unknown)] │ ◀──────┘ + │ unknown │ + │ (unknown) │ skip + │ [21-empty-loops.c:127:1-128:3 │ ───────┐ + │ (unknown)] │ │ + │ GraphML: true; server: true │ ◀──────┘ └─────────────────────────────────────────┘ │ │ Neg(1) @@ -258,6 +299,8 @@ ┌─────────────────────────────────────────┐ │ 21-empty-loops.c:131:1-131:1 │ │ (unknown) │ + │ YAML loc: 21-empty-loops.c:131:1-131:1 │ + │ GraphML: true; server: true │ └─────────────────────────────────────────┘ │ │ return @@ -273,10 +316,12 @@ │ │ (body) ▼ - ┌──────────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:135:3-137:3 (synthetic) │ ─────────┐ - │ (21-empty-loops.c:135:10-135:11 (synthetic)) │ │ - │ │ ◀────────┘ + ┌──────────────────────────────────────────────┐ + │ 21-empty-loops.c:135:3-137:3 (synthetic) │ + │ (21-empty-loops.c:135:10-135:11 (synthetic)) │ Pos(1) + │ YAML loop: 21-empty-loops.c:135:3-137:3 │ ─────────┐ + │ GraphML: true; server: false │ │ + │ loop: 21-empty-loops.c:135:3-137:3 │ ◀────────┘ └──────────────────────────────────────────────┘ │ │ Neg(1) @@ -284,6 +329,8 @@ ┌──────────────────────────────────────────────┐ │ 21-empty-loops.c:138:1-138:1 │ │ (unknown) │ + │ YAML loc: 21-empty-loops.c:138:1-138:1 │ + │ GraphML: true; server: true │ └──────────────────────────────────────────────┘ │ │ return @@ -293,31 +340,35 @@ └──────────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_goto_loop_multiple.dot - ┌────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple() │ - └────────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple() │ + └─────────────────────────────────────────┘ │ │ (body) ▼ - ┌────────────────────────────────────────┐ - │ 21-empty-loops.c:143:3-143:42 │ skip - │ (unknown) │ ───────┐ - │ [21-empty-loops.c:142:1-143:3 │ │ - │ (unknown)] │ ◀──────┘ - └────────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ 21-empty-loops.c:143:3-143:42 │ + │ (unknown) │ + │ [21-empty-loops.c:142:1-143:3 │ skip + │ (unknown)] │ ───────┐ + │ YAML loc: 21-empty-loops.c:143:3-143:42 │ │ + │ GraphML: true; server: true │ ◀──────┘ + └─────────────────────────────────────────┘ │ │ Neg(1) ▼ - ┌────────────────────────────────────────┐ - │ 21-empty-loops.c:146:1-146:1 │ - │ (unknown) │ - └────────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ 21-empty-loops.c:146:1-146:1 │ + │ (unknown) │ + │ YAML loc: 21-empty-loops.c:146:1-146:1 │ + │ GraphML: true; server: true │ + └─────────────────────────────────────────┘ │ │ return ▼ - ┌────────────────────────────────────────┐ - │ return of f_empty_goto_loop_multiple() │ - └────────────────────────────────────────┘ + ┌─────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple() │ + └─────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_first.dot ┌────────────────────────────────────────────────────────┐ @@ -327,10 +378,11 @@ │ (body) ▼ ┌────────────────────────────────────────────────────────┐ - │ unknown │ skip - │ (unknown) │ ───────┐ - │ [21-empty-loops.c:150:1-151:3 │ │ - │ (unknown)] │ ◀──────┘ + │ unknown │ + │ (unknown) │ skip + │ [21-empty-loops.c:150:1-151:3 │ ───────┐ + │ (unknown)] │ │ + │ GraphML: true; server: true │ ◀──────┘ └────────────────────────────────────────────────────────┘ │ │ Neg(1) @@ -338,6 +390,8 @@ ┌────────────────────────────────────────────────────────┐ │ 21-empty-loops.c:155:1-155:1 │ │ (unknown) │ + │ YAML loc: 21-empty-loops.c:155:1-155:1 │ + │ GraphML: true; server: true │ └────────────────────────────────────────────────────────┘ │ │ return @@ -354,10 +408,12 @@ │ (body) ▼ ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:160:3-160:59 │ skip - │ (unknown) │ ───────┐ - │ [21-empty-loops.c:159:1-160:3 │ │ - │ (unknown)] │ ◀──────┘ + │ 21-empty-loops.c:160:3-160:59 │ + │ (unknown) │ + │ [21-empty-loops.c:159:1-160:3 │ skip + │ (unknown)] │ ───────┐ + │ YAML loc: 21-empty-loops.c:160:3-160:59 │ │ + │ GraphML: true; server: true │ ◀──────┘ └─────────────────────────────────────────────────────────┘ │ │ Neg(1) @@ -365,6 +421,8 @@ ┌─────────────────────────────────────────────────────────┐ │ 21-empty-loops.c:164:1-164:1 │ │ (unknown) │ + │ YAML loc: 21-empty-loops.c:164:1-164:1 │ + │ GraphML: true; server: true │ └─────────────────────────────────────────────────────────┘ │ │ return @@ -381,10 +439,11 @@ │ (body) ▼ ┌───────────────────────────────────────────────────────┐ - │ unknown │ skip - │ (unknown) │ ───────┐ - │ [21-empty-loops.c:168:1-169:3 │ │ - │ (unknown)] │ ◀──────┘ + │ unknown │ + │ (unknown) │ skip + │ [21-empty-loops.c:168:1-169:3 │ ───────┐ + │ (unknown)] │ │ + │ GraphML: true; server: true │ ◀──────┘ └───────────────────────────────────────────────────────┘ │ │ Neg(1) @@ -392,6 +451,8 @@ ┌───────────────────────────────────────────────────────┐ │ 21-empty-loops.c:174:1-174:1 │ │ (unknown) │ + │ YAML loc: 21-empty-loops.c:174:1-174:1 │ + │ GraphML: true; server: true │ └───────────────────────────────────────────────────────┘ │ │ return diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c new file mode 100644 index 0000000000..39e3cbce49 --- /dev/null +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c @@ -0,0 +1,6 @@ +int main() { + int i = 0; + while (i < 10) + i++; + return 0; +} diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t new file mode 100644 index 0000000000..b154f8f57a --- /dev/null +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -0,0 +1,9 @@ +Suppress backtrace with code locations, especially for CI. + $ export OCAMLRUNPARAM=b=0 + + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' 11-unrolled-loop-invariant.c + [Error] YAML witnesses are incompatible with syntactic loop unrolling (https://github.com/goblint/analyzer/pull/1370). + Fatal error: exception Failure("Option error") + [2] + +TODO: Fix loop unrolling with YAML witnesses: https://github.com/goblint/analyzer/pull/1370 diff --git a/tests/regression/56-witness/05-prec-problem.c b/tests/regression/56-witness/05-prec-problem.c index 132ba6b466..08c665ce12 100644 --- a/tests/regression/56-witness/05-prec-problem.c +++ b/tests/regression/56-witness/05-prec-problem.c @@ -1,4 +1,4 @@ -//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types[+] precondition_loop_invariant +//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]' #include #include @@ -9,7 +9,8 @@ int foo(int* ptr1, int* ptr2){ } else { result = 1; } - // Look at the generated witness.yml to check whether there are contradictory precondition_loop_invariant[s] + + while (0); // cram test checks for precondition invariant soundness return result; } diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t new file mode 100644 index 0000000000..4c7dd02fa9 --- /dev/null +++ b/tests/regression/56-witness/05-prec-problem.t @@ -0,0 +1,62 @@ + $ goblint --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]' 05-prec-problem.c + [Success][Assert] Assertion "y != z" will succeed (05-prec-problem.c:22:5-22:28) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 13 + dead: 0 + 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: + total generation entries: 6 + +TODO: Don't generate duplicate entries from each context: should have generated just 3. + +Witness shouldn't contain two unsound precondition_loop_invariant-s with precondition `*ptr1 == 5 && *ptr2 == 5`, +and separately invariants `result == 0` and `result == 1`. +The sound invariant is `result == 1 || result == 0`. + + $ yamlWitnessStrip < witness.yml + - entry_type: precondition_loop_invariant + location: + file_name: 05-prec-problem.c + file_hash: $FILE_HASH + line: 13 + column: 4 + function: foo + loop_invariant: + string: result == 1 || result == 0 + type: assertion + format: C + precondition: + string: '*ptr1 == 5 && *ptr2 == 5' + type: assertion + format: C + - entry_type: precondition_loop_invariant + location: + file_name: 05-prec-problem.c + file_hash: $FILE_HASH + line: 13 + column: 4 + function: foo + loop_invariant: + string: '*ptr2 == 5' + type: assertion + format: C + precondition: + string: '*ptr1 == 5 && *ptr2 == 5' + type: assertion + format: C + - entry_type: precondition_loop_invariant + location: + file_name: 05-prec-problem.c + file_hash: $FILE_HASH + line: 13 + column: 4 + function: foo + loop_invariant: + string: '*ptr1 == 5' + type: assertion + format: C + precondition: + string: '*ptr1 == 5 && *ptr2 == 5' + type: assertion + format: C diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t index 64ab054549..bd7012ec25 100644 --- a/tests/regression/56-witness/08-witness-all-locals.t +++ b/tests/regression/56-witness/08-witness-all-locals.t @@ -6,7 +6,40 @@ [Info][Witness] witness generation summary: total generation entries: 3 -TODO: check witness.yml content with yamlWitnessStrip + $ yamlWitnessStrip < witness.yml + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 9 + column: 2 + function: main + location_invariant: + string: y == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 9 + column: 2 + function: main + location_invariant: + string: x == 5 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 7 + column: 4 + function: main + location_invariant: + string: x == 5 + type: assertion + format: C Fewer entries are emitted if locals from nested block scopes are excluded: @@ -19,4 +52,26 @@ Fewer entries are emitted if locals from nested block scopes are excluded: [Info][Witness] witness generation summary: total generation entries: 2 -TODO: check witness.yml content with yamlWitnessStrip + $ yamlWitnessStrip < witness.yml + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 9 + column: 2 + function: main + location_invariant: + string: x == 5 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 7 + column: 4 + function: main + location_invariant: + string: x == 5 + type: assertion + format: C diff --git a/tests/regression/56-witness/10-apron-unassume-interval.c b/tests/regression/56-witness/10-apron-unassume-interval.c index e35d42d563..1ee6117c61 100644 --- a/tests/regression/56-witness/10-apron-unassume-interval.c +++ b/tests/regression/56-witness/10-apron-unassume-interval.c @@ -3,7 +3,7 @@ // Using polyhedra instead of octagon, because the former has no narrowing and really needs the witness. int main() { int i = 0; - while (i < 100) { + while (i < 100) { // TODO: location invariant before loop doesn't work anymore i++; } assert(i == 100); diff --git a/tests/regression/56-witness/10-apron-unassume-interval.yml b/tests/regression/56-witness/10-apron-unassume-interval.yml index 12cc344957..f7958922ae 100644 --- a/tests/regression/56-witness/10-apron-unassume-interval.yml +++ b/tests/regression/56-witness/10-apron-unassume-interval.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e @@ -22,11 +22,11 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: 100LL - (long long )i >= 0LL type: assertion format: C -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 4e078bcd-9e55-4874-a86e-0563927704a5 @@ -50,7 +50,7 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: (long long )i >= 0LL type: assertion format: C diff --git a/tests/regression/56-witness/11-base-unassume-interval.c b/tests/regression/56-witness/11-base-unassume-interval.c index bfecee5bbe..f8b685fcb1 100644 --- a/tests/regression/56-witness/11-base-unassume-interval.c +++ b/tests/regression/56-witness/11-base-unassume-interval.c @@ -3,7 +3,7 @@ int main() { int i = 0; - while (i < 100) { + while (i < 100) { // TODO: location invariant before loop doesn't work anymore i++; } assert(i == 100); diff --git a/tests/regression/56-witness/11-base-unassume-interval.yml b/tests/regression/56-witness/11-base-unassume-interval.yml index bb4740c7b0..df939b7ca4 100644 --- a/tests/regression/56-witness/11-base-unassume-interval.yml +++ b/tests/regression/56-witness/11-base-unassume-interval.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e @@ -22,11 +22,11 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: 100LL - (long long )i >= 0LL type: assertion format: C -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 4e078bcd-9e55-4874-a86e-0563927704a5 @@ -50,7 +50,7 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: (long long )i >= 0LL type: assertion format: C diff --git a/tests/regression/56-witness/14-base-unassume-precondition.c b/tests/regression/56-witness/14-base-unassume-precondition.c index 8e6a1b3c73..23b2d8b923 100644 --- a/tests/regression/56-witness/14-base-unassume-precondition.c +++ b/tests/regression/56-witness/14-base-unassume-precondition.c @@ -3,7 +3,7 @@ void foo(int n) { int i = 0; - while (i < n) { + while (i < n) { // TODO: (precondition) location invariant before loop doesn't work anymore i++; } assert(i == n); diff --git a/tests/regression/56-witness/14-base-unassume-precondition.yml b/tests/regression/56-witness/14-base-unassume-precondition.yml index df4bbc8dc7..2d84e4ea9f 100644 --- a/tests/regression/56-witness/14-base-unassume-precondition.yml +++ b/tests/regression/56-witness/14-base-unassume-precondition.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 26e6d2de-13a6-4610-9b08-ee3d9e6b9338 @@ -21,7 +21,7 @@ line: 6 column: 2 function: foo - location_invariant: + loop_invariant: string: 0 <= i type: assertion format: C diff --git a/tests/regression/56-witness/20-apron-unassume-global.c b/tests/regression/56-witness/20-apron-unassume-global.c index 6ad4146ba2..f8cdc63ba4 100644 --- a/tests/regression/56-witness/20-apron-unassume-global.c +++ b/tests/regression/56-witness/20-apron-unassume-global.c @@ -3,7 +3,7 @@ int i = 0; int main() { - while (i < 100) { + while (i < 100) { // TODO: location invariant before loop doesn't work anymore i++; } assert(i == 100); diff --git a/tests/regression/56-witness/20-apron-unassume-global.yml b/tests/regression/56-witness/20-apron-unassume-global.yml index 641adcac2b..6f824d4f9f 100644 --- a/tests/regression/56-witness/20-apron-unassume-global.yml +++ b/tests/regression/56-witness/20-apron-unassume-global.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e @@ -22,11 +22,11 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: 100LL - (long long )i >= 0LL type: assertion format: C -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 4e078bcd-9e55-4874-a86e-0563927704a5 @@ -50,7 +50,7 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: (long long )i >= 0LL type: assertion format: C diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.c b/tests/regression/56-witness/26-mine-tutorial-ex4.6.c index d497c6344a..129f7e809a 100644 --- a/tests/regression/56-witness/26-mine-tutorial-ex4.6.c +++ b/tests/regression/56-witness/26-mine-tutorial-ex4.6.c @@ -2,7 +2,7 @@ #include int main() { int x = 40; - while (x != 0) { + while (x != 0) { // TODO: location invariant before loop doesn't work anymore __goblint_check(x <= 40); x--; __goblint_check(x >= 0); diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml index 2e3c6758fc..659537ba77 100644 --- a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml +++ b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 0e84a9de-b9f6-44dd-ab8d-ebdeca941482 @@ -21,7 +21,7 @@ line: 5 column: 2 function: main - location_invariant: + loop_invariant: string: 0 <= x && x <= 40 type: assertion format: C diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.c b/tests/regression/56-witness/27-mine-tutorial-ex4.7.c index 10f83ba6e2..2589c596b8 100644 --- a/tests/regression/56-witness/27-mine-tutorial-ex4.7.c +++ b/tests/regression/56-witness/27-mine-tutorial-ex4.7.c @@ -3,7 +3,7 @@ extern _Bool __VERIFIER_nondet_bool(); int main() { int x = 0; - while (__VERIFIER_nondet_bool() == 0) { + while (__VERIFIER_nondet_bool() == 0) { // TODO: location invariant before loop doesn't work anymore __goblint_check(0 <= x); __goblint_check(x <= 40); if (__VERIFIER_nondet_bool() == 0) { diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml index ad4c287227..c87b070d40 100644 --- a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml +++ b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: e17f9860-95af-4213-a767-ab4876ead27e @@ -21,9 +21,9 @@ file_name: 27-mine-tutorial-ex4.7.c file_hash: 4d06e38718d405171bd503e630f6c7a247bb3b0d3c1c6c951466e4989883b43c line: 6 - column: 8 + column: 2 function: main - location_invariant: + loop_invariant: string: 0 <= x && x <= 40 type: assertion format: C diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.c b/tests/regression/56-witness/28-mine-tutorial-ex4.8.c index 6892267fc8..b2881cdfa6 100644 --- a/tests/regression/56-witness/28-mine-tutorial-ex4.8.c +++ b/tests/regression/56-witness/28-mine-tutorial-ex4.8.c @@ -3,7 +3,7 @@ extern _Bool __VERIFIER_nondet_bool(); int main() { int v = 0; - while (__VERIFIER_nondet_bool() == 0) { + while (__VERIFIER_nondet_bool() == 0) { // TODO: location invariant before loop doesn't work anymore __goblint_check(0 <= v); __goblint_check(v <= 1); if (v == 0) diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml index 69479e6df0..c92f0223e4 100644 --- a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml +++ b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 299c2080-fb13-4879-be2b-5d2758465577 @@ -23,7 +23,7 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: 0 <= v && v <= 1 type: assertion format: C diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.c b/tests/regression/56-witness/29-mine-tutorial-ex4.10.c index 655c19e08e..437e20130c 100644 --- a/tests/regression/56-witness/29-mine-tutorial-ex4.10.c +++ b/tests/regression/56-witness/29-mine-tutorial-ex4.10.c @@ -3,7 +3,7 @@ #include int main() { int v = 1; // Not explicitly stated in Miné's example - while (v <= 50) { + while (v <= 50) { // TODO: location invariant before loop doesn't work anymore __goblint_check(1 <= v); v += 2; __goblint_check(v <= 52); diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml index 0f9b362290..c719c76c0a 100644 --- a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml +++ b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: f04fe372-3d6e-4a80-9567-80c64bd7fd03 @@ -24,7 +24,7 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: 1 <= v && v <= 52 type: assertion format: C diff --git a/tests/regression/56-witness/35-hh-ex1b.yml b/tests/regression/56-witness/35-hh-ex1b.yml index 9763960fd7..084c71cc97 100644 --- a/tests/regression/56-witness/35-hh-ex1b.yml +++ b/tests/regression/56-witness/35-hh-ex1b.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 1a354f1e-76e8-40e9-808a-8d5efbe35496 @@ -21,9 +21,9 @@ file_name: 35-hh-ex1b.c file_hash: 9fe07d5f950140350848bae4342d9d1b7c6c9f625f6985746089a36a37243600 line: 7 - column: 2 + column: 4 function: main - location_invariant: + loop_invariant: string: 0 <= i && i <= 99 type: assertion format: C diff --git a/tests/regression/56-witness/36-hh-ex2b.c b/tests/regression/56-witness/36-hh-ex2b.c index f8d35f28bd..41c5fcf71e 100644 --- a/tests/regression/56-witness/36-hh-ex2b.c +++ b/tests/regression/56-witness/36-hh-ex2b.c @@ -3,7 +3,7 @@ extern _Bool __VERIFIER_nondet_bool(); int main() { int n = 0; - while (1) { + while (1) { // TODO: location invariant before loop doesn't work anymore __goblint_check(n <= 60); if (__VERIFIER_nondet_bool()) { if (n < 60) { diff --git a/tests/regression/56-witness/36-hh-ex2b.yml b/tests/regression/56-witness/36-hh-ex2b.yml index 69e0a88841..d2a7218a28 100644 --- a/tests/regression/56-witness/36-hh-ex2b.yml +++ b/tests/regression/56-witness/36-hh-ex2b.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 9589b9d4-edce-4043-8413-279703946762 @@ -23,7 +23,7 @@ line: 6 column: 2 function: main - location_invariant: + loop_invariant: string: 0 <= n && n <= 60 type: assertion format: C diff --git a/tests/regression/56-witness/38-bh-ex3.c b/tests/regression/56-witness/38-bh-ex3.c index 633394586f..2a5d07fc1e 100644 --- a/tests/regression/56-witness/38-bh-ex3.c +++ b/tests/regression/56-witness/38-bh-ex3.c @@ -4,7 +4,7 @@ extern _Bool __VERIFIER_nondet_bool(); int main() { int m = 0; int n = 0; - while (1) { + while (1) { // TODO: location invariant before loop doesn't work anymore __goblint_check(m <= 60); __goblint_check(n <= 60); if (__VERIFIER_nondet_bool()) { diff --git a/tests/regression/56-witness/38-bh-ex3.yml b/tests/regression/56-witness/38-bh-ex3.yml index d1f6677fbb..2e489e1f17 100644 --- a/tests/regression/56-witness/38-bh-ex3.yml +++ b/tests/regression/56-witness/38-bh-ex3.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: bd436e09-244f-45db-a5f4-9337ca997424 @@ -23,7 +23,7 @@ line: 7 column: 2 function: main - location_invariant: + loop_invariant: string: 0 <= m && m <= 60 && 0 <= n && n <= 60 type: assertion format: C diff --git a/tests/regression/56-witness/39-bh-ex-add.c b/tests/regression/56-witness/39-bh-ex-add.c index 256e274b73..630ef344a4 100644 --- a/tests/regression/56-witness/39-bh-ex-add.c +++ b/tests/regression/56-witness/39-bh-ex-add.c @@ -4,7 +4,7 @@ extern _Bool __VERIFIER_nondet_bool(); int main() { int m = 0; int n = 0; - while (1) { + while (1) { // TODO: location invariant before loop doesn't work anymore __goblint_check(m <= 60); __goblint_check(n <= 60); if (__VERIFIER_nondet_bool()) { diff --git a/tests/regression/56-witness/39-bh-ex-add.yml b/tests/regression/56-witness/39-bh-ex-add.yml index 84aa374c1e..29d3006276 100644 --- a/tests/regression/56-witness/39-bh-ex-add.yml +++ b/tests/regression/56-witness/39-bh-ex-add.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: bd436e09-244f-45db-a5f4-9337ca997424 @@ -23,7 +23,7 @@ line: 7 column: 2 function: main - location_invariant: + loop_invariant: string: 0 <= m && m <= 60 && 0 <= n && n <= 60 type: assertion format: C diff --git a/tests/regression/56-witness/41-as-hybrid.c b/tests/regression/56-witness/41-as-hybrid.c index 7735187036..3a3a4c6ea6 100644 --- a/tests/regression/56-witness/41-as-hybrid.c +++ b/tests/regression/56-witness/41-as-hybrid.c @@ -2,7 +2,7 @@ #include int main() { int i = 0; - while (1) { + while (1) { // TODO: location invariant before loop doesn't work anymore i++; int j = 0; while (j < 10) { diff --git a/tests/regression/56-witness/41-as-hybrid.yml b/tests/regression/56-witness/41-as-hybrid.yml index 0e810b6aca..8eac9f75f7 100644 --- a/tests/regression/56-witness/41-as-hybrid.yml +++ b/tests/regression/56-witness/41-as-hybrid.yml @@ -1,4 +1,4 @@ -- entry_type: location_invariant +- entry_type: loop_invariant metadata: format_version: "0.1" uuid: 71b761c6-4f85-405e-8ee6-9a3a8f743513 @@ -23,7 +23,7 @@ line: 5 column: 2 function: main - location_invariant: + loop_invariant: string: 0 <= i && i <= 9 type: assertion format: C diff --git a/tests/regression/56-witness/44-base-unassume-array.yml b/tests/regression/56-witness/44-base-unassume-array.yml index dbf7fb8e54..ad2e3a3ad2 100644 --- a/tests/regression/56-witness/44-base-unassume-array.yml +++ b/tests/regression/56-witness/44-base-unassume-array.yml @@ -21,7 +21,7 @@ file_name: 44-base-unassume-array.c file_hash: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726 line: 7 - column: 6 + column: 2 function: main loop_invariant: string: 0 <= a[(long )"all_index"] @@ -50,7 +50,7 @@ file_name: 44-base-unassume-array.c file_hash: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726 line: 7 - column: 6 + column: 2 function: main loop_invariant: string: a[(long )"all_index"] < 3 diff --git a/tests/regression/70-transform/01-ordering.t b/tests/regression/70-transform/01-ordering.t index cd7ec8e36a..9ff5a9b739 100644 --- a/tests/regression/70-transform/01-ordering.t +++ b/tests/regression/70-transform/01-ordering.t @@ -1,3 +1,6 @@ +Suppress backtrace with code locations, especially for CI. + $ export OCAMLRUNPARAM=b=0 + Check that assert transform is not allowed to happen after dead code removal $ ./transform.sh --stderr remove_dead_code assert -- 01-empty.c [Error] trans.activated: the 'assert' transform may not occur after the 'remove_dead_code' transform diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index a9f91bf4a6..6dcb21863e 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -1,48 +1,215 @@ $ cfgDot foo.c $ graph-easy --as=boxart main.dot - ┌───────────────────────────────┐ - │ main() │ - └───────────────────────────────┘ - │ - │ (body) - ▼ - ┌───────────────────────────────┐ - │ foo.c:2:7-2:12 │ - │ (foo.c:2:7-2:12) │ - └───────────────────────────────┘ - │ - │ a = 1 - ▼ - ┌───────────────────────────────┐ - │ foo.c:2:14-2:19 │ - │ (foo.c:2:14-2:19) │ - └───────────────────────────────┘ - │ - │ b = 1 - ▼ - ┌──────────────────┐ ┌───────────────────────────────┐ - │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:3-6:3 (synthetic) │ - ┌──────▶ │ (unknown) │ ◀──────────── │ (foo.c:3:10-3:20 (synthetic)) │ ◀┐ - │ └──────────────────┘ └───────────────────────────────┘ │ - │ │ │ │ - │ │ return 0 │ Pos(a > 0) │ - │ ▼ ▼ │ - │ Neg(b) ┌──────────────────┐ ┌───────────────────────────────┐ │ - │ │ return of main() │ │ foo.c:3:3-6:3 (synthetic) │ │ - │ │ │ ┌─────────── │ (foo.c:3:10-3:20 (synthetic)) │ │ - │ └──────────────────┘ │ └───────────────────────────────┘ │ - │ │ │ │ - └──────────────────────────────┘ │ Pos(b) │ b = b - 1 - ▼ │ - ┌───────────────────────────────┐ │ - │ foo.c:4:5-4:8 │ │ - │ (foo.c:4:5-4:8) │ │ - └───────────────────────────────┘ │ - │ │ - │ a = a + 1 │ - ▼ │ - ┌───────────────────────────────┐ │ - │ foo.c:5:5-5:8 │ │ - │ (foo.c:5:5-5:8) │ ─┘ - └───────────────────────────────┘ + ┌───────────────────────────────┐ + │ main() │ + └───────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────┐ + │ foo.c:2:3-2:19 │ + │ (foo.c:2:7-2:12 (synthetic)) │ + │ YAML loc: foo.c:2:3-2:19 │ + │ GraphML: true; server: false │ + └───────────────────────────────┘ + │ + │ a = 1 + ▼ + ┌───────────────────────────────┐ + │ foo.c:2:3-2:19 (synthetic) │ + │ (foo.c:2:14-2:19 (synthetic)) │ + │ GraphML: true; server: false │ + └───────────────────────────────┘ + │ + │ b = 1 + ▼ + ┌─────────────────────────────┐ ┌───────────────────────────────┐ + │ foo.c:7:3-7:11 │ │ foo.c:3:3-6:3 (synthetic) │ + │ (foo.c:7:10-7:11) │ │ (foo.c:3:10-3:20 (synthetic)) │ + │ YAML loc: foo.c:7:3-7:11 │ │ YAML loop: foo.c:3:3-6:3 │ + │ GraphML: true; server: true │ Neg(a > 0) │ GraphML: true; server: false │ + ┌──────▶ │ │ ◀──────────── │ loop: foo.c:3:3-6:3 │ ◀┐ + │ └─────────────────────────────┘ └───────────────────────────────┘ │ + │ │ │ │ + │ │ return 0 │ Pos(a > 0) │ + │ ▼ ▼ │ + │ ┌─────────────────────────────┐ ┌───────────────────────────────┐ │ + │ Neg(b) │ │ │ foo.c:3:3-6:3 (synthetic) │ │ + │ │ return of main() │ │ (foo.c:3:10-3:20 (synthetic)) │ │ + │ │ │ ┌─────────── │ GraphML: true; server: false │ │ + │ └─────────────────────────────┘ │ └───────────────────────────────┘ │ + │ │ │ │ + └─────────────────────────────────────────┘ │ Pos(b) │ + ▼ │ b = b - 1 + ┌───────────────────────────────┐ │ + │ foo.c:4:5-4:8 │ │ + │ (foo.c:4:5-4:8) │ │ + │ YAML loc: foo.c:4:5-4:8 │ │ + │ GraphML: true; server: true │ │ + └───────────────────────────────┘ │ + │ │ + │ a = a + 1 │ + ▼ │ + ┌───────────────────────────────┐ │ + │ foo.c:5:5-5:8 │ │ + │ (foo.c:5:5-5:8) │ │ + │ YAML loc: foo.c:5:5-5:8 │ │ + │ GraphML: true; server: true │ ─┘ + └───────────────────────────────┘ + + $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' --set sem.int.signed_overflow assume_none foo.c + [Warning][Integer > Overflow][CWE-190] Signed integer overflow (foo.c:4:5-4:8) + [Warning][Integer > Overflow][CWE-191] Signed integer underflow (foo.c:5:5-5:8) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 6 + dead: 0 + 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: + total generation entries: 13 + + $ yamlWitnessStrip < witness.yml + - entry_type: loop_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 3 + column: 2 + function: main + loop_invariant: + string: b <= 1 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 3 + column: 2 + function: main + loop_invariant: + string: 1 <= a + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 7 + column: 2 + function: main + location_invariant: + string: b == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 7 + column: 2 + function: main + location_invariant: + string: a != 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 7 + column: 2 + function: main + location_invariant: + string: 1 <= a + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 5 + column: 4 + function: main + location_invariant: + string: b <= 1 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 5 + column: 4 + function: main + location_invariant: + string: b != 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 5 + column: 4 + function: main + location_invariant: + string: a != 1 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 5 + column: 4 + function: main + location_invariant: + string: 2 <= a + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: b <= 1 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: b != 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: a != 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: 1 <= a + type: assertion + format: C diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t index 78a81aff68..03dc2c1d0c 100644 --- a/tests/regression/cfg/issue-1356.t/run.t +++ b/tests/regression/cfg/issue-1356.t/run.t @@ -11,15 +11,18 @@ │ Pos((long )a >= (long )b - 2147483648) │ (body) │ ▼ ▼ │ ┌─────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ │ - │ issue-1356.c:9:3-9:53 (synthetic) │ Pos(b <= 0) │ issue-1356.c:9:3-9:53 │ │ - │ (issue-1356.c:9:3-9:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:9:3-9:53) │ │ + │ issue-1356.c:9:3-9:53 (synthetic) │ │ issue-1356.c:9:3-9:53 │ │ + │ (issue-1356.c:9:3-9:53 (synthetic)) │ │ (issue-1356.c:9:3-9:53) │ │ + │ GraphML: true; server: false │ Pos(b <= 0) │ YAML loc: issue-1356.c:9:3-9:53 │ │ + │ │ ◀────────────────────────── │ GraphML: true; server: true │ │ └─────────────────────────────────────────┘ └─────────────────────────────────────────┘ │ │ │ │ │ │ Neg(b <= 0) │ │ ▼ │ │ ┌─────────────────────────────────────────┐ │ │ │ issue-1356.c:9:3-9:53 (synthetic) │ │ - │ │ (issue-1356.c:9:3-9:53 (synthetic)) │ ─┘ + │ │ (issue-1356.c:9:3-9:53 (synthetic)) │ │ + │ │ GraphML: true; server: false │ ─┘ │ └─────────────────────────────────────────┘ │ │ │ │ Neg((long )a >= (long )b - 2147483648) @@ -27,48 +30,57 @@ │ ┌─────────────────────────────────────────┐ │ │ issue-1356.c:9:3-9:53 (synthetic) │ │ │ (issue-1356.c:9:3-9:53 (synthetic)) │ + │ │ GraphML: true; server: false │ │ └─────────────────────────────────────────┘ │ │ │ │ tmp = 0 │ ▼ │ ┌─────────────────────────────────────────┐ - │ tmp = 1 │ issue-1356.c:9:3-9:53 (synthetic) │ - └───────────────────────────────────────────────────────────────────▶ │ (issue-1356.c:9:3-9:53 (synthetic)) │ + │ │ issue-1356.c:9:3-9:53 (synthetic) │ + │ tmp = 1 │ (issue-1356.c:9:3-9:53 (synthetic)) │ + └───────────────────────────────────────────────────────────────────▶ │ GraphML: true; server: false │ └─────────────────────────────────────────┘ │ │ assume_abort_if_not(tmp) ▼ ┌─────────────────────────────────────────┐ │ issue-1356.c:10:3-10:53 │ - │ (issue-1356.c:10:3-10:53) │ ─┐ + │ (issue-1356.c:10:3-10:53) │ + │ YAML loc: issue-1356.c:10:3-10:53 │ + │ GraphML: true; server: true │ ─┐ └─────────────────────────────────────────┘ │ │ │ │ Neg(b >= 0) │ ▼ │ ┌─────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ │ - │ issue-1356.c:10:3-10:53 (synthetic) │ Neg(a <= b + 2147483647) │ issue-1356.c:10:3-10:53 (synthetic) │ │ - │ (issue-1356.c:10:3-10:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:10:3-10:53 (synthetic)) │ │ Pos(b >= 0) + │ issue-1356.c:10:3-10:53 (synthetic) │ │ issue-1356.c:10:3-10:53 (synthetic) │ │ + │ (issue-1356.c:10:3-10:53 (synthetic)) │ Neg(a <= b + 2147483647) │ (issue-1356.c:10:3-10:53 (synthetic)) │ │ Pos(b >= 0) + │ GraphML: true; server: false │ ◀────────────────────────── │ GraphML: true; server: false │ │ └─────────────────────────────────────────┘ └─────────────────────────────────────────┘ │ │ │ │ │ │ Pos(a <= b + 2147483647) │ │ ▼ │ │ ┌─────────────────────────────────────────┐ │ │ │ issue-1356.c:10:3-10:53 (synthetic) │ │ - │ │ (issue-1356.c:10:3-10:53 (synthetic)) │ ◀┘ + │ │ (issue-1356.c:10:3-10:53 (synthetic)) │ │ + │ │ GraphML: true; server: false │ ◀┘ │ └─────────────────────────────────────────┘ │ │ │ │ tmp___0 = 1 │ ▼ │ ┌─────────────────────────────────────────┐ - │ tmp___0 = 0 │ issue-1356.c:10:3-10:53 (synthetic) │ - └───────────────────────────────────────────────────────────────────▶ │ (issue-1356.c:10:3-10:53 (synthetic)) │ + │ │ issue-1356.c:10:3-10:53 (synthetic) │ + │ tmp___0 = 0 │ (issue-1356.c:10:3-10:53 (synthetic)) │ + └───────────────────────────────────────────────────────────────────▶ │ GraphML: true; server: false │ └─────────────────────────────────────────┘ │ │ assume_abort_if_not(tmp___0) ▼ ┌─────────────────────────────────────────┐ │ issue-1356.c:11:3-11:15 │ - │ (unknown) │ + │ (issue-1356.c:11:10-11:15) │ + │ YAML loc: issue-1356.c:11:3-11:15 │ + │ GraphML: true; server: true │ └─────────────────────────────────────────┘ │ │ return a - b @@ -76,3 +88,18 @@ ┌─────────────────────────────────────────┐ │ return of minus() │ └─────────────────────────────────────────┘ + + + + $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' issue-1356.c + [Warning][Integer > Overflow][CWE-190] Signed integer overflow (issue-1356.c:10:3-10:53) + [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:10-11:15) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 13 + dead: 0 + total lines: 13 + [Info][Witness] witness generation summary: + total generation entries: 0 + + $ yamlWitnessStrip < witness.yml + [] diff --git a/tests/regression/cfg/loops.t/loops.c b/tests/regression/cfg/loops.t/loops.c new file mode 100644 index 0000000000..cac7837bcc --- /dev/null +++ b/tests/regression/cfg/loops.t/loops.c @@ -0,0 +1,50 @@ +#include + +int main() { + int i; + + // while loop + i = 0; + while (i < 10) { + i++; + } + + // for loop + for (i = 0; i < 10; i++) { + __goblint_check(1); + } + + // for loop with empty body + for (i = 0; i < 10; i++) { + + } + + // for loop with empty increment + for (i = 0; i < 10;) { + i++; + } + + // for loop with empty initializer + i = 0; + for (; i < 10; i++) { + __goblint_check(1); + } + + // for loop with declaration initializer + for (int j = 0; j < 10; j++) { + __goblint_check(1); + } + + // for loop with two initializers + for (int k = (i = 0); i < 10; i++) { + __goblint_check(1); + } + + // do-while loop + i = 0; + do { + i++; + } while (i < 10); + + return 0; +} diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t new file mode 100644 index 0000000000..01216a624e --- /dev/null +++ b/tests/regression/cfg/loops.t/run.t @@ -0,0 +1,807 @@ + $ cfgDot loops.c + + $ graph-easy --as=boxart main.dot + + ┌──────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ │ + ┌───────────────────────────────────────────────────┼─────────────────────────────────────────────────────────────────────────┐ │ + │ │ │ │ + │ │ │ │ + │ ┌──────────────────────────────────────────────┼────────────────────────────────────────────────────────────────────┐ │ │ + │ │ │ │ │ │ + │ │ │ │ │ │ + │ │ ┌─────────────────────────────────────────┼────────────────────────────────────────────────────┐ │ │ │ + │ │ │ │ │ │ │ │ + │ │ │ │ ┌───────────────────────────────────┐ │ │ │ │ + │ │ │ ┌────────────────────────────────────┘ │ main() │ │ │ │ │ + │ │ │ │ └───────────────────────────────────┘ │ │ │ │ + │ │ │ │ │ │ │ │ │ i = i + 1 + │ │ │ │ │ (body) │ │ │ │ + │ │ │ │ ▼ │ │ │ │ + │ │ │ │ ┌───────────────────────────────────┐ │ │ │ │ + │ │ │ │ │ loops.c:7:3-7:8 │ │ │ │ │ + │ │ │ │ │ (loops.c:7:3-7:8) │ │ │ │ │ + │ │ │ │ │ YAML loc: loops.c:7:3-7:8 │ │ │ │ │ + │ │ │ │ │ GraphML: true; server: true │ │ │ │ │ + │ │ │ │ └───────────────────────────────────┘ │ │ │ │ + │ │ │ │ │ │ │ │ │ + │ │ │ │ │ i = 0 │ │ │ │ + │ │ │ │ ▼ │ │ │ │ + │ │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ │ │ + │ │ │ │ loops.c:9:5-9:8 │ │ loops.c:8:3-10:3 (synthetic) │ │ │ │ │ + │ │ │ │ (loops.c:9:5-9:8) │ │ (loops.c:8:10-8:16 (synthetic)) │ │ │ │ │ + │ │ │ │ YAML loc: loops.c:9:5-9:8 │ │ YAML loop: loops.c:8:3-10:3 │ │ │ │ │ + │ │ │ │ GraphML: true; server: true │ Pos(i < 10) │ GraphML: true; server: false │ │ │ │ │ + │ │ │ │ │ ◀───────────── │ loop: loops.c:8:3-10:3 │ ◀┼───────────────┼────┼────┘ + │ │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ │ Neg(i < 10) │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ + │ │ │ │ loops.c:13:3-15:3 │ │ │ │ + │ │ │ │ (loops.c:13:7-13:26 (synthetic)) │ │ │ │ + │ │ │ │ YAML loc: loops.c:13:3-15:3 │ │ i = i + 1 │ │ + │ │ │ │ GraphML: true; server: false │ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ │ i = 0 │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ │ + │ │ │ │ loops.c:14:5-14:23 │ │ loops.c:13:3-15:3 (synthetic) │ │ │ │ + │ │ │ │ (loops.c:14:5-14:23) │ │ (loops.c:13:7-13:26 (synthetic)) │ │ │ │ + │ │ │ │ YAML loc: loops.c:14:5-14:23 │ │ YAML loop: loops.c:13:3-15:3 │ │ │ │ + │ │ │ │ GraphML: true; server: true │ Pos(i < 10) │ GraphML: true; server: false │ │ │ │ + │ │ │ │ │ ◀───────────── │ loop: loops.c:13:3-15:3 │ ◀┘ │ │ + │ │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ + │ │ │ │ │ │ │ + │ │ │ │ __goblint_check(1) │ Neg(i < 10) │ │ + │ │ │ ▼ ▼ │ │ + │ │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ + │ │ │ │ loops.c:13:3-15:3 (synthetic) │ │ loops.c:18:3-20:3 │ │ │ + │ │ │ │ (loops.c:13:7-13:26 (synthetic)) │ │ (loops.c:18:7-18:26 (synthetic)) │ │ │ + │ │ │ │ GraphML: true; server: false │ │ YAML loc: loops.c:18:3-20:3 │ │ │ + │ │ └─ │ │ │ GraphML: true; server: false │ │ │ + │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ │ i = 0 │ │ + │ │ ▼ │ │ + │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ + │ │ │ │ │ loops.c:18:3-20:3 (synthetic) │ │ │ + │ │ │ loops.c:18:3-20:3 (synthetic) │ │ (loops.c:18:7-18:26 (synthetic)) │ │ │ + │ │ │ (loops.c:18:7-18:26 (synthetic)) │ │ YAML loop: loops.c:18:3-20:3 │ │ │ + │ │ │ GraphML: true; server: false │ Pos(i < 10) │ GraphML: true; server: false │ i = i + 1 │ │ + │ └────── │ │ ◀───────────── │ loop: loops.c:18:3-20:3 │ ◀────────────────┘ │ + │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ + │ │ │ + │ │ Neg(i < 10) │ + │ ▼ │ + │ ┌───────────────────────────────────┐ │ + │ │ loops.c:23:3-25:3 │ │ + │ │ (loops.c:23:7-23:22 (synthetic)) │ │ + │ │ YAML loc: loops.c:23:3-25:3 │ │ + │ │ GraphML: true; server: false │ │ + │ └───────────────────────────────────┘ │ + │ │ │ + │ │ i = 0 │ + │ ▼ │ + │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ + │ │ loops.c:24:5-24:8 │ │ loops.c:23:3-25:3 (synthetic) │ │ + │ │ (loops.c:24:5-24:8) │ │ (loops.c:23:7-23:22 (synthetic)) │ │ + │ │ YAML loc: loops.c:24:5-24:8 │ │ YAML loop: loops.c:23:3-25:3 │ │ + │ │ GraphML: true; server: true │ Pos(i < 10) │ GraphML: true; server: false │ i = i + 1 │ + └─────────── │ │ ◀───────────── │ loop: loops.c:23:3-25:3 │ ◀─────────────────────┘ + └───────────────────────────────────┘ └───────────────────────────────────┘ + │ + │ Neg(i < 10) + ▼ + ┌───────────────────────────────────┐ + │ loops.c:28:3-28:8 │ + │ (loops.c:28:3-28:8) │ + │ YAML loc: loops.c:28:3-28:8 │ + │ GraphML: true; server: true │ + └───────────────────────────────────┘ + │ + │ i = 0 + ▼ + ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ + │ loops.c:30:5-30:23 │ │ loops.c:29:3-31:3 (synthetic) │ + │ (loops.c:30:5-30:23) │ │ (loops.c:29:7-29:21 (synthetic)) │ + │ YAML loc: loops.c:30:5-30:23 │ │ YAML loop: loops.c:29:3-31:3 │ + │ GraphML: true; server: true │ Pos(i < 10) │ GraphML: true; server: false │ i = i + 1 + │ │ ◀───────────── │ loop: loops.c:29:3-31:3 │ ◀─────────────────────┐ + └───────────────────────────────────┘ └───────────────────────────────────┘ │ + │ │ │ + │ __goblint_check(1) │ Neg(i < 10) │ + ▼ ▼ │ + ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ + │ loops.c:29:3-31:3 (synthetic) │ │ loops.c:34:3-36:3 │ │ + │ (loops.c:29:7-29:21 (synthetic)) │ │ (loops.c:34:12-34:17 (synthetic)) │ │ + │ GraphML: true; server: false │ │ YAML loc: loops.c:34:3-36:3 │ │ + ┌────── │ │ │ GraphML: true; server: false │ │ + │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ + │ │ │ + │ │ j = 0 │ + │ ▼ │ + │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ + │ │ loops.c:35:5-35:23 │ │ loops.c:34:3-36:3 (synthetic) │ │ + │ │ (loops.c:35:5-35:23) │ │ (loops.c:34:7-34:30 (synthetic)) │ │ + │ │ YAML loc: loops.c:35:5-35:23 │ │ YAML loop: loops.c:34:3-36:3 │ │ + │ │ GraphML: true; server: true │ Pos(j < 10) │ GraphML: true; server: false │ j = j + 1 │ + │ │ │ ◀───────────── │ loop: loops.c:34:3-36:3 │ ◀─────────────────────┼────┐ + │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ __goblint_check(1) │ Neg(j < 10) │ │ + │ ▼ ▼ │ │ + │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ + │ │ loops.c:34:3-36:3 (synthetic) │ │ loops.c:39:3-41:3 │ │ │ + │ │ (loops.c:34:12-34:17 (synthetic)) │ │ (loops.c:39:12-39:23 (synthetic)) │ │ │ + │ │ GraphML: true; server: false │ │ YAML loc: loops.c:39:3-41:3 │ │ │ + │ │ │ │ GraphML: true; server: false │ │ │ + │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ │ i = 0 │ │ + │ │ ▼ │ │ + │ │ ┌───────────────────────────────────┐ │ │ + │ │ │ loops.c:39:3-41:3 (synthetic) │ │ │ + │ │ │ (loops.c:39:12-39:23 (synthetic)) │ │ │ + │ │ │ GraphML: true; server: false │ │ │ + │ │ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ ┌────┘ │ k = i │ │ + │ │ ▼ │ │ + │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ + │ │ │ loops.c:40:5-40:23 │ │ loops.c:39:3-41:3 (synthetic) │ │ │ + │ │ │ (loops.c:40:5-40:23) │ │ (loops.c:39:7-39:36 (synthetic)) │ │ │ + │ │ │ YAML loc: loops.c:40:5-40:23 │ │ YAML loop: loops.c:39:3-41:3 │ │ │ + │ │ │ GraphML: true; server: true │ Pos(i < 10) │ GraphML: true; server: false │ i = i + 1 │ │ + │ │ │ │ ◀───────────── │ loop: loops.c:39:3-41:3 │ ◀─────────────────────┼────┼─────────────┐ + │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ __goblint_check(1) │ Neg(i < 10) │ │ │ + │ │ ▼ ▼ │ │ │ + │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ │ + │ │ │ loops.c:39:3-41:3 (synthetic) │ │ loops.c:44:3-44:8 │ │ │ │ + │ │ │ (loops.c:39:12-39:23 (synthetic)) │ │ (loops.c:44:3-44:8) │ │ │ │ + │ │ │ GraphML: true; server: false │ │ YAML loc: loops.c:44:3-44:8 │ │ │ │ + │ │ │ │ │ GraphML: true; server: true │ │ │ │ + │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ │ i = 0 │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ + │ │ │ │ loops.c:46:5-46:8 │ │ │ │ + │ │ │ │ (loops.c:46:5-46:8) │ │ │ │ + │ │ │ │ YAML loc: loops.c:46:5-46:8 │ │ │ │ + │ │ │ │ YAML loop: loops.c:45:3-47:19 │ │ │ │ + │ │ │ │ GraphML: true; server: true │ │ │ │ + │ │ │ │ loop: loops.c:45:3-47:19 │ ◀┐ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ │ + │ │ │ │ │ │ │ │ + │ │ │ │ i = i + 1 │ Pos(i < 10) │ │ │ + │ │ │ ▼ │ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ │ + │ │ │ │ loops.c:45:3-47:19 (synthetic) │ │ │ │ │ + │ │ │ │ (loops.c:47:12-47:19 (synthetic)) │ │ │ │ │ + │ │ │ │ GraphML: true; server: false │ ─┘ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ │ Neg(i < 10) │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ + │ │ │ │ loops.c:49:3-49:11 │ │ │ │ + │ │ │ │ (loops.c:49:10-49:11) │ │ │ │ + │ │ │ │ YAML loc: loops.c:49:3-49:11 │ │ │ │ + │ │ │ │ GraphML: true; server: true │ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ └────┼────────────────────────────────────┐ │ return 0 │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ + │ │ │ │ return of main() │ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ + └─────────┼────────────────────────────────────┼─────────────────────────────────────────────────────────────────────────┘ │ │ + │ │ │ │ + │ │ │ │ + │ └──────────────────────────────────────────────────────────────────────────────┘ │ + │ │ + │ │ + └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ + + $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' loops.c + [Success][Assert] Assertion "1" will succeed (loops.c:14:5-14:23) + [Success][Assert] Assertion "1" will succeed (loops.c:30:5-30:23) + [Success][Assert] Assertion "1" will succeed (loops.c:35:5-35:23) + [Success][Assert] Assertion "1" will succeed (loops.c:40:5-40:23) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 20 + dead: 0 + total lines: 20 + [Info][Witness] witness generation summary: + total generation entries: 53 + + $ yamlWitnessStrip < witness.yml + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 45 + column: 2 + function: main + loop_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 45 + column: 2 + function: main + loop_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 45 + column: 2 + function: main + loop_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 45 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + loop_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + loop_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 34 + column: 2 + function: main + loop_invariant: + string: j <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 34 + column: 2 + function: main + loop_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 34 + column: 2 + function: main + loop_invariant: + string: 0 <= j + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 29 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 29 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 23 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 23 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 18 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 18 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 8 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 8 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 49 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 49 + column: 2 + function: main + location_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 49 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 46 + column: 4 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 46 + column: 4 + function: main + location_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 46 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 46 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 44 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 44 + column: 2 + function: main + location_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 44 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 40 + column: 4 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 40 + column: 4 + function: main + location_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 40 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 40 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + location_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 35 + column: 4 + function: main + location_invariant: + string: j <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 35 + column: 4 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 35 + column: 4 + function: main + location_invariant: + string: 0 <= j + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 34 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 30 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 30 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 28 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 24 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 24 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 23 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 18 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 14 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 14 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 9 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 9 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C diff --git a/tests/regression/cfg/pr-758.t/pr-758.c b/tests/regression/cfg/pr-758.t/pr-758.c index 87aa41889d..11db4589a2 100644 --- a/tests/regression/cfg/pr-758.t/pr-758.c +++ b/tests/regression/cfg/pr-758.t/pr-758.c @@ -3,7 +3,7 @@ int main() { // for loop int x = 42; - for (x = 0; x < 10; x++) { // there shouldn't be invariants x <= 9, x <= 10 and 0 <= x before this line + for (x = 0; x < 10; x++) { // there shouldn't be location invariants x <= 9, x <= 10 and 0 <= x before this line // ... } diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t index d87d9128c7..04a68be3b6 100644 --- a/tests/regression/cfg/pr-758.t/run.t +++ b/tests/regression/cfg/pr-758.t/run.t @@ -11,22 +11,29 @@ │ │ (body) │ │ ▼ │ │ ┌────────────────────────────────────┐ │ - │ │ pr-758.c:5:7-5:13 │ │ - │ │ (pr-758.c:5:7-5:13) │ │ + │ │ pr-758.c:5:3-5:13 │ │ + │ │ (pr-758.c:5:7-5:13 (synthetic)) │ │ + │ │ YAML loc: pr-758.c:5:3-5:13 │ │ + │ │ GraphML: true; server: false │ │ │ └────────────────────────────────────┘ │ │ │ │ x = x + 1 │ │ x = 42 │ │ ▼ │ │ ┌────────────────────────────────────┐ │ - │ │ pr-758.c:6:3-8:3 (synthetic) │ │ + │ │ pr-758.c:6:3-8:3 │ │ │ │ (pr-758.c:6:7-6:26 (synthetic)) │ │ + │ │ YAML loc: pr-758.c:6:3-8:3 │ │ + │ │ GraphML: true; server: false │ │ │ └────────────────────────────────────┘ │ │ │ │ │ │ x = 0 │ │ ▼ │ ┌─────────────────────────────────┐ ┌────────────────────────────────────┐ │ - │ pr-758.c:6:3-8:3 (synthetic) │ Pos(x < 10) │ pr-758.c:6:3-8:3 (synthetic) │ │ - │ (pr-758.c:6:7-6:26 (synthetic)) │ ◀───────────── │ (pr-758.c:6:7-6:26 (synthetic)) │ ◀┘ + │ │ │ pr-758.c:6:3-8:3 (synthetic) │ │ + │ pr-758.c:6:3-8:3 (synthetic) │ │ (pr-758.c:6:7-6:26 (synthetic)) │ │ + │ (pr-758.c:6:7-6:26 (synthetic)) │ │ YAML loop: pr-758.c:6:3-8:3 │ │ + │ GraphML: true; server: false │ Pos(x < 10) │ GraphML: true; server: false │ │ + │ │ ◀───────────── │ loop: pr-758.c:6:3-8:3 │ ◀┘ └─────────────────────────────────┘ └────────────────────────────────────┘ │ │ Neg(x < 10) @@ -34,6 +41,8 @@ ┌────────────────────────────────────┐ │ pr-758.c:12:3-12:12 │ │ (pr-758.c:12:3-12:12) │ + │ YAML loc: pr-758.c:12:3-12:12 │ + │ GraphML: true; server: true │ └────────────────────────────────────┘ │ │ k = 0 @@ -41,27 +50,33 @@ ┌────────────────────────────────────┐ │ pr-758.c:12:3-12:12 (synthetic) │ │ (pr-758.c:12:3-12:12 (synthetic)) │ + │ GraphML: true; server: false │ └────────────────────────────────────┘ │ │ i = k ▼ ┌────────────────────────────────────┐ - │ pr-758.c:20:15-20:24 │ - │ (pr-758.c:20:15-20:24) │ + │ pr-758.c:20:3-20:25 │ + │ (pr-758.c:20:15-20:24 (synthetic)) │ + │ YAML loc: pr-758.c:20:3-20:25 │ + │ GraphML: true; server: false │ └────────────────────────────────────┘ │ │ a.kaal = 2 ▼ ┌────────────────────────────────────┐ - │ pr-758.c:20:15-20:24 (synthetic) │ + │ pr-758.c:20:3-20:25 (synthetic) │ │ (pr-758.c:20:15-20:24 (synthetic)) │ + │ GraphML: true; server: false │ └────────────────────────────────────┘ │ │ a.hind = 3 ▼ ┌────────────────────────────────────┐ │ pr-758.c:21:3-21:11 │ - │ (unknown) │ + │ (pr-758.c:21:10-21:11) │ + │ YAML loc: pr-758.c:21:3-21:11 │ + │ GraphML: true; server: true │ └────────────────────────────────────┘ │ │ return 0 @@ -69,3 +84,147 @@ ┌────────────────────────────────────┐ │ return of main() │ └────────────────────────────────────┘ + + + + $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["loop_invariant", "location_invariant"]' pr-758.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 6 + dead: 0 + total lines: 6 + [Info][Witness] witness generation summary: + total generation entries: 12 + + $ yamlWitnessStrip < witness.yml + - entry_type: loop_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 6 + column: 2 + function: main + loop_invariant: + string: x <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 6 + column: 2 + function: main + loop_invariant: + string: 0 <= x + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: i == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: a.kaal == 2 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: a.hind == 3 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: i == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 6 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index 8d28933596..9fea4610ca 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -1,9 +1,15 @@ +open Goblint_lib + let main () = Goblint_logs.Logs.Level.current := Info; Cilfacade.init (); + GobConfig.set_bool "witness.invariant.loop-head" true; + GobConfig.set_bool "witness.invariant.after-lock" true; + GobConfig.set_bool "witness.invariant.other" true; let ast = Cilfacade.getAST (Fpath.v Sys.argv.(1)) in CilCfg0.end_basic_blocks ast; + Cilfacade.current_file := ast; (* Part of CilCfg.createCFG *) GoblintCil.iterGlobals ast (function | GFun (fd, _) -> @@ -12,6 +18,15 @@ let main () = | _ -> () ); let (module Cfg) = CfgTools.compute_cfg ast in + let module FileCfg = + struct + let file = ast + module Cfg = Cfg + end + in + + let module GraphmlWitnessInvariant = WitnessUtil.Invariant (FileCfg) in + let module YamlWitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in let module LocationExtraNodeStyles = struct @@ -30,12 +45,29 @@ let main () = let pp_label_locs ppf label = let locs = CilLocation.get_labelLoc label in - Format.fprintf ppf "[%a]" pp_locs locs + Format.fprintf ppf "@;[%a]" pp_locs locs + + let pp_yaml_loc ppf loc = + Format.fprintf ppf "@;YAML loc: %a" CilType.Location.pp loc + + let pp_yaml_loop ppf loc = + Format.fprintf ppf "@;YAML loop: %a" CilType.Location.pp loc + + let pp_loop_loc ppf loop = + Format.fprintf ppf "@;loop: %a" CilType.Location.pp loop let extraNodeStyles = function - | Node.Statement stmt -> + | Node.Statement stmt as n -> let locs: CilLocation.locs = CilLocation.get_stmtLoc stmt in - let label = Format.asprintf "@[%a@;%a@]" pp_locs locs (Format.pp_print_list ~pp_sep:Format.pp_print_cut pp_label_locs) stmt.labels in + let label = + Format.asprintf "@[%a%a%a%a@;GraphML: %B; server: %B%a@]" + pp_locs locs + (Format.pp_print_list ~pp_sep:GobFormat.pp_print_nothing pp_label_locs) stmt.labels + (Format.pp_print_option pp_yaml_loc) (YamlWitnessInvariant.location_location n) + (Format.pp_print_option pp_yaml_loop) (YamlWitnessInvariant.loop_location n) + (GraphmlWitnessInvariant.is_invariant_node n) (Server.is_server_node n) + (Format.pp_print_option pp_loop_loc) (GraphmlWitnessInvariant.find_syntactic_loop_head n) + in [Printf.sprintf "label=\"%s\"" (Str.global_replace (Str.regexp "\n") "\\n" label)] | _ -> [] end diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune index 8528aca384..21ca60b47b 100644 --- a/tests/regression/cfg/util/dune +++ b/tests/regression/cfg/util/dune @@ -4,6 +4,7 @@ goblint-cil goblint_logs goblint_common + goblint_lib ; TODO: avoid fpath goblint.sites.dune goblint.build-info.dune) diff --git a/tests/regression/dune b/tests/regression/dune index 29a0dc0c20..7ff91483c6 100644 --- a/tests/regression/dune +++ b/tests/regression/dune @@ -1,6 +1,8 @@ (env (_ - (binaries ./cfg/util/cfgDot.exe))) + (binaries + ./cfg/util/cfgDot.exe + ../util/yamlWitnessStrip.exe))) (rule (alias runtest) @@ -20,4 +22,6 @@ (cram (applies_to :whole_subtree) (alias runcramtest) - (deps (package goblint))) + (deps + (package goblint) + %{bin:yamlWitnessStrip})) diff --git a/tests/util/dune b/tests/util/dune new file mode 100644 index 0000000000..6637217651 --- /dev/null +++ b/tests/util/dune @@ -0,0 +1,11 @@ +(executable + (name yamlWitnessStrip) + (libraries + batteries.unthreaded + goblint_std + goblint_lib + yaml + goblint.sites.dune + goblint.build-info.dune) + (flags :standard -open Goblint_std) + (preprocess (pps ppx_deriving.std))) diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml new file mode 100644 index 0000000000..211a8a0e1a --- /dev/null +++ b/tests/util/yamlWitnessStrip.ml @@ -0,0 +1,90 @@ +open Goblint_lib +open YamlWitnessType + +module StrippedEntry = +struct + type t = { + entry_type: EntryType.t; + } + [@@deriving ord] + + let strip_file_hashes {entry_type} = + let stripped_file_hash = "$FILE_HASH" in + let location_strip_file_hash location: Location.t = + {location with file_hash = stripped_file_hash} + in + let target_strip_file_hash target: Target.t = + {target with file_hash = stripped_file_hash} + in + let invariant_strip_file_hash ({invariant_type}: InvariantSet.Invariant.t): InvariantSet.Invariant.t = + let invariant_type: InvariantSet.InvariantType.t = + match invariant_type with + | LocationInvariant x -> + LocationInvariant {x with location = location_strip_file_hash x.location} + | LoopInvariant x -> + LoopInvariant {x with location = location_strip_file_hash x.location} + in + {invariant_type} + in + let entry_type: EntryType.t = + match entry_type with + | LocationInvariant x -> + LocationInvariant {x with location = location_strip_file_hash x.location} + | LoopInvariant x -> + LoopInvariant {x with location = location_strip_file_hash x.location} + | FlowInsensitiveInvariant x -> + FlowInsensitiveInvariant x (* no location to strip *) + | PreconditionLoopInvariant x -> + PreconditionLoopInvariant {x with location = location_strip_file_hash x.location} + | LoopInvariantCertificate x -> + LoopInvariantCertificate {x with target = target_strip_file_hash x.target} + | PreconditionLoopInvariantCertificate x -> + PreconditionLoopInvariantCertificate {x with target = target_strip_file_hash x.target} + | InvariantSet x -> + InvariantSet {content = List.map invariant_strip_file_hash x.content} + | GhostVariable x -> + GhostVariable x (* no location to strip *) + | GhostUpdate x -> + GhostUpdate {x with location = location_strip_file_hash x.location} + in + {entry_type} + + let to_yaml {entry_type} = + `O ([ + ("entry_type", `String (EntryType.entry_type entry_type)); + ] @ EntryType.to_yaml' entry_type) +end + +(* Use set for output, so order is deterministic regardless of Goblint. *) +module StrippedEntrySet = Set.Make (StrippedEntry) + +let main () = + let yaml_str = Batteries.input_all stdin in + let yaml = Yaml.of_string_exn yaml_str in + let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in + + let stripped_entries = List.fold_left (fun stripped_entries yaml_entry -> + match YamlWitnessType.Entry.of_yaml yaml_entry with + | Ok {entry_type; _} -> + let stripped_entry: StrippedEntry.t = {entry_type} in + StrippedEntrySet.add stripped_entry stripped_entries + | Error (`Msg e) -> + Format.eprintf "couldn't parse entry: %s" e; + stripped_entries + ) StrippedEntrySet.empty yaml_entries + in + let stripped_yaml_entries = + StrippedEntrySet.elements stripped_entries + |> List.map StrippedEntry.strip_file_hashes + |> List.rev_map StrippedEntry.to_yaml + in + + let stripped_yaml = `A stripped_yaml_entries in + (* to_file/to_string uses a fixed-size buffer... *) + let stripped_yaml_str = match GobYaml.to_string' stripped_yaml with + | Ok text -> text + | Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m) + in + Batteries.output_string Batteries.stdout stripped_yaml_str + +let () = main ()