cprover
Loading...
Searching...
No Matches
enumerative_loop_contracts_synthesizer.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Enumerative Loop Contracts Synthesizer
4
5Author: Qinheping Hu
6
7\*******************************************************************/
8
11
12// NOLINTNEXTLINE(whitespace/line_length)
13#ifndef CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H
14// NOLINTNEXTLINE(whitespace/line_length)
15#define CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H
16
17#include <util/options.h>
18
20
21class messaget;
22class goto_modelt;
23
31{
32public:
43
47 exprt synthesize(loop_idt loop_id) override;
48
49 std::map<loop_idt, std::set<exprt>> get_assigns_map() const
50 {
51 return assigns_map;
52 }
53
56
57private:
59 void init_candidates();
60
63 void build_tmp_post_map();
64
67 std::set<symbol_exprt> compute_dependent_symbols(
68 const loop_idt &cause_loop_id,
69 const exprt &new_clause,
70 const std::set<exprt> &live_vars);
71
73 exprt synthesize_range_predicate(const exprt &violated_predicate);
74
77 exprt synthesize_same_object_predicate(const exprt &checked_pointer);
78
81 const std::vector<exprt> terminal_symbols,
82 const loop_idt &cause_loop_id,
83 const irep_idt &violation_id);
84
87 const exprt &checked_pointer,
88 const std::list<loop_idt> cause_loop_ids);
89
95
97 std::map<loop_idt, std::set<exprt>> assigns_map;
98
100 std::unordered_map<exprt, exprt, irep_hash> tmp_post_map;
101
104};
105
106// NOLINTNEXTLINE(whitespace/line_length)
107#endif // CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
exprt synthesize_strengthening_clause(const std::vector< exprt > terminal_symbols, const loop_idt &cause_loop_id, const irep_idt &violation_id)
Synthesize strengthening clause for invariant-not-preserved violation.
std::map< loop_idt, std::set< exprt > > get_assigns_map() const
std::map< loop_idt, std::set< exprt > > assigns_map
Synthesized assigns clauses.
invariant_mapt synthesize_all() override
This synthesizer guarantees that, with the synthesized loop contracts, all checks in the annotated GO...
exprt synthesize(loop_idt loop_id) override
Synthesize loop invariant for a specified loop in the goto_model.
exprt synthesize_range_predicate(const exprt &violated_predicate)
Synthesize range predicate for OOB violation with violated_predicate.
const symbol_tablet original_symbol_table
Symbol table of the input goto model.
enumerative_loop_contracts_synthesizert(goto_modelt &goto_model, const optionst &options, messaget &log)
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 ne...
invariant_mapt in_invariant_clause_map
Synthesize invariant of form (in_inv || !guard) && (!guard -> pos_inv)
void build_tmp_post_map()
Scan all ASSIGN instructions to build the map from tmp_post variables to their original variables.
std::unordered_map< exprt, exprt, irep_hash > tmp_post_map
Map from tmp_post variables to their original variables.
void init_candidates()
Initialize invariants as true for all unannotated loops.
void synthesize_assigns(const exprt &checked_pointer, const std::list< loop_idt > cause_loop_ids)
Synthesize assigns target and update assigns_map.
exprt synthesize_same_object_predicate(const exprt &checked_pointer)
Synthesize same object predicate for null-pointer violation for checked_pointer.
Base class for all expressions.
Definition expr.h:56
A base class for loop contracts synthesizers.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table.
Loop Contracts Synthesizer Interface.
Options.
Loop id used to identify loops.
Definition loop_ids.h:28
std::map< loop_idt, exprt > invariant_mapt
Definition utils.h:30