- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <goto-programs/goto_loop_invariant.h>#include <goto-programs/frame_enforcer.h>#include <goto-programs/remove_no_op.h>#include <util/lang/c_types.h>#include <util/expr/expr_util.h>#include <util/base/i2string.h>#include <util/irep/std_expr.h>#include <util/config/options.h>#include <irep2/irep2_utils.h>#include <functional>#include <map>Namespaces | |
| namespace | loop_invariant |
Functions | |
| bool | loop_invariant::is_inert_scan_instruction (goto_programt::const_targett t) |
| Instructions with no effect a caller needs to account for: no write to a tracked variable, no control-flow or heap/external effect. | |
| static bool | is_generated_name (const irep_idt &name) |
| True for a name the frontend generated rather than the user: ESBMC spells those with a '$' (e.g. | |
| static bool | is_compiler_temp (goto_programt::const_targett t) |
| Returns true if the instruction is a compiler-generated DECL, ASSIGN, or FUNCTION_CALL. | |
| static std::vector< expr2tc > | extract_invariants_near (goto_programt::targett loop_head, goto_programt::targett begin) |
Walk backwards from loop_head (up to kMaxInvariantSearchBack steps) and return the invariant expression(s) for the nearest LOOP_INVARIANT found. | |
| void | goto_loop_invariant (goto_functionst &goto_functions, contextt &context, bool use_frame_rule) |
| Entry point: process loop invariants for all functions. | |
| static bool | is_trivial_rhs (const expr2tc &expr) |
Return true if expr is a trivial RHS (constant 0/1, constant bool, or NONDET). | |
| static bool | is_likely_compiler_temp (const irep_idt &id) |
| Heuristic: compiler-generated temporaries (e.g. | |
| static bool | symbol_name_matches (const irep_idt &full_or_short, const irep_idt &decl_id, bool allow_suffix) |
True if full_or_short matches decl_id: either exact match, or (when allow_suffix) full_or_short ends with "::" + decl_id. | |
| static void | collect_symbols_local (const expr2tc &expr, std::set< irep_idt > &symbols) |
| Local helper: collect all symbol names reachable from an expression tree. | |
| static void | extract_and_remove_side_effects_impl (goto_functiont &goto_function, goto_programt::targett loop_head, const loopst &loop, const std::vector< expr2tc > &invariants, goto_programt &side_effects_out) |
| Shared implementation used by both the legacy loop-invariant pass and the combined loop-invariant + k-induction pass. | |
| void | goto_loop_invariant_combined (goto_functionst &goto_functions) |
| Combined loop-invariant + k-induction mode. | |
| static expr2tc | loop_entry_cond (goto_programt::targett loop_head) |
| The condition under which a while or for loop is entered: the negation of its head IF's guard, which ASSUME(entry_cond) stands in for so the head need not be copied. | |
| static goto_programt::targett | loop_body_begin (goto_programt::targett loop_head, const expr2tc &entry_cond) |
| Where the copied body starts: after the head when ASSUME(entry_cond) stands in for it, at the head otherwise, because a do-while head is a body instruction and skipping it left the verification branch empty (#7494). | |
| static void | assume_continue_cond (goto_programt::targett loop_exit, goto_programt &out) |
| Constrain the copied iteration to one another would follow. | |
Variables | |
| const char *const | kSynthesisedInvariantProperty = "synthesised-loop-invariant" |
| Property tag that goto_synthesise_loop_invariants stamps on the LOOP_INVARIANT markers it emits. | |
|
static |
Constrain the copied iteration to one another would follow.
A do-while's exit test lives on its back edge, so the copy may be the last iteration, and a head invariant need not hold where the loop exits: x <= 4 on do x++; while (x < 5) holds at every head and is false once the exiting iteration leaves x == 5. No-op for the unconditional back edge of a while or for loop (issue #7494).
Local helper: collect all symbol names reachable from an expression tree.
|
static |
Shared implementation used by both the legacy loop-invariant pass and the combined loop-invariant + k-induction pass.
See the declaration of goto_loop_invariantt::extract_and_remove_side_effects for a high-level description; this helper just takes an explicit goto_function parameter so it can be reused from both passes.
|
static |
Walk backwards from loop_head (up to kMaxInvariantSearchBack steps) and return the invariant expression(s) for the nearest LOOP_INVARIANT found.
Multiple conjuncts are folded into a single and2tc. Returns an empty vector when no annotated LOOP_INVARIANT is in range.
| void goto_loop_invariant | ( | goto_functionst & | goto_functions, |
| contextt & | context, | ||
| bool | use_frame_rule ) |
Entry point: process loop invariants for all functions.
When use_frame_rule is true, enables the observational frame rule (Snapshot → Havoc → Assume) for enhanced inductive verification.
| void goto_loop_invariant_combined | ( | goto_functionst & | goto_functions | ) |
Combined loop-invariant + k-induction mode.
Inserts a non-deterministic "Branch 1" verification block immediately before each annotated loop. Branch 1 checks that the user-supplied invariant is actually inductive (base case + inductive step), using specially tagged ASSERT instructions so the verifier can distinguish invariant failures from ordinary program assertion failures.
The original loop is left untouched for subsequent transformation by goto_k_induction (Branch 2), which adds ASSUME(invariant) after its nondet-assign step to tighten the inductive-step search space.
|
static |
Returns true if the instruction is a compiler-generated DECL, ASSIGN, or FUNCTION_CALL.
These may legitimately appear between consecutive __ESBMC_loop_invariant() calls. FUNCTION_CALL instructions arise when remove_function_call emits a DECL + FUNCTION_CALL pair for helper functions called inside an invariant.
True for a name the frontend generated rather than the user: ESBMC spells those with a '$' (e.g.
return_value$___ESBMC_forall$N).
Heuristic: compiler-generated temporaries (e.g.
for short-circuit evaluation) typically have '$' in their name; user variables do not. Used to avoid moving user variable DECLs/ASSIGNs while still collecting compiler temps.
Return true if expr is a trivial RHS (constant 0/1, constant bool, or NONDET).
We skip collecting such assignments when tracing back from the invariant so that we only pull in the "real" definition (e.g. from a function call) and not the fallback or initialiser.
|
static |
Where the copied body starts: after the head when ASSUME(entry_cond) stands in for it, at the head otherwise, because a do-while head is a body instruction and skipping it left the verification branch empty (#7494).
|
static |
The condition under which a while or for loop is entered: the negation of its head IF's guard, which ASSUME(entry_cond) stands in for so the head need not be copied.
Nil for a do-while, whose head is not a conditional goto but the first instruction of the body – it always enters (issue #7494).
|
static |
True if full_or_short matches decl_id: either exact match, or (when allow_suffix) full_or_short ends with "::" + decl_id.
| const char* const kSynthesisedInvariantProperty = "synthesised-loop-invariant" |
Property tag that goto_synthesise_loop_invariants stamps on the LOOP_INVARIANT markers it emits.
The extractor here accepts a tagged marker only when it sits immediately before the loop head it is being extracted for; a user-written __ESBMC_loop_invariant carries no tag and keeps the looser proximity rule. Without the tag the two passes share nothing but a 10-instruction window, and a synthesised invariant silently attaches itself to whichever loop happens to be nearby.
1.15.0