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());
143 ansi_c_parser.set_line_no(0);
144 ansi_c_parser.set_file(
"<predicate>");
145 ansi_c_parser.in = &is;
152 ansi_c_parser.cpp98 =
false;
153 ansi_c_parser.cpp11 =
false;
156 ansi_c_parser.parse();
159 exprt &inv_expr(
static_cast<exprt &
>(ansi_c_parser.parse_tree.items.front()
163 .add(ID_C_spec_loop_invariant))
166 log.debug() <<
"Extracted loop invariants: " << inv_expr.
pretty() <<
"\n"
170 std::optional<exprt> assigns_expr;
171 if(!loop_contracts.
assigns.empty())
173 assigns_expr =
static_cast<exprt &
>(ansi_c_parser.parse_tree.items.front()
177 .add(ID_C_spec_assigns))
185 for(
auto op :
static_cast<exprt &
>(ansi_c_parser.parse_tree.items.front()
189 .add(ID_C_spec_decreases))
192 decreases_exprs.emplace_back(op);
197 log.debug() <<
"Start to replace symbols" <<
log.eom;
199 if(assigns_expr.has_value())
203 for(
exprt &decrease_expr : decreases_exprs)
217 ansi_c_parser.parse_tree,
220 log.get_message_handler());
224 log.debug() <<
"Start to typecheck invariants." <<
log.eom;
228 "old is not allowed in loop invariants.");
237 log.debug() <<
"Start to typecheck assigns." <<
log.eom;
238 if(assigns_expr.has_value())
244 assigns_expr.value();
249 log.debug() <<
"Start to typecheck decreases." <<
log.eom;
250 if(!decreases_exprs.empty())
252 std::map<loop_idt, std::vector<exprt>> decreases_map;
254 std::vector<exprt>();
255 for(
exprt &decrease_expr : decreases_exprs)
259 .emplace_back(decrease_expr);
264 log.debug() <<
"Mangling finished." <<
log.eom;
285 if(!
function.is_object())
290 const auto function_name = function_entry.first;
291 const auto &items = function_entry.second;
293 if(!items.is_array())
298 function_config.
regex_str = function_name;
302 if(!function_item.is_object())
305 std::string loop_id =
"";
306 std::string invariants_str =
"";
307 std::string assigns_str =
"";
308 std::string decreases_str =
"";
313 if(!loop_item.second.is_string())
316 if(loop_item.first ==
"loop_id")
318 loop_id = loop_item.second.value;
322 if(loop_item.first ==
"assigns")
324 assigns_str = loop_item.second.value;
328 if(loop_item.first ==
"decreases")
330 decreases_str = loop_item.second.value;
334 if(loop_item.first ==
"invariants")
336 invariants_str = loop_item.second.value;
340 if(loop_item.first ==
"symbol_map")
342 std::string symbol_map_str = loop_item.second.value;
345 symbol_map_str.erase(
347 symbol_map_str.begin(), symbol_map_str.end(),
isspace),
348 symbol_map_str.end());
350 for(
const auto &symbol_map_entry :
353 const auto symbol_map_pair =
split_string(symbol_map_entry,
',');
355 if(symbol ==
nullptr)
357 "symbol with id \"" + symbol_map_pair.front() +
358 "\" does not exist in the symbol table");
363 replace_symbol.
insert(old_expr, symbol->symbol_expr());
375 "loop entry must have one identifier");
378 if(invariants_str.empty())
381 "loop entry must have one invariant string");
385 loop_id, invariants_str, assigns_str, decreases_str, replace_symbol);
void ansi_c_scanner_init(ansi_c_parsert &)
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)
std::vector< parametert > parameterst
struct configt::ansi_ct ansi_c
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'.
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.
const symbolt & lookup_ref(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.
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_arrayt & to_json_array(jsont &json)
json_objectt & to_json_object(jsont &json)
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
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)
bool ts_18661_3_Floatn_types
bool __float128_is_keyword
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_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_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.
std::map< loop_idt, exprt > invariant_mapt