diff --git a/goblint.opam b/goblint.opam index fa0e4f3c19..b3723b277b 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#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ] # 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 8c9e914575..d0de1c8255 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#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ] [ "ppx_deriving.5.2.1" diff --git a/goblint.opam.template b/goblint.opam.template index 1364586310..a3bb99ff5c 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#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ] # 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 88a2c5a5b1..40d4390eab 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -24,7 +24,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 = { @@ -38,26 +38,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) @@ -127,7 +127,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 -> @@ -190,7 +190,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 -> @@ -204,7 +204,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 35a4cce5d5..60a9a4dc84 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." 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. *) @@ -617,7 +611,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 @@ -626,13 +620,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..71290a2ec0 100644 --- a/src/common/framework/myCFG.ml +++ b/src/common/framework/myCFG.ml @@ -42,19 +42,36 @@ 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 + (** [skippedByEdge from edges to] returns the list of {{!GoblintCil.stmt} AST statements} skipped over by [find_real_stmt] in {!CfgTools.createCfg}. + This consists of statements which do not correspond to CFG nodes, but some surrounding AST constructions. *) +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 +81,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 3f4bd5e320..5f93e5c6ba 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 85f7db43b5..f3de153658 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/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..1b67dbf8a3 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -121,6 +121,12 @@ let serve serv = |> Seq.map Packet.t_of_yojson |> Seq.iter (handle_packet serv) +(** Is node valid for lookup by location? + Used for abstract debugging breakpoints. *) +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 +139,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 +254,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 +492,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..66d783c30f 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -79,7 +79,64 @@ struct emit_after_lock else emit_other + + let find_syntactic_loop_head = function + | Statement s -> + let n' = Statement (LoopUnrolling.find_original s) in + 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 + | FunctionEntry _ | Function _ -> None +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? i.e. exclude witness.invariant.loop-head check *) + 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 d9d39ccee1..513fa10a7a 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -165,17 +165,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 ) @@ -193,25 +204,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 @@ -254,30 +246,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 @@ -287,7 +275,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? needs both loop_invariant entry enabled and witness.invariant.loop-head option enabled *) 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 (||) *) @@ -309,7 +297,7 @@ struct ) else acc - ) (Lazy.force location2nodes) entries + ) (Lazy.force loop_nodes) entries ) else entries @@ -340,11 +328,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 *) @@ -392,47 +380,48 @@ 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 -> + 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 + end + | None -> acc ) lh entries ) @@ -449,30 +438,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 @@ -482,7 +467,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 (||) *) @@ -504,7 +489,7 @@ struct ) else acc - ) (Lazy.force location2nodes) invariants + ) (Lazy.force loop_nodes) invariants ) else invariants @@ -565,7 +550,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 @@ -581,19 +566,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 @@ -687,7 +669,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 -> @@ -727,7 +709,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 -> @@ -778,7 +760,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.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t index 81244d00f8..6ac093d2d5 100644 --- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -11,133 +11,176 @@ │ (body) ▼ ┌──────────────────────────────────────────────────────┐ - │ 11-unrolled-loop-invariant.c:2:7-2:12 │ - │ (11-unrolled-loop-invariant.c:2:7-2:12) │ + │ 11-unrolled-loop-invariant.c:2:3-2:12 │ + │ (11-unrolled-loop-invariant.c:2:7-2:12 (synthetic)) │ + │ YAML loc: 11-unrolled-loop-invariant.c:2:3-2:12 │ + │ GraphML: true; server: false │ └──────────────────────────────────────────────────────┘ │ │ i = 0 ▼ ┌──────────────────────────────────────────────────────┐ │ 11-unrolled-loop-invariant.c:3:3-4:8 (synthetic) │ - ┌───────────── │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic)) │ ·┐ + │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic)) │ + │ YAML loop: 11-unrolled-loop-invariant.c:3:3-4:8 │ + │ GraphML: true; server: false │ + ┌───────────── │ loop: 11-unrolled-loop-invariant.c:3:3-4:8 │ ·┐ │ └──────────────────────────────────────────────────────┘ : │ │ : │ │ Pos(i < 10) : │ ▼ : │ ┌──────────────────────────────────────────────────────┐ : │ │ 11-unrolled-loop-invariant.c:4:5-4:8 │ : - │ │ (11-unrolled-loop-invariant.c:4:5-4:8) │ ·┼··························································┐ - │ └──────────────────────────────────────────────────────┘ : : - │ │ : : - │ Neg(i < 10) │ i = i + 1 : : - │ ▼ ▼ : - │ ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : - │ │ 11-unrolled-loop-invariant.c:3:3-4:8 (synthetic) │ : - │ │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic)) │ : - │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : - │ │ │ ▲ : - │ │ Neg(i < 10) │ Pos(i < 10) │ i = i + 1 : - │ ▼ │ │ : - │ ┌──────────────────────────────────────────────────────┐ │ ┌─────────────────────────────────────────┐ : - │ │ 11-unrolled-loop-invariant.c:6:7-6:12 │ │ │ 11-unrolled-loop-invariant.c:4:5-4:8 │ : - └────────────▶ │ (11-unrolled-loop-invariant.c:6:7-6:12) │ └───────────▶ │ (11-unrolled-loop-invariant.c:4:5-4:8) │ ◀┘ - └──────────────────────────────────────────────────────┘ └─────────────────────────────────────────┘ + │ │ (11-unrolled-loop-invariant.c:4:5-4:8) │ : + │ │ YAML loc: 11-unrolled-loop-invariant.c:4:5-4:8 │ : + │ │ GraphML: true; server: true │ ·┼····································································┐ + │ └──────────────────────────────────────────────────────┘ : : + │ │ : : + │ │ i = i + 1 : : + │ Neg(i < 10) ▼ ▼ : + │ ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : + │ │ 11-unrolled-loop-invariant.c:3:3-4:8 (synthetic) │ : + │ │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic)) │ : + │ │ YAML loop: 11-unrolled-loop-invariant.c:3:3-4:8 │ : + │ │ GraphML: true; server: false │ : + │ │ loop: 11-unrolled-loop-invariant.c:3:3-4:8 │ : + │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : + │ │ │ ▲ : + │ │ Neg(i < 10) │ Pos(i < 10) │ i = i + 1 : + │ ▼ │ │ : + │ ┌──────────────────────────────────────────────────────┐ │ ┌───────────────────────────────────────────────────┐ : + │ │ 11-unrolled-loop-invariant.c:6:3-6:19 │ │ │ 11-unrolled-loop-invariant.c:4:5-4:8 │ : + │ │ (11-unrolled-loop-invariant.c:6:7-6:12 (synthetic)) │ │ │ (11-unrolled-loop-invariant.c:4:5-4:8) │ : + │ │ YAML loc: 11-unrolled-loop-invariant.c:6:3-6:19 │ │ │ YAML loc: 11-unrolled-loop-invariant.c:4:5-4:8 │ : + └────────────▶ │ GraphML: true; server: false │ └───────────▶ │ GraphML: true; server: true │ ◀┘ + └──────────────────────────────────────────────────────┘ └───────────────────────────────────────────────────┘ │ │ j = 0 ▼ ┌──────────────────────────────────────────────────────┐ - │ 11-unrolled-loop-invariant.c:6:14-6:19 │ - │ (11-unrolled-loop-invariant.c:6:14-6:19) │ + │ 11-unrolled-loop-invariant.c:6:3-6:19 (synthetic) │ + │ (11-unrolled-loop-invariant.c:6:14-6:19 (synthetic)) │ + │ GraphML: true; server: false │ └──────────────────────────────────────────────────────┘ │ │ k = 0 ▼ - ┌──────────────────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ ┌──────────────────┐ - │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic) │ Neg(j < 10) │ 11-unrolled-loop-invariant.c:12:3-12:11 │ return 0 │ return of main() │ - ┌············· │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic)) │ ─────────────▶ │ (unknown) │ ──────────▶ │ │ - : └──────────────────────────────────────────────────────┘ └─────────────────────────────────────────┘ └──────────────────┘ - : │ ▲ Neg(j < 10) - : │ Pos(j < 10) └────────────────────────────────────────────────────────────────────────────────┐ - : ▼ │ - : ┌──────────────────────────────────────────────────────┐ │ - : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ │ - ┌──────────────────────────┼───────────── │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ ····························································┐ │ - │ : └──────────────────────────────────────────────────────┘ : │ - │ : │ : │ - │ : │ Pos(k < 100) : │ - │ : ▼ : │ - │ : ┌──────────────────────────────────────────────────────┐ : │ - │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ - │ : │ (11-unrolled-loop-invariant.c:9:7-9:10) │ ····························································┼············┐ │ - │ : └──────────────────────────────────────────────────────┘ : : │ - │ : │ : : │ - │ : │ k = k + 1 ┌──────────────────────────────────────────┼────────────┼────────────────────────┼─────────────┐ - │ : ▼ │ : : │ │ - │ : ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : │ │ - │ : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : │ │ - │ : │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ : : │ │ - │ : └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : │ │ - │ : │ : ▲ : : │ │ - │ : │ Pos(k < 100) : │ k = k + 1 : : │ │ - │ : ▼ : │ : : │ │ - │ : ┌──────────────────────────────────────────────────────┐ : │ : : │ │ - │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ : : │ │ - │ : │ (11-unrolled-loop-invariant.c:9:7-9:10) │ ─┼───────────────┘ : : │ │ - │ : └──────────────────────────────────────────────────────┘ : : : │ │ - │ : : : : : │ │ - ┌────┘ : : : : : │ │ - │ : ▼ : : : │ │ - │ : ┌──────────────────────────────────────────────────────┐ : : : │ │ - │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : : : │ │ - │ ┌··························┼············▶ │ (11-unrolled-loop-invariant.c:9:7-9:10) │ ◀┼───────────────┐ : : │ │ - │ : : └──────────────────────────────────────────────────────┘ : │ : : │ │ - │ : : │ : │ : : │ │ - │ : : │ k = k + 1 : │ Pos(k < 100) : : │ │ - │ : : ▼ ▼ │ : : │ │ - │ : : ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : │ │ - │ : k = k + 1 : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : │ │ - │ : ┌─────────────────────┼────────────▶ │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ ◀┼············┼···················┐ │ │ - │ : │ : └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : : │ │ - │ : │ : │ : : : │ │ - │ : │ : │ Neg(k < 100) : : : │ │ - │ : │ : ▼ : : : │ │ - │ : │ : ┌──────────────────────────────────────────────────────┐ : : : │ │ - │ : │ : │ 11-unrolled-loop-invariant.c:10:5-10:8 │ : : : │ │ - │ : │ ┌────────────────┼────────────▶ │ (11-unrolled-loop-invariant.c:10:5-10:8) │ ◀···························································┼············┼···················┼····┼·············┼····┐ - │ : │ │ : └──────────────────────────────────────────────────────┘ : : : │ │ : - │ : │ │ : │ : : : │ │ : - │ : │ │ : │ j = j + 1 ┌──────────────────────────────────────────┼────────────┼───────────────────┼────┘ │ : - │ : │ │ : ▼ │ : : : │ : - │ : │ │ : ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : : │ : - │ : │ │ : │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic) │ : : : │ : - │ : │ │ Neg(k < 100) └············▶ │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic)) │ ◀┼────────────┼───────────────────┼────┐ │ : - │ : │ │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : : │ │ : - │ : │ │ │ : : : │ │ : - │ : │ │ │ Pos(j < 10) : : : │ │ : - │ : │ │ ▼ : : : │ │ : - │ : │ │ ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : : │ │ : - │ : │ │ │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : : │ │ : - │ : │ └────────────────────────────── │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ ◀┘ : : │ j = j + 1 │ : - │ : │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : │ │ : - │ : │ │ : : : │ │ : - │ : │ │ Pos(k < 100) └·······················································┼···················┘ │ │ : - │ : │ ▼ : │ │ : - │ : │ ┌──────────────────────────────────────────────────────┐ : │ │ : - │ : │ │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ │ : - │ : └─────────────────────────────────── │ (11-unrolled-loop-invariant.c:9:7-9:10) │ ◀········································································┘ ┌····┼·············┼····┘ - │ : └──────────────────────────────────────────────────────┘ : │ │ - │ : : : │ │ - │ └···········································┘ : │ │ - │ : │ │ - │ : │ │ - │ ┌···················································································································································┘ │ │ - │ : │ │ - │ ┌──────────────────────────────────────────────────────┐ │ │ - │ Neg(k < 100) │ 11-unrolled-loop-invariant.c:10:5-10:8 │ │ │ - └────────────────────────────────────────────▶ │ (11-unrolled-loop-invariant.c:10:5-10:8) │ ──────────────────────────────────────────────────────────────────────────────────────────────────┘ │ - └──────────────────────────────────────────────────────┘ │ - ▲ Neg(k < 100) │ - └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ + ┌──────────────────────────────────────────────────────┐ ┌───────────────────────────────────────────────────┐ ┌──────────────────┐ + │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic) │ │ 11-unrolled-loop-invariant.c:12:3-12:11 │ │ │ + │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic)) │ │ (11-unrolled-loop-invariant.c:12:10-12:11) │ │ │ + │ YAML loop: 11-unrolled-loop-invariant.c:7:3-11:3 │ │ YAML loc: 11-unrolled-loop-invariant.c:12:3-12:11 │ │ return of main() │ + │ GraphML: true; server: false │ Neg(j < 10) │ GraphML: true; server: true │ return 0 │ │ + ┌············· │ loop: 11-unrolled-loop-invariant.c:7:3-11:3 │ ─────────────▶ │ │ ──────────▶ │ │ + : └──────────────────────────────────────────────────────┘ └───────────────────────────────────────────────────┘ └──────────────────┘ + : │ ▲ Neg(j < 10) + : │ Pos(j < 10) └──────────────────────────────────────────────────────────────────────────────────────────┐ + : ▼ │ + : ┌──────────────────────────────────────────────────────┐ │ + : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ │ + : │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ │ + : │ YAML loop: 11-unrolled-loop-invariant.c:8:5-9:10 │ │ + : │ GraphML: true; server: false │ │ + ┌──────────────────────────┼───────────── │ loop: 11-unrolled-loop-invariant.c:8:5-9:10 │ ······································································┐ │ + │ : └──────────────────────────────────────────────────────┘ : │ + │ : │ : │ + │ : │ Pos(k < 100) : │ + │ : ▼ : │ + │ : ┌──────────────────────────────────────────────────────┐ : │ + │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ + │ : │ (11-unrolled-loop-invariant.c:9:7-9:10) │ : │ + │ : │ YAML loc: 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ + │ : │ GraphML: true; server: true │ ······································································┼············┐ │ + │ : └──────────────────────────────────────────────────────┘ : : │ + │ : │ : : │ + │ : │ k = k + 1 ┌────────────────────────────────────────────────────┼────────────┼────────────────────────┼─────────────┐ + │ : ▼ │ : : │ │ + │ : ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : │ │ + │ : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : │ │ + │ : │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ : : │ │ + │ : │ YAML loop: 11-unrolled-loop-invariant.c:8:5-9:10 │ : : │ │ + │ : │ GraphML: true; server: false │ : : │ │ + │ : │ loop: 11-unrolled-loop-invariant.c:8:5-9:10 │ : : │ │ + │ : └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : │ │ + │ : │ : ▲ : : │ │ + │ : │ Pos(k < 100) : │ k = k + 1 : : │ │ + │ : ▼ : │ : : │ │ + │ : ┌──────────────────────────────────────────────────────┐ : │ : : │ │ + │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ : : │ │ + │ : │ (11-unrolled-loop-invariant.c:9:7-9:10) │ : │ : : │ │ + │ : │ YAML loc: 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ : : │ │ + │ : │ GraphML: true; server: true │ ─┼───────────────┘ : : │ │ + │ : └──────────────────────────────────────────────────────┘ : : : │ │ + │ : : : : : │ │ + ┌────┘ : : : : : │ │ + │ : ▼ : : : │ │ + │ : ┌──────────────────────────────────────────────────────┐ : : : │ │ + │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : : : │ │ + │ : │ (11-unrolled-loop-invariant.c:9:7-9:10) │ : : : │ │ + │ : │ YAML loc: 11-unrolled-loop-invariant.c:9:7-9:10 │ : : : │ │ + │ ┌··························┼············▶ │ GraphML: true; server: true │ ◀┼───────────────┐ : : │ │ + │ : : └──────────────────────────────────────────────────────┘ : │ : : │ │ + │ : : │ : │ : : │ │ + │ : : │ k = k + 1 : │ Pos(k < 100) : : │ │ + │ : : ▼ ▼ │ : : │ │ + │ : : ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : │ │ + │ : : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : │ │ + │ : : │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ : : │ │ + │ : : │ YAML loop: 11-unrolled-loop-invariant.c:8:5-9:10 │ : : │ │ + │ : k = k + 1 : │ GraphML: true; server: false │ : : │ │ + │ : ┌─────────────────────┼────────────▶ │ loop: 11-unrolled-loop-invariant.c:8:5-9:10 │ ◀┼············┼···················┐ │ │ + │ : │ : └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : : │ │ + │ : │ : │ : : : │ │ + │ : │ : │ Neg(k < 100) : : : │ │ + │ : │ : ▼ : : : │ │ + │ : │ : ┌──────────────────────────────────────────────────────┐ : : : │ │ + │ : │ : │ 11-unrolled-loop-invariant.c:10:5-10:8 │ : : : │ │ + │ : │ : │ (11-unrolled-loop-invariant.c:10:5-10:8) │ : : : │ │ + │ : │ : │ YAML loc: 11-unrolled-loop-invariant.c:10:5-10:8 │ : : : │ │ + │ : │ ┌────────────────┼────────────▶ │ GraphML: true; server: true │ ◀·····································································┼············┼···················┼····┼·············┼····┐ + │ : │ │ : └──────────────────────────────────────────────────────┘ : : : │ │ : + │ : │ │ : │ : : : │ │ : + │ : │ │ : │ j = j + 1 ┌────────────────────────────────────────────────────┼────────────┼───────────────────┼────┘ │ : + │ : │ │ : ▼ │ : : : │ : + │ : │ │ : ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : : │ : + │ : │ │ : │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic) │ : : : │ : + │ : │ │ : │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic)) │ : : : │ : + │ : │ │ Neg(k < 100) : │ YAML loop: 11-unrolled-loop-invariant.c:7:3-11:3 │ : : : │ : + │ : │ │ : │ GraphML: true; server: false │ : : : │ : + │ : │ │ └············▶ │ loop: 11-unrolled-loop-invariant.c:7:3-11:3 │ ◀┼────────────┼───────────────────┼────┐ │ : + │ : │ │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : : │ │ : + │ : │ │ │ : : : │ │ : + │ : │ │ │ Pos(j < 10) : : : │ │ : + │ : │ │ ▼ : : : │ │ : + │ : │ │ ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : : │ │ : + │ : │ │ │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : : │ │ : + │ : │ │ │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ : : : │ │ : + │ : │ │ │ YAML loop: 11-unrolled-loop-invariant.c:8:5-9:10 │ : : : │ j = j + 1 │ : + │ : │ │ │ GraphML: true; server: false │ : : : │ │ : + │ : │ └────────────────────────────── │ loop: 11-unrolled-loop-invariant.c:8:5-9:10 │ ◀┘ : : │ │ : + │ : │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : │ │ : + │ : │ │ : : : │ │ : + │ : │ │ Pos(k < 100) └·································································┼···················┘ │ │ : + │ : │ ▼ : │ │ : + │ : │ ┌──────────────────────────────────────────────────────┐ : │ │ : + │ : │ │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ │ : + │ : │ │ (11-unrolled-loop-invariant.c:9:7-9:10) │ : │ │ : + │ : │ │ YAML loc: 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ │ : + │ : └─────────────────────────────────── │ GraphML: true; server: true │ ◀··················································································┘ ┌····┼·············┼····┘ + │ : └──────────────────────────────────────────────────────┘ : │ │ + │ : : : │ │ + │ └···········································┘ : │ │ + │ : │ │ + │ : │ │ + │ ┌·····························································································································································┘ │ │ + │ : │ │ + │ ┌──────────────────────────────────────────────────────┐ │ │ + │ │ 11-unrolled-loop-invariant.c:10:5-10:8 │ │ │ + │ │ (11-unrolled-loop-invariant.c:10:5-10:8) │ │ │ + │ Neg(k < 100) │ YAML loc: 11-unrolled-loop-invariant.c:10:5-10:8 │ │ │ + └────────────────────────────────────────────▶ │ GraphML: true; server: true │ ────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ + └──────────────────────────────────────────────────────┘ │ + ▲ Neg(k < 100) │ + └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 11-unrolled-loop-invariant.c [Info] unrolling loop at 11-unrolled-loop-invariant.c:3:3-4:8 with factor 5 @@ -168,16 +211,14 @@ [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:12-8:19) [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:7:10-7:16) [Info][Witness] witness generation summary: - total generation entries: 19 + total generation entries: 17 TODO: use yamlWitnessStrip for this + $ cat witness.yml | grep -A 1 'value:' value: i == 10 format: c_expression - -- - value: i == 10 - format: c_expression -- value: j == 10 format: c_expression @@ -208,18 +249,15 @@ TODO: use yamlWitnessStrip for this -- value: i == 10 format: c_expression - -- - value: j == 0 - format: c_expression - -- - value: (((((5 <= i && i <= 10) || i == 4) || i == 3) || i == 2) || i == 1) || - i == 0 -- value: i == 10 format: c_expression -- value: (((((((k == 100 && (((j == 2 || (5 <= j && j <= 9)) || j == 1) || j == 4)) || ((5 <= k && k <= 100) && j == 0)) || (j == 0 && k == 4)) || (j == 0 + -- + value: (((((5 <= i && i <= 10) || i == 4) || i == 3) || i == 2) || i == 1) || + i == 0 -- value: i == 10 format: c_expression 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 1dc21aeacc..5e35fbc911 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 @@ -19,7 +19,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 c0473adecb..06bae19e07 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 @@ -17,9 +17,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 2ccf85fdd2..49bd9b028b 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 @@ -19,7 +19,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 f82c321f73..39fa14eb23 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 @@ -19,7 +19,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 530ae08906..4d7b98fd17 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 @@ -17,9 +17,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 9ec4a7845a..64e1b79f16 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 @@ -19,7 +19,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 8a55e96e3a..cfd80c21c8 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 @@ -19,7 +19,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 c20801d044..d51aa91699 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 @@ -19,7 +19,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 336657e52d..5ade41e167 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 @@ -19,7 +19,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/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index a9f91bf4a6..ba7720d81f 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -1,48 +1,59 @@ $ 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 │ ─┘ + └───────────────────────────────┘ diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t index 78a81aff68..195b29deef 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,4 @@ ┌─────────────────────────────────────────┐ │ return of minus() │ └─────────────────────────────────────────┘ + diff --git a/tests/regression/cfg/loops.t/loops.c b/tests/regression/cfg/loops.t/loops.c new file mode 100644 index 0000000000..0e038e1898 --- /dev/null +++ b/tests/regression/cfg/loops.t/loops.c @@ -0,0 +1,45 @@ +#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 two initializers + for (int j = (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..bd9ec42307 --- /dev/null +++ b/tests/regression/cfg/loops.t/run.t @@ -0,0 +1,190 @@ + $ 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:8-34:23 │ │ + │ (loops.c:29:7-29:21 (synthetic)) │ │ (loops.c:34:12-34:23 (synthetic)) │ │ + │ GraphML: true; server: false │ │ YAML loc: loops.c:34:8-34:23 │ │ + │ │ │ GraphML: true; server: false │ │ + └───────────────────────────────────┘ └───────────────────────────────────┘ │ + │ │ │ + │ │ i = 0 │ + │ ▼ │ + │ ┌───────────────────────────────────┐ │ + │ │ loops.c:34:8-34:23 (synthetic) │ │ + │ │ (loops.c:34:12-34:23 (synthetic)) │ │ + │ │ GraphML: true; server: false │ │ + │ └───────────────────────────────────┘ │ + │ │ │ + ┌────┘ │ j = i │ + │ ▼ │ + │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ + │ │ loops.c:35:5-35:23 │ │ loops.c:34:3-36:3 (synthetic) │ │ + │ │ (loops.c:35:5-35:23) │ │ (loops.c:34:7-34:36 (synthetic)) │ │ + │ │ YAML loc: loops.c:35:5-35:23 │ │ YAML loop: loops.c:34:3-36:3 │ │ + │ │ GraphML: true; server: true │ Pos(i < 10) │ GraphML: true; server: false │ i = i + 1 │ + │ │ │ ◀───────────── │ loop: loops.c:34:3-36:3 │ ◀─────────────────────┼────┐ + │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ __goblint_check(1) │ Neg(i < 10) │ │ + │ ▼ ▼ │ │ + │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ + │ │ loops.c:34:8-34:23 (synthetic) │ │ loops.c:39:3-39:8 │ │ │ + │ │ (loops.c:34:12-34:23 (synthetic)) │ │ (loops.c:39:3-39:8) │ │ │ + │ │ GraphML: true; server: false │ │ YAML loc: loops.c:39:3-39:8 │ │ │ + │ │ │ ─┐ │ GraphML: true; server: true │ │ │ + │ └───────────────────────────────────┘ │ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ │ i = 0 │ │ + │ │ ▼ │ │ + │ │ ┌───────────────────────────────────┐ │ │ + │ │ │ loops.c:41:5-41:8 │ │ │ + │ │ │ (loops.c:41:5-41:8) │ │ │ + │ │ │ YAML loc: loops.c:41:5-41:8 │ │ │ + │ │ │ YAML loop: loops.c:40:3-42:19 │ │ │ + │ │ │ GraphML: true; server: true │ │ │ + │ │ │ loop: loops.c:40:3-42:19 │ ◀┐ │ │ + │ │ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ + │ │ │ i = i + 1 │ Pos(i < 10) │ │ + │ │ ▼ │ │ │ + │ │ ┌───────────────────────────────────┐ │ │ │ + │ │ │ loops.c:40:3-42:19 (synthetic) │ │ │ │ + │ │ │ (loops.c:42:12-42:19 (synthetic)) │ │ │ │ + │ │ │ GraphML: true; server: false │ ─┘ │ │ + │ │ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ │ Neg(i < 10) │ │ + │ │ ▼ │ │ + │ │ ┌───────────────────────────────────┐ │ │ + │ │ │ loops.c:44:3-44:11 │ │ │ + │ │ │ (loops.c:44:10-44:11) │ │ │ + │ │ │ YAML loc: loops.c:44:3-44:11 │ │ │ + │ │ │ GraphML: true; server: true │ │ │ + │ │ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ │ return 0 │ │ + │ │ ▼ │ │ + │ │ ┌───────────────────────────────────┐ │ │ + │ │ │ return of main() │ │ │ + │ │ └───────────────────────────────────┘ │ │ + │ │ │ │ + └─────────────────────────────────────────┼─────────────────────────────────────────────────────────────────────────┘ │ + │ │ + │ │ + └──────────────────────────────────────────────────────────────────────────────┘ + + diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t index d87d9128c7..d05e5affcb 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,4 @@ ┌────────────────────────────────────┐ │ return of main() │ └────────────────────────────────────┘ + diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index 7eb7cb27c1..a58029086a 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -17,10 +17,14 @@ let main () = Cilfacade.init (); GobConfig.set_bool "dbg.cfg.loop-unrolling" true; GobConfig.set_int "exp.unrolling-factor" !unroll; + GobConfig.set_bool "witness.invariant.loop-head" true; + GobConfig.set_bool "witness.invariant.after-lock" true; + GobConfig.set_bool "witness.invariant.other" true; assert (List.length !files = 1); let ast = Cilfacade.getAST (Fpath.v (List.hd !files)) in CilCfg0.end_basic_blocks ast; + Cilfacade.current_file := ast; (* Part of CilCfg.createCFG *) GoblintCil.iterGlobals ast (function | GFun (fd, _) -> @@ -31,6 +35,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 @@ -49,12 +62,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 fe03f7a3ec..fb3c5e6899 100644 --- a/tests/regression/cfg/util/dune +++ b/tests/regression/cfg/util/dune @@ -4,7 +4,7 @@ goblint-cil goblint_logs goblint_common - goblint_lib ; TODO: avoid: extract LoopUnrolling from goblint_lib + goblint_lib ; TODO: avoid: extract LoopUnrolling and WitnessUtil node predicates from goblint_lib fpath goblint.sites.dune goblint.build-info.dune)