Enumerative loop contracts synthesizers. More...

#include <enumerative_loop_contracts_synthesizer.h>

Inheritance diagram for enumerative_loop_contracts_synthesizert:

Collaboration diagram for enumerative_loop_contracts_synthesizert:

Public Member Functions
	enumerative_loop_contracts_synthesizert (goto_modelt &goto_model, const optionst &options, messaget &log)

invariant_mapt	synthesize_all () override
	This synthesizer guarantees that, with the synthesized loop contracts, all checks in the annotated GOTO program pass. More...

exprt	synthesize (loop_idt loop_id) override
	Synthesize loop invariant for a specified loop in the `goto_model`. More...

std::map< loop_idt, std::set< exprt > >	get_assigns_map () const

Public Member Functions inherited from loop_contracts_synthesizer_baset
	loop_contracts_synthesizer_baset (goto_modelt &goto_model, messaget &log)

virtual	~loop_contracts_synthesizer_baset ()=default

Public Attributes
const optionst &	options

namespacet	ns

Private Member Functions
void	init_candidates ()
	Initialize invariants as true for all unannotated loops. More...

void	build_tmp_post_map ()
	Scan all ASSIGN instructions to build the map from tmp_post variables to their original variables. More...

std::set< symbol_exprt >	compute_dependent_symbols (const loop_idt &cause_loop_id, const exprt &new_clause, const std::set< exprt > &live_vars)
	Compute the dependent symbols for a loop with invariant-not-preserved violation which happen after `new_clause` was added. More...

exprt	synthesize_range_predicate (const exprt &violated_predicate)
	Synthesize range predicate for OOB violation with `violated_predicate`. More...

exprt	synthesize_same_object_predicate (const exprt &checked_pointer)
	Synthesize same object predicate for null-pointer violation for `checked_pointer`. More...

exprt	synthesize_strengthening_clause (const std::vector< exprt > terminal_symbols, const loop_idt &cause_loop_id, const irep_idt &violation_id, const std::vector< cext > &cexs)
	Synthesize strengthening clause for invariant-not-preserved violation. More...

void	synthesize_assigns (const exprt &checked_pointer, const std::list< loop_idt > cause_loop_ids)
	Synthesize assigns target and update assigns_map. More...

Private Attributes
invariant_mapt	in_invariant_clause_map
	Synthesize invariant of form (in_inv \|\| !guard) && (!guard -> pos_inv) More...

invariant_mapt	pos_invariant_clause_map

invariant_mapt	neg_guards

std::map< loop_idt, std::set< exprt > >	assigns_map
	Synthesized assigns clauses. More...

std::unordered_map< exprt, exprt, irep_hash >	tmp_post_map
	Map from tmp_post variables to their original variables. More...

const symbol_tablet	original_symbol_table
	Symbol table of the input goto model. More...

Additional Inherited Members
Protected Attributes inherited from loop_contracts_synthesizer_baset
goto_modelt &	goto_model

messaget &	log

Detailed Description

Enumerative loop contracts synthesizers.

It is designed for goto_model containing only checks instrumented by goto-instrument with the --pointer-check flag. When other checks present, it will just enumerate candidates and check if they are valid.

Definition at line 30 of file enumerative_loop_contracts_synthesizer.h.

Constructor & Destructor Documentation

◆ enumerative_loop_contracts_synthesizert()

enumerative_loop_contracts_synthesizert::enumerative_loop_contracts_synthesizert	(	goto_modelt &	goto_model,
		const optionst &	options,
		messaget &	log
	)

inline

Definition at line 34 of file enumerative_loop_contracts_synthesizer.h.

Member Function Documentation

◆ build_tmp_post_map()

void enumerative_loop_contracts_synthesizert::build_tmp_post_map ( )

private

Scan all ASSIGN instructions to build the map from tmp_post variables to their original variables.

Definition at line 234 of file enumerative_loop_contracts_synthesizer.cpp.

◆ compute_dependent_symbols()

std::set< symbol_exprt > enumerative_loop_contracts_synthesizert::compute_dependent_symbols	(	const loop_idt &	cause_loop_id,
		const exprt &	new_clause,
		const std::set< exprt > &	live_vars
	)

private

Compute the dependent symbols for a loop with invariant-not-preserved violation which happen after new_clause was added.

Definition at line 259 of file enumerative_loop_contracts_synthesizer.cpp.

◆ get_assigns_map()

std::map<loop_idt, std::set<exprt> > enumerative_loop_contracts_synthesizert::get_assigns_map ( ) const

inline

Definition at line 50 of file enumerative_loop_contracts_synthesizer.h.

◆ init_candidates()

void enumerative_loop_contracts_synthesizert::init_candidates ( )

private

Initialize invariants as true for all unannotated loops.

Definition at line 92 of file enumerative_loop_contracts_synthesizer.cpp.

◆ synthesize()

exprt enumerative_loop_contracts_synthesizert::synthesize ( loop_idt )

overridevirtual

Synthesize loop invariant for a specified loop in the goto_model.

Implements loop_contracts_synthesizer_baset.

Definition at line 564 of file enumerative_loop_contracts_synthesizer.cpp.

◆ synthesize_all()

invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all ( )

overridevirtual

This synthesizer guarantees that, with the synthesized loop contracts, all checks in the annotated GOTO program pass.

Implements loop_contracts_synthesizer_baset.

Definition at line 431 of file enumerative_loop_contracts_synthesizer.cpp.

◆ synthesize_assigns()

void enumerative_loop_contracts_synthesizert::synthesize_assigns	(	const exprt &	checked_pointer,
		const std::list< loop_idt >	cause_loop_ids
	)

private

Synthesize assigns target and update assigns_map.

Definition at line 192 of file enumerative_loop_contracts_synthesizer.cpp.

◆ synthesize_range_predicate()

exprt enumerative_loop_contracts_synthesizert::synthesize_range_predicate ( const exprt & violated_predicate )

private

Synthesize range predicate for OOB violation with violated_predicate.

Definition at line 286 of file enumerative_loop_contracts_synthesizer.cpp.

◆ synthesize_same_object_predicate()

exprt enumerative_loop_contracts_synthesizert::synthesize_same_object_predicate ( const exprt & checked_pointer )

private

Synthesize same object predicate for null-pointer violation for checked_pointer.

Definition at line 296 of file enumerative_loop_contracts_synthesizer.cpp.

◆ synthesize_strengthening_clause()

exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause	(	const std::vector< exprt >	terminal_symbols,
		const loop_idt &	cause_loop_id,
		const irep_idt &	violation_id,
		const std::vector< cext > &	cexs
	)

private

Synthesize strengthening clause for invariant-not-preserved violation.

Definition at line 307 of file enumerative_loop_contracts_synthesizer.cpp.

Member Data Documentation

◆ assigns_map

std::map<loop_idt, std::set<exprt> > enumerative_loop_contracts_synthesizert::assigns_map

private

Synthesized assigns clauses.

Definition at line 99 of file enumerative_loop_contracts_synthesizer.h.

◆ in_invariant_clause_map

invariant_mapt enumerative_loop_contracts_synthesizert::in_invariant_clause_map

private

Synthesize invariant of form (in_inv || !guard) && (!guard -> pos_inv)

Definition at line 94 of file enumerative_loop_contracts_synthesizer.h.

◆ neg_guards

invariant_mapt enumerative_loop_contracts_synthesizert::neg_guards

private

Definition at line 96 of file enumerative_loop_contracts_synthesizer.h.

◆ ns

namespacet enumerative_loop_contracts_synthesizert::ns

Definition at line 56 of file enumerative_loop_contracts_synthesizer.h.

◆ options

const optionst& enumerative_loop_contracts_synthesizert::options

Definition at line 55 of file enumerative_loop_contracts_synthesizer.h.

◆ original_symbol_table

const symbol_tablet enumerative_loop_contracts_synthesizert::original_symbol_table

private

Symbol table of the input goto model.

Definition at line 105 of file enumerative_loop_contracts_synthesizer.h.

◆ pos_invariant_clause_map

invariant_mapt enumerative_loop_contracts_synthesizert::pos_invariant_clause_map

private

Definition at line 95 of file enumerative_loop_contracts_synthesizer.h.

◆ tmp_post_map

std::unordered_map<exprt, exprt, irep_hash> enumerative_loop_contracts_synthesizert::tmp_post_map

private

Map from tmp_post variables to their original variables.

Definition at line 102 of file enumerative_loop_contracts_synthesizer.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h
/home/runner/work/cbmc/cbmc/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ enumerative_loop_contracts_synthesizert()

Member Function Documentation

◆ build_tmp_post_map()

◆ compute_dependent_symbols()

◆ get_assigns_map()

◆ init_candidates()

◆ synthesize()

◆ synthesize_all()

◆ synthesize_assigns()

◆ synthesize_range_predicate()

◆ synthesize_same_object_predicate()

◆ synthesize_strengthening_clause()

Member Data Documentation

◆ assigns_map

◆ in_invariant_clause_map

◆ neg_guards

◆ ns

◆ options

◆ original_symbol_table

◆ pos_invariant_clause_map

◆ tmp_post_map