diff --git a/README.md b/README.md
index f4b68cf..b146090 100644
--- a/README.md
+++ b/README.md
@@ -270,7 +270,7 @@ The server exposes the following tool groups:
| Domain | Tools | Purpose |
|--------|-------|---------|
| Project | `reload_project`, `list`, `context`, `self_check`, `parse_surface` | Load source, inspect declarations, navigate call relationships, report server capabilities, and measure how much of a file set Frama-C can parse at all |
-| Concurrency | `analyze_concurrency` | Screen source text for concurrent events, lock order, and race candidates. Level-0 syntax: candidates are never verdicts, and an absent candidate is not one either |
+| Concurrency | `analyze_concurrency` | Screen source text for concurrent events, lock order, and race and deadlock candidates. Level-0 syntax: candidates are never verdicts, and an absent candidate is not one either |
| EVA/WP | `check`, `run_wp`, `get_wp_goals`, `proof_coverage`, `run_e_acsl` | Run verification, read its conclusions, report stored proof coverage, and execute runtime counterexamples |
| Annotations | `inject_all_annotations`, `propose_annotations` | Dry-run validate and inject ACSL annotations, and propose the frame conditions the code determines |
| Sandbox | `create_sandbox`, `delete_sandbox` | Isolate annotation experiments |
@@ -407,6 +407,24 @@ Set it to `false`, on the profile or on `reload_project` and `check`, only for
code whose idioms wrap by design; a run under it reports `RTE_REDUCED`, and a
receipt made under it names the setting in its load identity.
+`rte_pointer` is optional, and false when unset: set it to `true`, on the
+profile or on `reload_project` and `check`, and a load that also has `rte`
+checks that every pointer formed points into an object or one past it
+(`-warn-invalid-pointer`). Under `rte: false` there are no runtime-error
+obligations for it to add to, so it does nothing.
+Without it, `base + off` computed before a NULL test proves. It is off by
+default because idioms such as `container_of` form such pointers on purpose. A
+receipt made under it names the setting in its load identity.
+
+`builtin_models` is optional, and false when unset: set it to `true`, on the
+profile or on `reload_project` and `check`, to force-include this server's
+contracts for `__builtin_unreachable`, `__builtin_trap`, `__builtin_clz`,
+`__builtin_ctz` and `__builtin_popcount`. Frama-C declares the first as an
+ordinary returning function and the second not at all, so without them a
+proof cannot use the fact that the code after `if (x < 0)
+__builtin_unreachable();` has `x >= 0`. Every contract in the header is an
+assumption, and the receipt's load identity carries the header's sha256.
+
Two further fields are optional, and say what this server cannot otherwise
know. `min_goals` is the floor on obligations the target requires WP to
*generate*, and a run that generates fewer is refused: "N of N discharged" is
@@ -676,6 +694,13 @@ payload contract and the change rule. The full set:
| `WP_WEAKENED_MODEL` | The run's memory model used a selector that departs from C semantics: `+cast` (unsafe pointer casts), `+nat` (unbounded integers) or `+real` (exact reals) |
| `SMOKE_TEST_FAILED` | Smoke tests were requested and WP proved a smoke goal, so something in scope is unreachable or contradictory and the goals around it prove for the wrong reason |
| `SMOKE_TEST_UNCHECKED` | Smoke tests were requested and did not run, so whether the specification is vacuous is unknown |
+| `REACHABILITY_PROPERTY_UNENCODED` | The program states its property SV-COMP style, as a `reach_error` or `__VERIFIER_assert` call, and the harness preconditions do not make it a proof obligation: every error function needs `requires \false`, and `__VERIFIER_assert` its parameter `!= 0` when no error function is defined |
+| `CONCURRENT_PROGRAM` | The program creates threads, and EVA and WP analyze it sequentially: thread bodies are not analyzed from `main` and no interleaving is considered, so run `analyze_concurrency` |
+| `COMPILE_FLAGS_DROPPED` | The compilation database builds with flags Frama-C drops on import, such as `-funsigned-char`, `-fwrapv` or `-m32`, so the analyzed program differs from the compiled one |
+| `PINNED_PROPERTY_MISSING` | A property passed in `pinned` is no longer in the program in the form it was pinned, so what was proved is not what was asked for |
+| `PINNED_PROPERTY_NOT_PROVED` | A property passed in `pinned` is present and not proved |
+| `CONTRACT_DECORATIVE` | With `mutants: true`, a stub body (`return 0`, `return `) proves every postcondition of the function's contract, so the proof does not tell the function from the stub |
+| `CONTRACT_MUTANTS_UNCHECKED` | `mutants: true` was asked for and no stub could be judged: no `function`, an extraction failure, or no postcondition to test |
| `AST_PARSE_DIAGNOSTICS_UNAVAILABLE` | This server has no record of what the front end dropped, so nothing says the analyzed program is the compiled one |
Treat the set as additive: codes are added as gaps are found, and three were
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