Interval Analysis. More...

#include "interval_analysis.h"
#include <goto-programs/abstract-interpretation/interval_domain.h>
#include <unordered_set>
#include <util/base/prefix.h>
#include <goto-programs/goto_loops.h>
#include <util/base/time_stopping.h>
#include <fstream>

Include dependency graph for interval_analysis.cpp:

Functions
template<class Interval>
void	optimize_expr_interval (expr2tc &expr, const interval_domaint &state)
static void	optimize_expression (expr2tc &expr, const interval_domaint &state)
void	optimize_function (const ait< interval_domaint > &interval_analysis, goto_functiont &goto_function)
void	instrument_symbol_constraints (const ait< interval_domaint > &interval_analysis, std::unordered_set< expr2tc, irep2_hash > symbols, goto_programt::instructionst::iterator &it, goto_functiont &goto_function)
void	instrument_loops (const ait< interval_domaint > &interval_analysis, goto_functionst &program)
	Instrument loops with all variables that are affected by it (not only the guards).
static goto_programt::targett	skip_inductive_preamble (goto_programt::targett loop_head, goto_programt::targett loop_exit)
	Find the first instruction at or after `loop_head` that was NOT inserted by k-induction's preamble (havoc + entry-condition assume).
void	instrument_loop_bounds_after_kind (goto_functionst &goto_functions, const namespacet &ns, const optionst &options, bool continue_past_failed_assertions)
	Post-k-induction loop-bounds instrumentation.
void	instrument_intervals (const ait< interval_domaint > &interval_analysis, goto_functiont &goto_function, const INTERVAL_INSTRUMENTATION_MODE instrument_mode)
void	dump_intervals (std::ostringstream &out, const goto_functiont &goto_function, const ait< interval_domaint > &interval_analysis)
void	interval_analysis (goto_functionst &goto_functions, const namespacet &ns, const optionst &options, bool continue_past_failed_assertions, const INTERVAL_INSTRUMENTATION_MODE instrument_mode)

Detailed Description

Interval Analysis.

Function Documentation

◆ dump_intervals()

void dump_intervals	(	std::ostringstream &	out,
		const goto_functiont &	goto_function,
		const ait< interval_domaint > &	interval_analysis )

◆ instrument_intervals()

void instrument_intervals	(	const ait< interval_domaint > &	interval_analysis,
		goto_functiont &	goto_function,
		const INTERVAL_INSTRUMENTATION_MODE	instrument_mode )

◆ instrument_loop_bounds_after_kind()

void instrument_loop_bounds_after_kind	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		const optionst &	options,
		bool	continue_past_failed_assertions )

Post-k-induction loop-bounds instrumentation.

Re-runs interval analysis with inductive_step_instruction instructions (k-induction's nondet havocs and entry-condition assumes) treated as transparent no-ops, so the fixpoint at each loop head reflects the original program's dataflow. For every loop, inserts a single ASSUME(bounds) immediately before the loop's exit-test (the IF that k-induction's preamble runs into) — i.e. between the havoc'd assignments and the IF, so the bounds tighten the havoc'd values for the inductive step. The inserted ASSUME is marked inductive_step_instruction = true so base case and forward condition skip it.

Must run AFTER goto_k_induction(). Always runs the full ait fixpoint and per-loop scan; inserts no ASSUME for loops where every variable's bound simplifies to true (i.e. no useful tightening).

◆ instrument_loops()

void instrument_loops	(	const ait< interval_domaint > &	interval_analysis,
		goto_functionst &	program )

Instrument loops with all variables that are affected by it (not only the guards).

Before: before-loop 1 : IF !(COND == 0) GOTO 2 X = Y // X changes and Y is read-only ... GOTO 1 2: after-loop

After: before-loop ASSUME (COND >= some_value && ... && Y <= some_value2) 1: IF !(COND == 0) GOTO 2 X = Y // X changes and Y is read-only ... ASSUME (COND >= some_value && ... && Y <= some_value2) GOTO 1 2: ASSUME (COND >= some_value && ... && Y <= some_value2) after-loop

◆ instrument_symbol_constraints()

void instrument_symbol_constraints	(	const ait< interval_domaint > &	interval_analysis,
		std::unordered_set< expr2tc, irep2_hash >	symbols,
		goto_programt::instructionst::iterator &	it,
		goto_functiont &	goto_function )

inline

◆ interval_analysis()

void interval_analysis	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		const optionst &	options,
		bool	continue_past_failed_assertions,
		const INTERVAL_INSTRUMENTATION_MODE	instrument_mode )

◆ optimize_expr_interval()

template<class Interval>

void optimize_expr_interval	(	expr2tc &	expr,
		const interval_domaint &	state )

inline

◆ optimize_expression()

void optimize_expression	(	expr2tc &	expr,
		const interval_domaint &	state )

static

◆ optimize_function()

void optimize_function	(	const ait< interval_domaint > &	interval_analysis,
		goto_functiont &	goto_function )

◆ skip_inductive_preamble()

goto_programt::targett skip_inductive_preamble	(	goto_programt::targett	loop_head,
		goto_programt::targett	loop_exit )