Harden check against verdicts the run did not establish

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 <param>`) 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

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)]