cprover
Loading...
Searching...
No Matches
contracts_wrangler.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Parse and annotate contracts from configuration files
4
5Author: Qinheping Hu
6
7Date: June 2023
8
9\*******************************************************************/
10
13
14#include "contracts_wrangler.h"
15
16#include <util/c_types.h>
17#include <util/expr_iterator.h>
18#include <util/format_expr.h>
19#include <util/pointer_expr.h>
20#include <util/simplify_expr.h>
21#include <util/std_types.h>
22
24
28
30 goto_modelt &goto_model,
31 const std::string &file_name,
32 message_handlert &message_handler)
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)
38{
39 jsont configuration;
40
41 if(parse_json(file_name, message_handler, configuration))
42 throw deserialization_exceptiont(file_name + " is not a valid JSON file");
43
44 configure_functions(configuration);
45
46 // Mangle loop contracts function by function.
47 // We match function with a regex. There should one and only one function
48 // with name matched by the regex.
49 for(const auto &function_entry : this->functions)
50 {
51 bool function_found = false;
52
53 for(const auto &function : goto_model.goto_functions.function_map)
54 {
55 // We find a matched function.
56 if(std::regex_match(function.first.c_str(), function_entry.first))
57 {
60 "function regex " + function_entry.second.regex_str +
61 " matches more than one function");
62
63 function_found = true;
64
65 // Mangle all loop contracts in the function.
66 for(const auto &loop_entry : function_entry.second.loop_contracts)
67 {
68 mangle(loop_entry, function.first);
69 }
70 }
71 }
72
75 "function regex " + function_entry.second.regex_str +
76 " matches no function");
77 }
78}
79
81 std::string function_name,
82 const std::size_t num_of_args)
83{
84 // Already exist.
85 if(symbol_table.has_symbol(CPROVER_PREFIX + function_name))
86 return;
87
88 code_typet::parameterst parameters;
89 for(unsigned i = 0; i < num_of_args; i++)
90 {
91 parameters.emplace_back(pointer_type(void_type()));
92 }
94 CPROVER_PREFIX + function_name,
95 code_typet(parameters, empty_typet()),
96 ID_C);
98}
99
101 const loop_contracts_clauset &loop_contracts,
102 const irep_idt &function_id)
103{
105 // Loop contracts mangling consists of four steps.
106 //
107 // 1. Construct a fake function with a fake loop that contains the loop
108 // contracts for parsing the contracts.
109 // 2. Parse the fake function and extract the contracts as exprt.
110 // 3. Replace symbols in the extracted exprt with the symbols in the
111 // symbol table of the goto model according to the symbol map provided by
112 // the user.
113 // 4. Typecheck all contracts exprt.
114 // 5. Annotate all contracts exprt to the corresponding loop.
115
116 // Construct a fake function to parse.
117 // void function_id()
118 // {
119 // while(1==1)
120 // __CPROVER_assigns(assigns_str) // optional
121 // __CPROVER_loop_invariant(invariants_str)
122 // __CPROVER_decreases(decreases_str) // optional
123 // }
124 std::ostringstream pr;
125 pr << "void _fn() { while(1==1)";
126 if(!loop_contracts.assigns.empty())
127 {
128 pr << CPROVER_PREFIX << "assigns(" << loop_contracts.assigns << ") ";
129 }
130 pr << CPROVER_PREFIX << "loop_invariant(" << loop_contracts.invariants
131 << ") ";
132 if(!loop_contracts.decreases.empty())
133 {
134 pr << CPROVER_PREFIX << "decreases(" << loop_contracts.decreases << ") ";
135 }
136 pr << " {}}" << std::endl;
137
138 log.debug() << "Constructing fake function:\n" << pr.str() << log.eom;
139
140 // Parse the fake function.
141 std::istringstream is(pr.str());
144 ansi_c_parser.set_file("<predicate>");
148
149 // Extract the invariants from prase_tree.
150 exprt &inv_expr(static_cast<exprt &>(ansi_c_parser.parse_tree.items.front()
151 .declarator()
152 .value()
153 .operands()[0]
155 .operands()[0]);
156
157 log.debug() << "Extracted loop invariants: " << inv_expr.pretty() << "\n"
158 << log.eom;
159
160 // Extract the assigns from parse_tree.
162 if(!loop_contracts.assigns.empty())
163 {
164 assigns_expr = static_cast<exprt &>(ansi_c_parser.parse_tree.items.front()
165 .declarator()
166 .value()
167 .operands()[0]
168 .add(ID_C_spec_assigns))
169 .operands()[0];
170 }
171
172 // Extract the decreases from parse_tree.
174 if(!loop_contracts.decreases.empty())
175 {
176 for(auto op : static_cast<exprt &>(ansi_c_parser.parse_tree.items.front()
177 .declarator()
178 .value()
179 .operands()[0]
181 .operands())
182 {
183 decreases_exprs.emplace_back(op);
184 }
185 }
186
187 // Replace symbols in the clauses with the symbols in the symbol table.
188 log.debug() << "Start to replace symbols" << log.eom;
189 loop_contracts.replace_symbol(inv_expr);
190 if(assigns_expr.has_value())
191 {
192 loop_contracts.replace_symbol(assigns_expr.value());
193 }
195 {
196 loop_contracts.replace_symbol(decrease_expr);
197 }
198
199 // Add builtin functions that might be used in contracts to the symbol table.
201 add_builtin_pointer_function_symbol("same_object", 2);
202 add_builtin_pointer_function_symbol("OBJECT_SIZE", 1);
203 add_builtin_pointer_function_symbol("POINTER_OBJECT", 1);
204 add_builtin_pointer_function_symbol("POINTER_OFFSET", 1);
205
206 // Typecheck clauses.
210 symbol_table.lookup_ref(function_id).module.c_str(),
211 log.get_message_handler());
212
213 // Typecheck and annotate invariants.
214 {
215 log.debug() << "Start to typecheck invariants." << log.eom;
216 ansi_c_typecheck.typecheck_expr(inv_expr);
219 "old is not allowed in loop invariants.");
220
222 inv_map[loop_idt(function_id, std::stoi(loop_contracts.identifier))] =
225 }
226
227 // Typecheck and annotate assigns.
228 log.debug() << "Start to typecheck assigns." << log.eom;
229 if(assigns_expr.has_value())
230 {
231 ansi_c_typecheck.typecheck_spec_assigns(assigns_expr.value().operands());
232
233 invariant_mapt assigns_map;
234 assigns_map[loop_idt(function_id, std::stoi(loop_contracts.identifier))] =
235 assigns_expr.value();
236 annotate_assigns(assigns_map, goto_model);
237 }
238
239 // Typecheck an annotate decreases.
240 log.debug() << "Start to typecheck decreases." << log.eom;
241 if(!decreases_exprs.empty())
242 {
243 std::map<loop_idt, std::vector<exprt>> decreases_map;
244 decreases_map[loop_idt(function_id, std::stoi(loop_contracts.identifier))] =
245 std::vector<exprt>();
247 {
248 ansi_c_typecheck.typecheck_expr(decrease_expr);
249 decreases_map[loop_idt(function_id, std::stoi(loop_contracts.identifier))]
250 .emplace_back(decrease_expr);
251 }
253 }
254
255 log.debug() << "Mangling finished." << log.eom;
256 // Remove added symbol.
257 symbol_table.remove(CPROVER_PREFIX "loop_entry");
258 symbol_table.remove(CPROVER_PREFIX "same_object");
259 symbol_table.remove(CPROVER_PREFIX "OBJECT_SIZE");
260 symbol_table.remove(CPROVER_PREFIX "POINTER_OBJECT");
261 symbol_table.remove(CPROVER_PREFIX "POINTER_OFFSET");
262}
263
265{
266 auto functions = config["functions"];
267
268 if(functions.is_null())
269 return;
270
271 if(!functions.is_array())
272 throw deserialization_exceptiont("functions entry must be sequence");
273
274 for(const auto &function : to_json_array(functions))
275 {
276 if(!function.is_object())
277 throw deserialization_exceptiont("function entry must be object");
278
279 for(const auto &function_entry : to_json_object(function))
280 {
281 const auto function_name = function_entry.first;
282 const auto &items = function_entry.second;
283
284 if(!items.is_array())
285 throw deserialization_exceptiont("loops entry must be sequence");
286
287 this->functions.emplace_back(function_name, functiont{});
288 functiont &function_config = this->functions.back().second;
289 function_config.regex_str = function_name;
290
291 for(const auto &function_item : to_json_array(items))
292 {
293 if(!function_item.is_object())
294 throw deserialization_exceptiont("loop entry must be object");
295
296 std::string loop_id = "";
297 std::string invariants_str = "";
298 std::string assigns_str = "";
299 std::string decreases_str = "";
300 unchecked_replace_symbolt replace_symbol;
301
302 for(const auto &loop_item : to_json_object(function_item))
303 {
304 if(!loop_item.second.is_string())
305 throw deserialization_exceptiont("loop item must be string");
306
307 if(loop_item.first == "loop_id")
308 {
309 loop_id = loop_item.second.value;
310 continue;
311 }
312
313 if(loop_item.first == "assigns")
314 {
315 assigns_str = loop_item.second.value;
316 continue;
317 }
318
319 if(loop_item.first == "decreases")
320 {
321 decreases_str = loop_item.second.value;
322 continue;
323 }
324
325 if(loop_item.first == "invariants")
326 {
327 invariants_str = loop_item.second.value;
328 continue;
329 }
330
331 if(loop_item.first == "symbol_map")
332 {
333 std::string symbol_map_str = loop_item.second.value;
334
335 // Remove all space in symbol_map_str
336 symbol_map_str.erase(
337 std::remove_if(
338 symbol_map_str.begin(), symbol_map_str.end(), isspace),
339 symbol_map_str.end());
340
341 for(const auto &symbol_map_entry :
343 {
345 const auto &symbol = symbol_table.lookup(symbol_map_pair.back());
346 if(symbol == nullptr)
348 "symbol with id \"" + symbol_map_pair.front() +
349 "\" does not exist in the symbol table");
350 // Create a dummy symbol. The type will be discarded when inserted
351 // into replace_symbol.
353 symbol_map_pair.front(), bool_typet());
354 replace_symbol.insert(old_expr, symbol->symbol_expr());
355 }
356
357 continue;
358 }
359
360 throw deserialization_exceptiont("unexpected loop item");
361 }
362
363 if(loop_id.empty())
364 {
366 "loop entry must have one identifier");
367 }
368
369 if(invariants_str.empty())
370 {
372 "loop entry must have one invariant string");
373 }
374
375 function_config.loop_contracts.emplace_back(
376 loop_id, invariants_str, assigns_str, decreases_str, replace_symbol);
377 }
378 }
379 }
380}
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.
configt config
Definition config.cpp:25
empty_typet void_type()
Definition c_types.cpp:250
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
ansi_c_parse_treet parse_tree
virtual void clear() override
virtual bool parse() override
The Boolean type.
Definition std_types.h:36
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
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.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
operandst & operands()
Definition expr.h:94
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
Thrown when user-provided input cannot be processed.
Definition json.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
static eomt eom
Definition message.h:297
std::istream * in
Definition parser.h:26
void set_file(const irep_idt &file)
Definition parser.h:85
void set_line_no(unsigned _line_no)
Definition parser.h:80
Expression to hold a symbol (variable)
Definition std_expr.h:113
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.
Symbol table entry.
Definition symbol.h:28
The Boolean constant true.
Definition std_expr.h:3008
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Parse and annotate contracts.
#define CPROVER_PREFIX
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)
Definition json.h:444
json_arrayt & to_json_array(jsont &json)
Definition json.h:426
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
API to expression classes for Pointers.
Unused function removal.
exprt simplify_expr(exprt src, const namespacet &ns)
Pre-defined types.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
std::string regex_str
unchecked_replace_symbolt replace_symbol
Loop id used to identify loops.
Definition loop_ids.h:28
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.
Definition utils.cpp:761
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.
Definition utils.cpp:720
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
Definition utils.cpp:700
std::map< loop_idt, exprt > invariant_mapt
Definition utils.h:30