31 const std::string &file_name,
33 : ns(goto_model.symbol_table),
34 goto_model(goto_model),
35 symbol_table(goto_model.symbol_table),
36 goto_functions(goto_model.goto_functions),
37 message_handler(message_handler)
49 for(
const auto &function_entry : this->
functions)
51 bool function_found =
false;
56 if(std::regex_match(function.first.c_str(), function_entry.first))
60 "function regex " + function_entry.second.regex_str +
61 " matches more than one function");
63 function_found =
true;
66 for(
const auto &loop_entry : function_entry.second.loop_contracts)
68 mangle(loop_entry, function.first);
75 "function regex " + function_entry.second.regex_str +
76 " matches no function");
81 std::string function_name,
82 const std::size_t num_of_args)
89 for(
unsigned i = 0; i < num_of_args; i++)
124 std::ostringstream pr;
125 pr <<
"void _fn() { while(1==1)";
126 if(!loop_contracts.
assigns.empty())
136 pr <<
" {}}" << std::endl;
138 log.
debug() <<
"Constructing fake function:\n" << pr.str() << log.
eom;
141 std::istringstream is(pr.str());
154 .add(ID_C_spec_loop_invariant))
157 log.
debug() <<
"Extracted loop invariants: " << inv_expr.
pretty() <<
"\n"
162 if(!loop_contracts.
assigns.empty())
168 .add(ID_C_spec_assigns))
180 .add(ID_C_spec_decreases))
183 decreases_exprs.emplace_back(op);
188 log.
debug() <<
"Start to replace symbols" << log.
eom;
190 if(assigns_expr.has_value())
194 for(
exprt &decrease_expr : decreases_exprs)
215 log.
debug() <<
"Start to typecheck invariants." << log.
eom;
219 "old is not allowed in loop invariants.");
228 log.
debug() <<
"Start to typecheck assigns." << log.
eom;
229 if(assigns_expr.has_value())
235 assigns_expr.value();
240 log.
debug() <<
"Start to typecheck decreases." << log.
eom;
241 if(!decreases_exprs.empty())
243 std::map<loop_idt, std::vector<exprt>> decreases_map;
245 std::vector<exprt>();
246 for(
exprt &decrease_expr : decreases_exprs)
250 .emplace_back(decrease_expr);
255 log.
debug() <<
"Mangling finished." << log.
eom;
276 if(!function.is_object())
281 const auto function_name = function_entry.first;
282 const auto &items = function_entry.second;
284 if(!items.is_array())
289 function_config.
regex_str = function_name;
293 if(!function_item.is_object())
296 std::string loop_id =
"";
297 std::string invariants_str =
"";
298 std::string assigns_str =
"";
299 std::string decreases_str =
"";
304 if(!loop_item.second.is_string())
307 if(loop_item.first ==
"loop_id")
309 loop_id = loop_item.second.value;
313 if(loop_item.first ==
"assigns")
315 assigns_str = loop_item.second.value;
319 if(loop_item.first ==
"decreases")
321 decreases_str = loop_item.second.value;
325 if(loop_item.first ==
"invariants")
327 invariants_str = loop_item.second.value;
331 if(loop_item.first ==
"symbol_map")
333 std::string symbol_map_str = loop_item.second.value;
336 symbol_map_str.erase(
338 symbol_map_str.begin(), symbol_map_str.end(), isspace),
339 symbol_map_str.end());
341 for(
const auto &symbol_map_entry :
344 const auto symbol_map_pair =
split_string(symbol_map_entry,
',');
346 if(symbol ==
nullptr)
348 "symbol with id \"" + symbol_map_pair.front() +
349 "\" does not exist in the symbol table");
354 replace_symbol.
insert(old_expr, symbol->symbol_expr());
366 "loop entry must have one identifier");
369 if(invariants_str.empty())
372 "loop entry must have one invariant string");
376 loop_id, invariants_str, assigns_str, decreases_str, replace_symbol);
ansi_c_parsert ansi_c_parser
void ansi_c_scanner_init()
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
ANSI-C Language Type Checking.
pointer_typet pointer_type(const typet &subtype)
ansi_c_parse_treet parse_tree
virtual void clear() override
virtual bool parse() override
std::vector< parametert > parameterst
symbol_tablet & symbol_table
message_handlert & message_handler
void configure_functions(const jsont &)
void add_builtin_pointer_function_symbol(std::string function_name, const std::size_t num_of_args)
Add builtin function symbol with function_name into symbol table.
contracts_wranglert(goto_modelt &goto_model, const std::string &file_name, message_handlert &message_handler)
void mangle(const loop_contracts_clauset &loop_contracts, const irep_idt &function_id)
Mangle loop_contracts in the function with function_id
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
std::vector< exprt > operandst
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Class that provides messages with a built-in verbosity 'level'.
message_handlert & get_message_handler()
void set_file(const irep_idt &file)
void set_line_no(unsigned _line_no)
Expression to hold a symbol (variable)
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
irep_idt module
Name of module the symbol belongs to.
The Boolean constant true.
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Parse and annotate contracts.
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
json_objectt & to_json_object(jsont &json)
json_arrayt & to_json_array(jsont &json)
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
nonstd::optional< T > optionalt
API to expression classes for Pointers.
exprt simplify_expr(exprt src, const namespacet &ns)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
std::vector< loop_contracts_clauset > loop_contracts
unchecked_replace_symbolt replace_symbol
Loop id used to identify loops.
void annotate_decreases(const std::map< loop_idt, std::vector< exprt > > &decreases_map, goto_modelt &goto_model)
Annotate the decreases in decreases_map to their corresponding loops.
void annotate_assigns(const std::map< loop_idt, std::set< exprt > > &assigns_map, goto_modelt &goto_model)
Annotate the assigns in assigns_map to their corresponding loops.
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
std::map< loop_idt, exprt > invariant_mapt