From 8156c1856eaa69033deef2f94e8beb6be8b17579 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Thu, 8 Oct 2026 14:35:37 +0800 Subject: [PATCH 1/3] Fix ghost insertion and list recursive logic Inserting a ghost declaration, assignment, else-branch assignment or label rebuilt the CFG without Ast.mark_as_changed, so WP's per-function cache, which depends on Ast.self, kept proving the body as it was before the insertion. Every body edit now ends in commit_body_edit, which rebuilds and invalidates together. Ghost locals go into the blocals of the block holding them, with vdefined set, which Filecheck requires. Names in ghost expressions resolve through the enclosing blocks, then formals, then globals, instead of any local of the function. Mutating requests run Filecheck when AST_UTILS_CHECK_AST is set, and the regressions load the plug-in this tree built, with the check on. getRecursiveLogic lists recursive logic definitions with their components, because WP assumes each one without checking that it terminates. execSetWpConfig takes a step budget, and the ghost registries, written and never read, are gone. --- ast-utils/src/ast_utils_ast.ml | 113 +++++++ ast-utils/src/ast_utils_ghost.ml | 316 ++++++++++-------- ast-utils/src/ast_utils_register.ml | 122 ++++++- ast-utils/test/dune | 55 ++- ast-utils/test/regressions/ghost-integrity.c | 43 +++ ast-utils/test/regressions/recursive-logic.c | 40 +++ .../test/regressions/run-ghost-integrity.sh | 198 +++++++++++ .../test/regressions/run-recursive-logic.sh | 111 ++++++ .../test/regressions/with-built-plugin.sh | 33 ++ 9 files changed, 869 insertions(+), 162 deletions(-) create mode 100644 ast-utils/test/regressions/ghost-integrity.c create mode 100644 ast-utils/test/regressions/recursive-logic.c create mode 100755 ast-utils/test/regressions/run-ghost-integrity.sh create mode 100755 ast-utils/test/regressions/run-recursive-logic.sh create mode 100755 ast-utils/test/regressions/with-built-plugin.sh diff --git a/ast-utils/src/ast_utils_ast.ml b/ast-utils/src/ast_utils_ast.ml index 4219cc7..0ceefd3 100644 --- a/ast-utils/src/ast_utils_ast.ml +++ b/ast-utils/src/ast_utils_ast.ml @@ -1257,3 +1257,116 @@ let get_contract_context (kf : kernel_function) : Yojson.Basic.t = ("unresolved_callees", `List unresolved_callees); ("callee_resolution_complete", `Bool (unresolved_callees = [])); ] + +(* ====== Recursive logic definitions ====== *) + +class logic_uses_visitor (uses : (int, unit) Hashtbl.t) = object + inherit Cil.nopCilVisitor + + method! vlogic_info_use li = + Hashtbl.replace uses li.l_var_info.lv_id (); + DoChildren +end + +(** Every ACSL logic function or predicate defined with a body that is + recursive, directly or through others. + + WP turns such a definition into an axiom and never asks whether the + recursion terminates, so a definition like "bad(n) = bad(n) + 1" is an + inconsistent axiom from which any goal follows. This lists them; it does not + try to decide termination. + + Nodes are the definitions whose body is a term or a predicate, found at top + level and inside axiomatic blocks and modules. Inductive predicates are not + nodes: they denote least fixpoints, which are consistent by construction. An + edge goes from a definition to every node its body mentions, and a node is + reported when its strongly connected component has more than one member or + it mentions itself. "cycle" is that component in source order. *) +let get_recursive_logic () : Yojson.Basic.t = + let seen = Hashtbl.create 16 in + let defs = ref [] in + let rec collect = function + | Dfun_or_pred (li, loc) -> + (match li.l_body with + | LBterm _ | LBpred _ when not (Hashtbl.mem seen li.l_var_info.lv_id) -> + Hashtbl.replace seen li.l_var_info.lv_id (); + defs := (li, loc) :: !defs + | _ -> ()) + | Daxiomatic (_, inner, _, _) -> List.iter collect inner + | Dmodule (_, inner, _, _, _) -> List.iter collect inner + | _ -> () + in + Annotations.iter_global (fun _ ga -> collect ga); + let by_position (a, la) (b, lb) = + compare + (Ast_utils_compat.loc_file la, Ast_utils_compat.loc_line la, + a.l_var_info.lv_name) + (Ast_utils_compat.loc_file lb, Ast_utils_compat.loc_line lb, + b.l_var_info.lv_name) + in + let defs = Array.of_list (List.sort by_position !defs) in + let n = Array.length defs in + let index_of = Hashtbl.create n in + Array.iteri (fun i (li, _) -> Hashtbl.replace index_of li.l_var_info.lv_id i) + defs; + let succs = Array.map (fun (li, _) -> + let uses = Hashtbl.create 8 in + let vis = new logic_uses_visitor uses in + (match li.l_body with + | LBterm t -> ignore (Cil.visitCilTerm (vis :> Cil.cilVisitor) t) + | LBpred p -> ignore (Cil.visitCilPredicate (vis :> Cil.cilVisitor) p) + | _ -> ()); + Hashtbl.fold (fun id () acc -> + match Hashtbl.find_opt index_of id with + | Some j -> j :: acc + | None -> acc) uses [] + |> List.sort_uniq compare + ) defs in + (* Tarjan's strongly connected components. *) + let index = Array.make n (-1) and low = Array.make n 0 in + let on_stack = Array.make n false and stack = ref [] in + let counter = ref 0 and comp = Array.make n (-1) and ncomp = ref 0 in + let rec visit v = + index.(v) <- !counter; low.(v) <- !counter; incr counter; + stack := v :: !stack; on_stack.(v) <- true; + List.iter (fun w -> + if index.(w) < 0 then begin + visit w; low.(v) <- min low.(v) low.(w) + end else if on_stack.(w) then + low.(v) <- min low.(v) index.(w)) succs.(v); + if low.(v) = index.(v) then begin + let rec pop () = + match !stack with + | w :: rest -> + stack := rest; on_stack.(w) <- false; comp.(w) <- !ncomp; + if w <> v then pop () + | [] -> () + in + pop (); incr ncomp + end + in + for v = 0 to n - 1 do if index.(v) < 0 then visit v done; + (* Members bucketed once after the walk, in source order, rather than + rebuilt by scanning every definition for each one, which made even an + acyclic program quadratic in its logic definitions. *) + let buckets = Array.make (max 1 !ncomp) [] in + for i = n - 1 downto 0 do + buckets.(comp.(i)) <- i :: buckets.(comp.(i)) + done; + let members c = buckets.(c) in + let recursive v = + List.mem v succs.(v) || List.compare_length_with (members comp.(v)) 1 > 0 in + let name i = (fst defs.(i)).l_var_info.lv_name in + let definitions = + List.filter recursive (List.init n Fun.id) + |> List.map (fun i -> + let li, loc = defs.(i) in + `Assoc [ + ("name", `String (name i)); + ("kind", `String (if li.l_type = None then "predicate" else "function")); + ("file", `String (Ast_utils_compat.loc_file loc)); + ("line", `Int (Ast_utils_compat.loc_line loc)); + ("cycle", `List (List.map (fun j -> `String (name j)) (members comp.(i)))); + ]) + in + `Assoc [("definitions", `List definitions)] diff --git a/ast-utils/src/ast_utils_ghost.ml b/ast-utils/src/ast_utils_ghost.ml index 76763e0..fa44f8a 100644 --- a/ast-utils/src/ast_utils_ghost.ml +++ b/ast-utils/src/ast_utils_ghost.ml @@ -1,12 +1,22 @@ -(** ast_utils_ghost.ml — Ghost statement insertion/removal via direct CIL construction. +(** ast_utils_ghost.ml: ghost code insertion via direct CIL construction. Provides: - - Type name resolution (string → CIL typ) - - Simple C expression parser (recursive descent) - - Ghost variable declaration insertion - - Ghost assignment insertion - - Ghost global variable insertion/removal - - Ghost statement/variable removal with registry tracking + - Type name resolution (string to CIL typ) + - Simple C expression parser (recursive descent), resolving names through + the blocks that enclose the insertion point, then formals, then globals + - Insertion of ghost globals, formals, lemma functions, local declarations, + assignments, empty-else assignments, labels and counting loops + + There is no removal: an inserted ghost goes away only by reloading the + project. Nothing records what was inserted either; the three registries + that once did were written and never read, and were removed. + + Every insertion that rewrites a function body rebuilds its CFG and calls + Ast.mark_as_changed, so states computed from the old body, WP's + per-function CFG cache among them, are recomputed. A ghost local is listed + both in the function's slocals and in the blocals of the block holding its + declaration, with vdefined set, which is what Filecheck expects of a + Local_init. All inserted statements have stmt.ghost = true and target variables have vghost = true, ensuring soundness (no effect on program semantics). *) @@ -14,19 +24,6 @@ open Frama_c_kernel open Cil_types -(* ====== Ghost Registry ====== *) - -(* key: (function_name, var_name), value: sids of statements we inserted *) -let ghost_registry : (string * string, int list) Hashtbl.t = - Hashtbl.create 16 - -(* key: function_name, value: statement-only ghost insert sids *) -let ghost_stmt_registry : (string, int list) Hashtbl.t = - Hashtbl.create 16 - -let ghost_global_registry : (string, varinfo) Hashtbl.t = - Hashtbl.create 16 - let is_valid_c_identifier name = let len = String.length name in len > 0 && @@ -166,74 +163,141 @@ let peek ls = ls.pos <- saved; tok -let find_var_in_fundec fundec name = - try List.find (fun vi -> vi.vname = name) fundec.slocals - with Not_found -> - try List.find (fun vi -> vi.vname = name) fundec.sformals - with Not_found -> - try Globals.Vars.find_from_astinfo name Global - with Not_found -> - failwith (Printf.sprintf "unknown variable '%s'" name) +(* The blocks enclosing the statement with this sid, innermost first, each + paired with its statements that precede the one leading to the target. None + when the body does not contain it. A walk over the body rather than + Kernel_function.find_all_enclosing_blocks, because the kernel's statement + tables do not know a statement inserted since the last Ast.mark_as_changed. *) +let enclosing_blocks fundec target_sid = + let rec in_block acc b = + let rec scan before = function + | [] -> None + | s :: rest -> + if s.sid = target_sid then Some ((b, List.rev before) :: acc) + else + match in_stmt ((b, List.rev before) :: acc) s with + | Some _ as found -> found + | None -> scan (s :: before) rest + in + scan [] b.bstmts + and in_stmt acc s = + match s.skind with + | If (_, tb, fb, _) -> + (match in_block acc tb with + | Some _ as found -> found + | None -> in_block acc fb) + | Loop (_, b, _, _, _) | Block b | Switch (_, b, _, _) -> in_block acc b + | UnspecifiedSequence seq -> + List.find_map (fun (s, _, _, _, _) -> + if s.sid = target_sid then Some acc else in_stmt acc s) seq + | _ -> None + in + in_block [] fundec.sbody + +(* Whether stmt is the Local_init of vi, the statement C scope starts at. *) +let rec initializes vi stmt = + match stmt.skind with + | Instr (Local_init (v, _, _)) -> v.vid = vi.vid + | UnspecifiedSequence seq -> + List.exists (fun (s, _, _, _, _) -> initializes vi s) seq + | _ -> false + +(* Resolve a C name as it reads at the statement with this sid: the locals of + the enclosing blocks, innermost first, then the formals, then the globals. + A block local with an initializer is visible only once that initializer has + run, since CIL lists every local at the top of its block whatever its C + scope. Within a block the CIL name wins over the source name, so "t_0" and + "t" both reach a second "t" CIL renamed, and neither reaches a sibling + block. *) +let find_var_in_scope fundec target_sid name = + let blocks = + match enclosing_blocks fundec target_sid with + | Some blocks -> blocks + | None -> + failwith (Printf.sprintf "statement %d not found in function body" + target_sid) + in + let in_block (b, before) = + let visible vi = + (not vi.vdefined) || List.exists (initializes vi) before in + let named f = List.find_opt (fun vi -> f vi && visible vi) b.blocals in + match named (fun vi -> vi.vname = name) with + | Some _ as found -> found + | None -> named (fun vi -> vi.vorig_name = name) + in + match List.find_map in_block blocks with + | Some vi -> vi + | None -> + match List.find_opt (fun vi -> vi.vname = name) fundec.sformals with + | Some vi -> vi + | None -> + try Globals.Vars.find_from_astinfo name Global + with Not_found -> + if List.exists (fun vi -> vi.vname = name) fundec.slocals then + failwith (Printf.sprintf + "variable '%s' is not in scope at statement %d" name target_sid) + else + failwith (Printf.sprintf "unknown variable '%s'" name) -let rec parse_expr_impl ls fundec loc = - parse_additive ls fundec loc +let rec parse_expr_impl ls lookup loc = + parse_additive ls lookup loc -and parse_additive ls fundec loc = - let left = ref (parse_multiplicative ls fundec loc) in +and parse_additive ls lookup loc = + let left = ref (parse_multiplicative ls lookup loc) in let cont = ref true in while !cont do match peek ls with | TkPlus -> ignore (next_token ls); left := Ast_utils_compat.mk_binop ~loc PlusA !left - (parse_multiplicative ls fundec loc) + (parse_multiplicative ls lookup loc) | TkMinus -> ignore (next_token ls); left := Ast_utils_compat.mk_binop ~loc MinusA !left - (parse_multiplicative ls fundec loc) + (parse_multiplicative ls lookup loc) | _ -> cont := false done; !left -and parse_multiplicative ls fundec loc = - let left = ref (parse_unary ls fundec loc) in +and parse_multiplicative ls lookup loc = + let left = ref (parse_unary ls lookup loc) in let cont = ref true in while !cont do match peek ls with | TkStar -> ignore (next_token ls); left := Ast_utils_compat.mk_binop ~loc Mult !left - (parse_unary ls fundec loc) + (parse_unary ls lookup loc) | TkSlash -> ignore (next_token ls); left := Ast_utils_compat.mk_binop ~loc Div !left - (parse_unary ls fundec loc) + (parse_unary ls lookup loc) | TkPercent -> ignore (next_token ls); left := Ast_utils_compat.mk_binop ~loc Mod !left - (parse_unary ls fundec loc) + (parse_unary ls lookup loc) | _ -> cont := false done; !left -and parse_unary ls fundec loc = +and parse_unary ls lookup loc = match peek ls with | TkMinus -> ignore (next_token ls); - let e = parse_unary ls fundec loc in + let e = parse_unary ls lookup loc in Cil.new_exp ~loc (UnOp (Neg, e, Cil.typeOf e)) - | _ -> parse_primary ls fundec loc + | _ -> parse_primary ls lookup loc -and parse_primary ls fundec loc = +and parse_primary ls lookup loc = match next_token ls with | TkInt n -> Cil.integer ~loc n | TkIdent name -> - let vi = find_var_in_fundec fundec name in + let vi = lookup name in (match peek ls with | TkLBracket -> ignore (next_token ls); - let idx = parse_expr_impl ls fundec loc in + let idx = parse_expr_impl ls lookup loc in (match next_token ls with | TkRBracket -> () | _ -> failwith (Printf.sprintf @@ -250,7 +314,7 @@ and parse_primary ls fundec loc = | _ -> Cil.evar ~loc vi) | TkLParen -> - let e = parse_expr_impl ls fundec loc in + let e = parse_expr_impl ls lookup loc in (match next_token ls with | TkRParen -> () | _ -> failwith (Printf.sprintf @@ -262,13 +326,17 @@ and parse_primary ls fundec loc = failwith (Printf.sprintf "parse error: unexpected token at position %d" ls.pos) -let parse_c_expr fundec loc expr_string = +(* Parse an expression as it reads just before stmt, which is where every + caller inserts the code that uses it. *) +let parse_c_expr fundec stmt expr_string = if String.length (String.trim expr_string) = 0 then Error "empty expression" else try + let loc = Cil_datatype.Stmt.loc stmt in + let lookup = find_var_in_scope fundec stmt.sid in let ls = mk_lexer expr_string in - let e = parse_expr_impl ls fundec loc in + let e = parse_expr_impl ls lookup loc in (match peek ls with | TkEof -> Ok e | _ -> Error (Printf.sprintf @@ -296,30 +364,37 @@ let rebuild_cfg fundec = Cfg.clearCFGinfo ~clear_id:false fundec; Cfg.cfgFun fundec -(* Insert new_stmt before target_sid in the function body (recursive) *) +(* The end of every finished body edit: rebuild the CFG and invalidate what was + computed from the old body. WP keeps a per-function cache that depends on + Ast.self, so an edit that rebuilt without marking left the next proof + running against the body as it was. One name for the pair, so a new + insertion cannot do half of it. rebuild_cfg alone is for the two paths that + mark later on purpose, after typing an annotation or registering a + function. *) +let commit_body_edit fundec = + rebuild_cfg fundec; + Ast.mark_as_changed () + +(* Insert new_stmt before the statement with target_sid, searching nested + blocks. Returns the block that now holds both, or None when the body has no + such statement, in which case nothing was changed. *) let rec insert_in_block target_sid new_stmt b = - let found = ref false in - let new_bstmts = List.fold_right (fun s acc -> - if s.sid = target_sid then begin - found := true; - new_stmt :: s :: acc - end else begin - insert_in_skind target_sid new_stmt s.skind; - s :: acc - end - ) b.bstmts [] in - if !found then b.bstmts <- new_bstmts; - !found - -and insert_in_skind target_sid new_stmt = function + if List.exists (fun s -> s.sid = target_sid) b.bstmts then begin + b.bstmts <- List.concat_map + (fun s -> if s.sid = target_sid then [new_stmt; s] else [s]) b.bstmts; + Some b + end else + List.find_map (insert_in_stmt target_sid new_stmt) b.bstmts + +and insert_in_stmt target_sid new_stmt s = + match s.skind with | If (_, tb, fb, _) -> - ignore (insert_in_block target_sid new_stmt tb); - ignore (insert_in_block target_sid new_stmt fb) - | Loop (_, b, _, _, _) | Block b -> - ignore (insert_in_block target_sid new_stmt b) - | Switch (_, b, _, _) -> - ignore (insert_in_block target_sid new_stmt b) - | _ -> () + (match insert_in_block target_sid new_stmt tb with + | Some _ as found -> found + | None -> insert_in_block target_sid new_stmt fb) + | Loop (_, b, _, _, _) | Block b | Switch (_, b, _, _) -> + insert_in_block target_sid new_stmt b + | _ -> None (* Remove statements by sid list from the function body (recursive) *) let rec remove_from_block sids b = @@ -384,7 +459,6 @@ let insert_ghost_global name typ init = let file = Ast.get () in file.globals <- file.globals @ [global]; Globals.Vars.add vi initinfo; - Hashtbl.replace ghost_global_registry name vi; Ast.mark_as_changed (); Ok vi end @@ -500,7 +574,6 @@ let insert_ghost_formal kf name typ where = let insert_ghost_decl kf stmt var_name typ init_exp = try let fundec = Kernel_function.get_definition kf in - let kf_name = Kernel_function.get_name kf in (* Check for duplicate variable name *) let exists_in_locals = List.exists (fun vi -> vi.vname = var_name) fundec.slocals in @@ -519,26 +592,25 @@ let insert_ghost_decl kf stmt var_name typ init_exp = (* Create ghost local variable (insert:false = don't auto-add) *) let vi = Cil.makeLocalVar ~insert:false ~ghost:true ~loc fundec var_name typ in - (* Manually add to slocals *) - fundec.slocals <- fundec.slocals @ [vi]; (* Build Local_init instruction *) let init_instr = Local_init (vi, AssignInit (SingleInit cast_exp), loc) in let new_stmt = Cil.mkStmtOneInstr ~ghost:true ~valid_sid:true init_instr in (* Insert before target stmt *) - let inserted = insert_in_block stmt.sid new_stmt fundec.sbody in - if not inserted then + match insert_in_block stmt.sid new_stmt fundec.sbody with + | None -> Error (Printf.sprintf "statement %d not found in function body" stmt.sid) - else begin + | Some holder -> + (* Declared where it is initialized: the holding block's locals, with + vdefined set because a Local_init initializes it. *) + vi.vdefined <- true; + holder.blocals <- holder.blocals @ [vi]; + fundec.slocals <- fundec.slocals @ [vi]; fundec.sallstmts <- new_stmt :: fundec.sallstmts; - rebuild_cfg fundec; - (* Update registry *) - Hashtbl.replace ghost_registry - (kf_name, var_name) [new_stmt.sid]; + commit_body_edit fundec; Ok new_stmt - end end with | Kernel_function.No_Definition -> @@ -550,13 +622,8 @@ let insert_ghost_decl kf stmt var_name typ init_exp = let insert_ghost_assign kf stmt target_name expr = try let fundec = Kernel_function.get_definition kf in - let kf_name = Kernel_function.get_name kf in - (* Find the target ghost variable *) - let vi = - try List.find (fun vi -> vi.vname = target_name) fundec.slocals - with Not_found -> - failwith (Printf.sprintf "variable '%s' not found" target_name) - in + (* Find the target ghost variable as it reads at the insertion point *) + let vi = find_var_in_scope fundec stmt.sid target_name in if not vi.vghost then failwith (Printf.sprintf "variable '%s' is not a ghost variable" target_name); @@ -572,21 +639,14 @@ let insert_ghost_assign kf stmt target_name expr = let new_stmt = Cil.mkStmtOneInstr ~ghost:true ~valid_sid:true set_instr in (* Insert before target stmt *) - let inserted = insert_in_block stmt.sid new_stmt fundec.sbody in - if not inserted then + match insert_in_block stmt.sid new_stmt fundec.sbody with + | None -> Error (Printf.sprintf "statement %d not found in function body" stmt.sid) - else begin + | Some _ -> fundec.sallstmts <- new_stmt :: fundec.sallstmts; - rebuild_cfg fundec; - (* Update registry *) - let key = (kf_name, target_name) in - let existing = - try Hashtbl.find ghost_registry key - with Not_found -> [] in - Hashtbl.replace ghost_registry key (new_stmt.sid :: existing); + commit_body_edit fundec; Ok new_stmt - end with | Kernel_function.No_Definition -> Error (Printf.sprintf "function '%s' has no definition" @@ -597,17 +657,16 @@ let insert_ghost_assign kf stmt target_name expr = let insert_ghost_else_assign kf if_stmt target_name expr = try let fundec = Kernel_function.get_definition kf in - let kf_name = Kernel_function.get_name kf in - let vi = - try List.find (fun vi -> vi.vname = target_name) fundec.slocals - with Not_found -> - failwith (Printf.sprintf "variable '%s' not found" target_name) - in - if not vi.vghost then - failwith (Printf.sprintf - "variable '%s' is not a ghost variable" target_name); + (* The statement kind is checked before the name is resolved: a target + that is not an if is the more basic error, and resolving first answered + "not in scope" for a ghost declared by the target statement itself. *) match if_stmt.skind with | If (_, _, false_block, loc) -> + (* The else branch sees what the if statement sees *) + let vi = find_var_in_scope fundec if_stmt.sid target_name in + if not vi.vghost then + failwith (Printf.sprintf + "variable '%s' is not a ghost variable" target_name); if false_block.bstmts <> [] then Error "else_set requires an if statement with an empty else branch" else begin @@ -621,12 +680,7 @@ let insert_ghost_else_assign kf if_stmt target_name expr = Cil.mkStmtOneInstr ~ghost:true ~valid_sid:true set_instr in false_block.bstmts <- [new_stmt]; fundec.sallstmts <- new_stmt :: fundec.sallstmts; - rebuild_cfg fundec; - let key = (kf_name, target_name) in - let existing = - try Hashtbl.find ghost_registry key - with Not_found -> [] in - Hashtbl.replace ghost_registry key (new_stmt.sid :: existing); + commit_body_edit fundec; Ok new_stmt end | _ -> @@ -642,7 +696,6 @@ let insert_ghost_loop kf stmt var_name typ init_exp stop_exp step_exp invariant assigns variant assert_pred = try let fundec = Kernel_function.get_definition kf in - let kf_name = Kernel_function.get_name kf in let exists = List.exists (fun vi -> vi.vname = var_name) fundec.slocals || List.exists (fun vi -> vi.vname = var_name) fundec.sformals @@ -655,7 +708,7 @@ let insert_ghost_loop let loc = Cil_datatype.Stmt.loc stmt in let vi = Cil.makeLocalVar ~insert:false ~ghost:true ~loc fundec var_name typ in - fundec.slocals <- fundec.slocals @ [vi]; + vi.vdefined <- true; let cast_to_counter exp = if Cil_datatype.Typ.equal (Cil.typeOf exp) typ then exp else Cil.mkCast ~newt:typ exp @@ -696,14 +749,15 @@ let insert_ghost_loop post_assert := Some (stmt, pred); stmts := !stmts @ [stmt]); let block = Cil.mkBlock !stmts in + (* The counter is scoped to the ghost block that initializes it *) + block.blocals <- [vi]; let block_stmt = Cil.mkStmt ~ghost:true ~valid_sid:true (Block block) in force_stmt_ghost block_stmt; - let inserted = insert_in_block stmt.sid block_stmt fundec.sbody in - if not inserted then begin - fundec.slocals <- List.filter (fun v -> v.vid <> vi.vid) fundec.slocals; + match insert_in_block stmt.sid block_stmt fundec.sbody with + | None -> Error (Printf.sprintf "statement %d not found in function body" stmt.sid) - end - else begin + | Some _ -> + fundec.slocals <- fundec.slocals @ [vi]; let inserted_sids = collect_stmt_tree [] block_stmt |> List.map (fun s -> s.sid) in fundec.sallstmts <- collect_stmt_tree [] block_stmt @ fundec.sallstmts; @@ -715,7 +769,7 @@ let insert_ghost_loop fundec.sallstmts; fundec.slocals <- List.filter (fun v -> v.vid <> vi.vid) fundec.slocals; - rebuild_cfg fundec; + commit_body_edit fundec; Error msg in let loop_acsl = @@ -739,10 +793,8 @@ let insert_ghost_loop | None -> () | Some (stmt, _) -> Ast_utils_core.insert_annots kf stmt assert_annots); - Hashtbl.replace ghost_registry (kf_name, var_name) inserted_sids; Ast.mark_as_changed (); Ok (block_stmt, loop_stmt, vi, inserted_sids) - end end with | Kernel_function.No_Definition -> @@ -754,7 +806,6 @@ let insert_ghost_loop let insert_ghost_label kf stmt label_name = try let fundec = Kernel_function.get_definition kf in - let kf_name = Kernel_function.get_name kf in if not (is_valid_c_identifier label_name) then Error (Printf.sprintf "invalid label name '%s'" label_name) else if is_reserved_logic_label label_name then @@ -766,19 +817,14 @@ let insert_ghost_label kf stmt label_name = let loc = Cil_datatype.Stmt.loc stmt in let new_stmt = Cil.mkEmptyStmt ~ghost:true ~valid_sid:true ~loc () in new_stmt.labels <- [Label (label_name, loc, true)]; - let inserted = insert_in_block stmt.sid new_stmt fundec.sbody in - if not inserted then + match insert_in_block stmt.sid new_stmt fundec.sbody with + | None -> Error (Printf.sprintf "statement %d not found in function body" stmt.sid) - else begin + | Some _ -> fundec.sallstmts <- new_stmt :: fundec.sallstmts; - rebuild_cfg fundec; - let existing = - try Hashtbl.find ghost_stmt_registry kf_name - with Not_found -> [] in - Hashtbl.replace ghost_stmt_registry kf_name (new_stmt.sid :: existing); + commit_body_edit fundec; Ok new_stmt - end end with | Kernel_function.No_Definition -> diff --git a/ast-utils/src/ast_utils_register.ml b/ast-utils/src/ast_utils_register.ml index 3f31a75..f8e4793 100644 --- a/ast-utils/src/ast_utils_register.ml +++ b/ast-utils/src/ast_utils_register.ml @@ -19,6 +19,8 @@ - getLoopEffects: direct writes grouped by loop - getLogicDeps: ACSL logic dependencies by function contract and annotation - getRteObligations: generated RTE assertions with alarm metadata + - getRecursiveLogic: logic definitions that are directly or mutually + recursive, which WP assumes without a termination check - getWriteEffects: direct writes and direct callee assigns *) open Frama_c_kernel @@ -32,6 +34,69 @@ module Self = Plugin.Register (struct let help = "CIL AST JSON serialization and ACSL annotation manipulation" end) +(* ====== AST integrity check ====== *) + +module CheckAst = Self.False(struct + let option_name = "-ast-utils-check-ast" + let help = "Run the kernel's AST integrity check (Filecheck) after every \ + request that changes the AST, and report a failure as the \ + request's error. Also enabled by AST_UTILS_CHECK_AST set to \ + anything but empty or 0." +end) + +let check_ast_enabled () = + CheckAst.get () + || (match Sys.getenv_opt "AST_UTILS_CHECK_AST" with + | None | Some ("" | "0") -> false + | Some _ -> true) + +(* Filecheck reports through Kernel.fatal, which prints the reason and raises + an exception that carries only the plug-in name. The reason is taken from + the message stream instead, recorded only while a check runs. *) +let check_failure : string option ref = ref None +let checking = ref false + +let () = + Log.add_listener ~kind:[Log.Failure] (fun event -> + if !checking && !check_failure = None then + check_failure := Some (Rich_text.plain event.Log.evt_message)) + +(* Run Filecheck over the current AST after a mutating request, when enabled, + and turn a failure into the request's error. The mutation is not undone: the + point is to say that the AST is no longer one the kernel accepts, so the + caller reloads rather than proving against it. Fields the request already + returned are kept beside success = false and the error. *) +let checked_ast request (result : Json.t) : Json.t = + if not (check_ast_enabled ()) then result + else begin + check_failure := None; + checking := true; + let outcome = + try Filecheck.check_ast ("ast-utils " ^ request); None + with exn -> + Some (match !check_failure with + | Some reason -> reason + | None -> Printexc.to_string exn) + in + checking := false; + match outcome with + | None -> result + | Some reason -> + let msg = Printf.sprintf + "AST integrity check failed after %s; the AST is left modified \ + and the project should be reloaded: %s" + request + (String.concat " " + (List.filter (( <> ) "") + (String.split_on_char '\n' (String.trim reason)))) in + let kept = match result with + | `Assoc fields -> + List.filter (fun (k, _) -> k <> "success" && k <> "error") fields + | _ -> [] + in + `Assoc (("success", `Bool false) :: ("error", `String msg) :: kept) + end + (* ====== Helpers ====== *) let find_kf name = @@ -254,6 +319,21 @@ let () = with Kernel_function.No_Definition -> error_json (Printf.sprintf "function '%s' has no definition" name)) +(* getRecursiveLogic *) + +let () = + Server.Request.register + ~package + ~kind:`GET + ~name:"getRecursiveLogic" + ~descr:(Markdown.plain + "List ACSL logic functions and predicates whose definition is \ + recursive, directly or mutually. WP assumes such a definition \ + as an axiom without checking termination.") + ~input:(module Server.Data.Jany) + ~output:(module Server.Data.Jany) + (fun _ignored -> Ast_utils_ast.get_recursive_logic ()) + (* getRteObligations *) let () = @@ -379,7 +459,7 @@ let () = | Error msg -> ok_json [("success", `Bool false); ("error", `String msg)] in - set_result rq result) + set_result rq (checked_ast "execAddGlobalAcsl" result)) (* ====== execRemoveGlobalAcsl ====== *) @@ -407,7 +487,7 @@ let () = | Error msg -> ok_json [("success", `Bool false); ("error", `String msg)] in - set_result rq result) + set_result rq (checked_ast "execRemoveGlobalAcsl" result)) (* ====== execInsertGhostGlobal ====== *) @@ -451,7 +531,7 @@ let () = ok_json [("success", `Bool true); ("name", `String name); ("vid", `Int vi.vid); ("error", `Null)] in - set_result rq result) + set_result rq (checked_ast "execInsertGhostGlobal" result)) (* ====== execInsertGhostFormal ====== *) @@ -498,7 +578,7 @@ let () = ok_json [("success", `Bool true); ("name", `String name); ("vid", `Int vi.vid); ("error", `Null)] in - set_result rq result) + set_result rq (checked_ast "execInsertGhostFormal" result)) (* ====== execInsertGhostLemmaFunction ====== *) @@ -573,7 +653,7 @@ let () = ("sids", `List sids); ("error", `Null)] in - set_result rq result) + set_result rq (checked_ast "execInsertGhostLemmaFunction" result)) (* ====== execAddAnnotation ====== *) @@ -645,7 +725,7 @@ let () = | _ -> error_json (Printf.sprintf "unknown kind '%s', expected 'spec' or 'annot'" kind) in - set_result rq result) + set_result rq (checked_ast "execAddAnnotation" result)) (* ====== execRemoveAnnotations ====== *) @@ -659,6 +739,7 @@ let () = ~input:(module Server.Data.Jstring) ~output:(module Server.Data.Jany) (fun name -> + checked_ast "execRemoveAnnotations" @@ match find_kf name with | Error msg -> error_json msg | Ok kf -> @@ -698,7 +779,7 @@ let () = ok_json [("success", `Bool false); ("error", `String "annotation not found")] in - set_result rq result) + set_result rq (checked_ast "execRemoveAnnotationByLabel" result)) (* ====== execInsertGhostLoop ====== *) @@ -769,9 +850,8 @@ let () = with Kernel_function.No_Definition -> failwith "function has no definition" in - let loc = Cil_datatype.Stmt.loc stmt in let parse_expr field text = - match Ast_utils_ghost.parse_c_expr fundec loc text with + match Ast_utils_ghost.parse_c_expr fundec stmt text with | Ok exp -> Ok exp | Error msg -> Error (Printf.sprintf "%s: %s" field msg) in @@ -809,7 +889,7 @@ let () = ("sids", `List (List.map (fun sid -> `Int sid) sids)); ("error", `Null)] in - set_result rq result) + set_result rq (checked_ast "execInsertGhostLoop" result)) (* ====== execInsertGhostStmt ====== *) @@ -861,13 +941,12 @@ let () = with Kernel_function.No_Definition -> failwith "function has no definition" in - let loc = Cil_datatype.Stmt.loc stmt in match op with | "decl" -> (match Ast_utils_ghost.resolve_ghost_type type_name with | Error msg -> error_json msg | Ok typ -> - match Ast_utils_ghost.parse_c_expr fundec loc expr_str with + match Ast_utils_ghost.parse_c_expr fundec stmt expr_str with | Error msg -> error_json msg | Ok init_exp -> match Ast_utils_ghost.insert_ghost_decl @@ -881,7 +960,7 @@ let () = ("sid", `Int new_stmt.sid); ("error", `Null)]) | "set" -> - (match Ast_utils_ghost.parse_c_expr fundec loc expr_str with + (match Ast_utils_ghost.parse_c_expr fundec stmt expr_str with | Error msg -> error_json msg | Ok expr -> match Ast_utils_ghost.insert_ghost_assign @@ -895,7 +974,7 @@ let () = ("sid", `Int new_stmt.sid); ("error", `Null)]) | "else_set" -> - (match Ast_utils_ghost.parse_c_expr fundec loc expr_str with + (match Ast_utils_ghost.parse_c_expr fundec stmt expr_str with | Error msg -> error_json msg | Ok expr -> match Ast_utils_ghost.insert_ghost_else_assign @@ -923,7 +1002,7 @@ let () = error_json (Printf.sprintf "unknown op '%s', expected 'decl', 'set', 'label', or 'else_set'" op) in - set_result rq result) + set_result rq (checked_ast "execInsertGhostStmt" result)) (* ====== getVcDetails ====== *) @@ -1085,6 +1164,10 @@ let () = ~name:"par" ~descr:(Markdown.plain "Number of parallel WP prover processes") (module Server.Data.Jint) in + let get_steps = Server.Request.param_opt s + ~name:"steps" ~descr:(Markdown.plain + "Prover step budget; 0 means no step limit") + (module Server.Data.Jint) in let set_result = Server.Request.result s ~name:"result" ~descr:(Markdown.plain "Configuration result") (module Server.Data.Jany) in @@ -1121,6 +1204,13 @@ let () = Wp.Wp_parameters.Procs.set p; changed := ("par", `Int p) :: !changed | None -> ()); + (match get_steps rq with + | Some n -> + if n < 0 then + invalid_arg "steps must not be negative"; + Wp.Wp_parameters.Steps.set n; + changed := ("steps", `Int n) :: !changed + | None -> ()); set_result rq (ok_json [("success", `Bool true); ("changed", `List (List.map (fun (k, v) -> @@ -1140,6 +1230,7 @@ let () = ~input:(module Server.Data.Jstring) ~output:(module Server.Data.Jany) (fun name -> + checked_ast "execCreateSandbox" @@ match find_kf name with | Error msg -> error_json msg | Ok kf -> @@ -1164,6 +1255,7 @@ let () = ~input:(module Server.Data.Jstring) ~output:(module Server.Data.Jany) (fun sandbox_name -> + checked_ast "execDeleteSandbox" @@ match Ast_utils_sandbox.delete_sandbox sandbox_name with | Error msg -> error_json msg | Ok () -> diff --git a/ast-utils/test/dune b/ast-utils/test/dune index d63b54c..a8ae7ea 100644 --- a/ast-utils/test/dune +++ b/ast-utils/test/dune @@ -1,29 +1,60 @@ +; Every regression runs through with-built-plugin.sh, which points findlib at +; this tree's freshly built plug-in rather than the copy installed in the opam +; switch, and turns on the AST integrity check. (package ast_utils) is the +; dependency that makes dune populate the install lib it points at. + +(rule + (alias runtest) + (deps (source_tree regressions) (package ast_utils)) + (action + (run ./regressions/with-built-plugin.sh + %{workspace_root}/../install/default/lib ./regressions/run.sh))) + +(rule + (alias runtest) + (deps (source_tree regressions) (package ast_utils)) + (action + (run ./regressions/with-built-plugin.sh + %{workspace_root}/../install/default/lib ./regressions/run_exec_add_funspec.sh))) + (rule (alias runtest) - (deps (source_tree regressions)) - (action (run ./regressions/run.sh))) + (deps (source_tree regressions) (package ast_utils)) + (action + (run ./regressions/with-built-plugin.sh + %{workspace_root}/../install/default/lib ./regressions/run_funspec_scope.sh))) (rule (alias runtest) - (deps (source_tree regressions)) - (action (run ./regressions/run_exec_add_funspec.sh))) + (deps (source_tree regressions) (package ast_utils)) + (action + (run ./regressions/with-built-plugin.sh + %{workspace_root}/../install/default/lib ./regressions/run-payload-shapes.sh))) (rule (alias runtest) - (deps (source_tree regressions)) - (action (run ./regressions/run_funspec_scope.sh))) + (deps (source_tree regressions) (package ast_utils)) + (action + (run ./regressions/with-built-plugin.sh + %{workspace_root}/../install/default/lib ./regressions/run-contract-frontier.sh))) (rule (alias runtest) - (deps (source_tree regressions)) - (action (run ./regressions/run-payload-shapes.sh))) + (deps (source_tree regressions) (package ast_utils)) + (action + (run ./regressions/with-built-plugin.sh + %{workspace_root}/../install/default/lib ./regressions/run-cache-provenance.sh))) (rule (alias runtest) - (deps (source_tree regressions)) - (action (run ./regressions/run-contract-frontier.sh))) + (deps (source_tree regressions) (package ast_utils)) + (action + (run ./regressions/with-built-plugin.sh + %{workspace_root}/../install/default/lib ./regressions/run-ghost-integrity.sh))) (rule (alias runtest) - (deps (source_tree regressions)) - (action (run ./regressions/run-cache-provenance.sh))) + (deps (source_tree regressions) (package ast_utils)) + (action + (run ./regressions/with-built-plugin.sh + %{workspace_root}/../install/default/lib ./regressions/run-recursive-logic.sh))) diff --git a/ast-utils/test/regressions/ghost-integrity.c b/ast-utils/test/regressions/ghost-integrity.c new file mode 100644 index 0000000..9f21f86 --- /dev/null +++ b/ast-utils/test/regressions/ghost-integrity.c @@ -0,0 +1,43 @@ +/* + * Fixture for run-ghost-integrity.sh. Every statement an insertion targets sits + * on a line of its own, because the harness finds its sid by line. + */ + +int stale(int x) +{ + //@ ghost int g = 0; + x = x; + //@ assert g == 1; + return 0; +} + +int scoped(int x) +{ + int r = 0; + if (x > 0) { + int t = x; + r = t; + } else { + int t = -x; + r = t; + } + return r; +} + +int cond(int x) +{ + int r = 0; + if (x > 5) { + r = 1; + } + return r; +} + +int looped(int n) +{ + int s = 0; + for (int i = 0; i < n; i++) { + s += 1; + } + return s; +} diff --git a/ast-utils/test/regressions/recursive-logic.c b/ast-utils/test/regressions/recursive-logic.c new file mode 100644 index 0000000..5e564e5 --- /dev/null +++ b/ast-utils/test/regressions/recursive-logic.c @@ -0,0 +1,40 @@ +/* + * Fixture for run-recursive-logic.sh: one definition of each shape. The mutual + * case is in the script, because the kernel rejects it at parse time and every + * .c file here must parse for run.sh. + */ + +/* Direct recursion with no decreasing argument: an inconsistent axiom. */ +/*@ logic integer bad(integer n) = bad(n) + 1; */ + +/* Direct recursion inside an axiomatic block. It terminates, which this request + * does not try to decide: it is reported all the same. + */ +/*@ axiomatic Fact { + logic integer fact(integer n) = n <= 0 ? 1 : n * fact(n - 1); + } +*/ + +/* Not recursive, though it calls another definition. */ +/*@ logic integer twice(integer n) = n + n; + logic integer quad(integer n) = twice(twice(n)); +*/ + +/* Inductive: a least fixpoint, consistent by construction, even though its + * cases mention it. + */ +/*@ inductive reach(integer a, integer b) { + case refl: \forall integer a; reach(a, a); + case step: \forall integer a, b; reach(a + 1, b) ==> reach(a, b); + } +*/ + +/* Defined with a body that uses the inductive, so it is a node with an edge to + * a non-node, and not recursive. + */ +/*@ predicate reach_next(integer a) = reach(a, a + 1); */ + +int main(void) +{ + return 0; +} diff --git a/ast-utils/test/regressions/run-ghost-integrity.sh b/ast-utils/test/regressions/run-ghost-integrity.sh new file mode 100755 index 0000000..073e065 --- /dev/null +++ b/ast-utils/test/regressions/run-ghost-integrity.sh @@ -0,0 +1,198 @@ +#!/usr/bin/env bash +# Ghost statement insertion leaves an AST the kernel accepts and WP re-reads. +# +# Four contracts, each one broken before the fix that added this harness: +# - WP sees the inserted statement. Without Ast.mark_as_changed the per-function +# CFG cache WP keeps was not cleared, so a VC generated after the insertion +# was the VC of the old body: the assert below stayed "false". +# - A ghost local is declared in the block that holds it. Listing it in the +# function locals only made Filecheck report it as initialized twice. +# - A statement nested in a block is a valid target. The insertion used to +# report "not found" while having already spliced the statement in. +# - Names resolve through the blocks enclosing the insertion point, so a +# local of a sibling block is not in scope, and a source name CIL renamed +# (the second "t" below becomes t_0) means the declaration in scope. +# +# AST_UTILS_CHECK_AST is set by the dune rule, so every mutating request also +# runs Filecheck and fails with "AST integrity check failed" when it does not +# hold. The harness sets it again so a direct run checks the same thing. +set -euo pipefail + +FC="${FRAMA_C:-$(command -v frama-c || echo ~/.opam/frama/bin/frama-c)}" +if [[ ! -x "$FC" ]]; then + echo "frama-c not found; set FRAMA_C env var" >&2 + exit 2 +fi + +# Absolute, because the runs below change directory first and a relative FRAMA_C +# would then name nothing. +FC="$(cd "$(dirname "$FC")" && pwd)/$(basename "$FC")" +export AST_UTILS_CHECK_AST=1 + +HERE="$(cd "$(dirname "$0")" && pwd)" +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + +cp "$HERE/ghost-integrity.c" "$WORK/" + +# Phase 1: statement ids by source line, from a pristine load. +cat > "$WORK/context.json" << 'JSON' +[ + {"kind":"GET","id":"stale","request":"plugins.ast-utils.getCilContext","data":"stale"}, + {"kind":"GET","id":"scoped","request":"plugins.ast-utils.getCilContext","data":"scoped"}, + {"kind":"GET","id":"cond","request":"plugins.ast-utils.getCilContext","data":"cond"}, + {"kind":"GET","id":"looped","request":"plugins.ast-utils.getCilContext","data":"looped"} +] +JSON +(cd "$WORK" && "$FC" -load-module ast_utils_plugin -server-batch context.json \ + -server-batch-output-dir . ghost-integrity.c > /dev/null 2>&1) + +# Phase 2: the insertions, against a fresh load of the same file, so the sids +# found above name the same statements. +python3 - "$WORK/context.out.json" "$WORK/batch.json" "$HERE/ghost-integrity.c" << 'PY' +import json, sys + +ctx = {row["id"]: row["data"] for row in json.load(open(sys.argv[1]))} +source = open(sys.argv[3]).read().splitlines() + + +# A target's line is found by its text inside its function rather than written +# here, so a comment reflowed above it cannot move the target out from under +# the harness: the nth line holding text after the function's own header. +def at(fn, text, nth=1): + start = next(n for n, line in enumerate(source, 1) if f"int {fn}(" in line) + hits = [n for n, line in enumerate(source, 1) if n > start and text in line] + return hits[nth - 1] + + +def sid(fn, line, kind=None): + for st in ctx[fn]["statements"]: + if st["loc"]["line"] == line and (kind is None or st["kind"] == kind): + return st["sid"] + raise SystemExit(f"no statement of {fn} at line {line}") + + +def ghost(rid, fn, line, op, name, expr="", typ=None, kind=None): + data = {"function": fn, "stmt": sid(fn, line, kind), "op": op, + "name": name, "expr": expr} + if typ: + data["type"] = typ + return {"kind": "EXEC", "id": rid, + "request": "plugins.ast-utils.execInsertGhostStmt", "data": data} + + +batch = [ + {"kind": "GET", "id": "vc_before", "request": "plugins.ast-utils.getVcDetails", + "data": {"function": "stale"}}, + ghost("set_g", "stale", at("stale", "x = x;"), "set", "g", "1"), + {"kind": "GET", "id": "vc_after", "request": "plugins.ast-utils.getVcDetails", + "data": {"function": "stale"}}, + ghost("decl_nested", "scoped", at("scoped", "r = t;"), "decl", "gv", "t", "int"), + ghost("set_nested", "scoped", at("scoped", "r = t;"), "set", "gv", "t + 1"), + ghost("set_out_of_scope", "scoped", at("scoped", "r = t;", 2), "set", "gv", "1"), + ghost("decl_sibling", "scoped", at("scoped", "r = t;", 2), "decl", "gw", "t", "int"), + ghost("decl_outer_ref", "scoped", at("scoped", "return r;"), "decl", "gz", "t", "int"), + ghost("label", "scoped", at("scoped", "return r;"), "label", "Lend"), + ghost("decl_cond", "cond", at("cond", "if (x > 5)"), "decl", "gc", "0", "int", kind="if"), + ghost("else_set", "cond", at("cond", "if (x > 5)"), "else_set", "gc", "2", kind="if"), + {"kind": "EXEC", "id": "loop", "request": "plugins.ast-utils.execInsertGhostLoop", + "data": {"function": "looped", "stmt": sid("looped", at("looped", "return s;")), "name": "k", + "type": "int", "stop": "n", "invariant": "0 <= k", + "assigns": "k", "variant": "n - k"}}, + {"kind": "EXEC", "id": "sandbox", "request": "plugins.ast-utils.execCreateSandbox", + "data": "looped"}, + {"kind": "GET", "id": "src", "request": "plugins.ast-utils.printSource", + "data": ""}, +] +json.dump(batch, open(sys.argv[2], "w")) +PY + +(cd "$WORK" && "$FC" -load-module ast_utils_plugin -server-batch batch.json \ + -server-batch-output-dir . ghost-integrity.c > "$WORK/batch.log" 2>&1) + +python3 - "$WORK/batch.out.json" "$WORK/printed.c" << 'PY' +import json, re, sys + +rows = {row["id"]: row.get("data") for row in json.load(open(sys.argv[1]))} +fails = [] + + +def result(rid): + data = rows.get(rid) + if isinstance(data, dict) and "result" in data: + return data["result"] + return data + + +def expect_ok(rid): + res = result(rid) or {} + if res.get("success") is not True: + fails.append(f"{rid}: expected success, got {res}") + + +def expect_err(rid, substr): + res = result(rid) or {} + err = res.get("error") or "" + if res.get("success") is not False and "error" not in res: + fails.append(f"{rid}: expected a failure, got {res}") + elif substr not in err: + fails.append(f"{rid}: error {err!r} does not mention {substr!r}") + if "AST integrity" in err: + fails.append(f"{rid}: a refused insertion still corrupted the AST: {err}") + + +def assert_goals(rid): + res = result(rid) or {} + return [vc["goal"] for vc in res.get("vcs", []) + if "assert" in vc.get("description", "").lower() + or (vc.get("clause") or {}).get("kind") == "assert"] + + +before, after = assert_goals("vc_before"), assert_goals("vc_after") +if before != ["false"]: + fails.append(f"vc_before: expected the assert goal to be false, got {before}") +if after != ["true"]: + fails.append(f"vc_after: expected the assert goal to be true once g = 1 is in the body, got {after}") + +expect_ok("set_g") +expect_ok("decl_nested") +expect_ok("set_nested") +expect_err("set_out_of_scope", "not in scope") +expect_ok("decl_sibling") +expect_err("decl_outer_ref", "variable 't' is not in scope") +expect_ok("label") +expect_ok("decl_cond") +expect_ok("else_set") +expect_ok("loop") +sandbox = result("sandbox") or {} +if not sandbox.get("sandbox_name"): + fails.append(f"sandbox: expected a sandbox name, got {sandbox}") + +src = rows.get("src") +if not isinstance(src, str): + fails.append(f"src: expected printed source, got {src!r}") + src = "" +open(sys.argv[2], "w").write(src) +if not re.search(r"ghost int gw = t_0;", src): + fails.append("decl_sibling: 'gw' is not initialized from the 't' in scope (t_0)") +# The ghost local belongs to the then block: declared after the if opens and +# before its else. +scoped = src[src.find("int scoped("):] +then_part = scoped[scoped.find("if"):scoped.find("else")] +if "ghost int gv = t;" not in then_part: + fails.append("decl_nested: 'gv' was not declared inside the then block") + +if fails: + print("FAIL - ghost insertion integrity") + for f in fails: + print(f" {f}") + sys.exit(1) +print("PASS - ghost insertion integrity") +PY + +# The printed AST must still be C that Frama-C accepts. +if ! "$FC" "$WORK/printed.c" > "$WORK/printed.log" 2>&1; then + echo "FAIL - ghost insertion integrity: printed source does not parse" + tail -15 "$WORK/printed.log" | sed 's/^/ /' + exit 1 +fi diff --git a/ast-utils/test/regressions/run-recursive-logic.sh b/ast-utils/test/regressions/run-recursive-logic.sh new file mode 100755 index 0000000..24b880a --- /dev/null +++ b/ast-utils/test/regressions/run-recursive-logic.sh @@ -0,0 +1,111 @@ +#!/usr/bin/env bash +# getRecursiveLogic lists the logic definitions WP assumes without a termination +# check: those whose body reaches themselves. +# +# recursive-logic.c holds a direct recursion at top level, one inside an +# axiomatic block, a non-recursive pair where one calls the other, an inductive +# predicate whose cases mention it, and a definition that uses the inductive. +# Only the first two may be reported. +# +# The mutual case is written below rather than as a fixture. Measured on Frama-C +# 33.0, the kernel rejects it: a definition may name only symbols declared +# before it, and redefining a symbol declared without a body in an axiomatic +# block is "already declared". So no file can make two bodies refer to each +# other, and the check here is that this stays true; if a release starts +# accepting it, the request must then report both with a cycle of two. +set -euo pipefail + +FC="${FRAMA_C:-$(command -v frama-c || echo ~/.opam/frama/bin/frama-c)}" +if [[ ! -x "$FC" ]]; then + echo "frama-c not found; set FRAMA_C env var" >&2 + exit 2 +fi + +# Absolute, because the runs below change directory first and a relative FRAMA_C +# would then name nothing. +FC="$(cd "$(dirname "$FC")" && pwd)/$(basename "$FC")" + +HERE="$(cd "$(dirname "$0")" && pwd)" +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + +cp "$HERE/recursive-logic.c" "$WORK/" +cat > "$WORK/batch.json" << 'JSON' +[ {"kind":"GET","id":"rec","request":"plugins.ast-utils.getRecursiveLogic","data":null} ] +JSON +cat > "$WORK/mutual.c" << 'C' +/*@ predicate is_even(integer n) = n == 0 || (n > 0 && is_odd(n - 1)); + predicate is_odd(integer n) = n > 0 && is_even(n - 1); +*/ +int main(void) { return 0; } +C + +(cd "$WORK" && "$FC" -load-module ast_utils_plugin -server-batch batch.json \ + -server-batch-output-dir . recursive-logic.c > /dev/null 2>&1) + +mutual_parsed=1 +cp "$WORK/batch.json" "$WORK/mutual.json" +if ! (cd "$WORK" && "$FC" -load-module ast_utils_plugin \ + -server-batch mutual.json -server-batch-output-dir . mutual.c \ + > "$WORK/mutual.log" 2>&1); then + mutual_parsed=0 +fi + +python3 - "$WORK/batch.out.json" "$WORK/mutual.out.json" "$mutual_parsed" \ + "$WORK/mutual.log" "$HERE/recursive-logic.c" << 'PY' +import json, sys + +fails = [] + + +def definitions(path): + rows = {row["id"]: row.get("data") for row in json.load(open(path))} + data = rows.get("rec") or {} + return {d["name"]: d for d in data.get("definitions", [])} + + +found = definitions(sys.argv[1]) +# Each definition's line is looked up in the fixture rather than written +# here, so a comment reflowed above it does not fail the check. +source = open(sys.argv[5]).read().splitlines() + + +def line_of(text): + return next(n for n, line in enumerate(source, 1) if text in line) + + +want = { + "bad": ("function", line_of("logic integer bad(")), + "fact": ("function", line_of("logic integer fact(")), +} +for name, (kind, line) in want.items(): + d = found.get(name) + if d is None: + fails.append(f"{name}: recursive definition not reported") + continue + if d.get("kind") != kind: + fails.append(f"{name}: kind {d.get('kind')!r}, expected {kind!r}") + if d.get("line") != line or d.get("file") != "recursive-logic.c": + fails.append(f"{name}: at {d.get('file')}:{d.get('line')}, expected line {line}") + if d.get("cycle") != [name]: + fails.append(f"{name}: cycle {d.get('cycle')}, expected [{name!r}]") +for name in sorted(set(found) - set(want)): + fails.append(f"{name}: reported but not recursive (or inductive)") + +if sys.argv[3] == "1": + mutual = definitions(sys.argv[2]) + for name in ("is_even", "is_odd"): + d = mutual.get(name) + if d is None or d.get("kind") != "predicate" \ + or sorted(d.get("cycle", [])) != ["is_even", "is_odd"]: + fails.append(f"mutual: {name} reported as {d}") +elif "unbound logic predicate is_odd" not in open(sys.argv[4]).read(): + fails.append("mutual: the kernel rejected the fixture for another reason") + +if fails: + print("FAIL - getRecursiveLogic") + for f in fails: + print(f" {f}") + sys.exit(1) +print("PASS - getRecursiveLogic") +PY diff --git a/ast-utils/test/regressions/with-built-plugin.sh b/ast-utils/test/regressions/with-built-plugin.sh new file mode 100755 index 0000000..adc0781 --- /dev/null +++ b/ast-utils/test/regressions/with-built-plugin.sh @@ -0,0 +1,33 @@ +#!/usr/bin/env bash +# Run a regression script against the plug-in this tree just built. +# +# Usage: with-built-plugin.sh