#include <transition-system/ts_extraction.h>
#include <goto-symex/equation/symex_target_equation.h>
#include <goto-symex/scheduler/reachability_tree.h>
#include <irep2/irep2_utils.h>
#include <langapi/language_util.h>
#include <util/irep/migrate.h>
#include <util/message/message.h>
#include <util/symtab/symbol.h>
#include <algorithm>
#include <set>

Include dependency graph for ts_extraction.cpp:

Functions
bool	extract_transition_system (const goto_functionst &goto_functions, contextt &context, const optionst &options, transition_systemt &ts)
	Extraction marks the three points that delimit a step, runs symex once, then reads the markers back out of the SSA.

Function Documentation

◆ extract_transition_system()

bool extract_transition_system	(	const goto_functionst &	goto_functions,
		contextt &	context,
		const optionst &	options,
		transition_systemt &	ts )

Extraction marks the three points that delimit a step, runs symex once, then reads the markers back out of the SSA.

Recognise a single unbounded loop in main (after the k-induction transformation) and extract it into ts, running symbolic execution over one iteration.

x = 0                 prefix
ts$init$0 = x         <- before the havoc: value entering the loop
x = nondet()             the k-induction havoc

head: ts$pre$0 = x <- before the head: state at the loop head assert(x < 4) body x = (x + 1) & 3 ts$post$0 = x <- before the back edge: state at the back edge goto head

One symbolic execution of that yields an SSA in which the marker assignments cut everything into regions:

x@1 == 0              i < init_first        -> prefix_defs
ts$init$0 == x@1      init_first            -> states[0].init
x@2 == nondet         havoc region             dropped (is_only)
ts$pre$0 == x@2       pre_first..pre_last   -> states[0].pre
guard => x@2 < 4      i > pre_last          -> bad
x@3 == (x@2 + 1) & 3                        -> body_defs
ts$post$0 == x@3      post_first            -> states[0].post

So each marker's rhs is the value wanted, and the steps between markers are the prefix and the body: assignments become *_defs, assumes become *_assumes (or invariants when inductive-step-only), asserts become *_bad. back_guard is the guard the first ts$post$ step carries.

Functions

Function Documentation

◆ extract_transition_system()