cprover
Loading...
Searching...
No Matches
dfcc_obeys_contract.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: Remi Delmas, delmasrd@amazon.com
6Date: August 2022
7
8\*******************************************************************/
9
10#include "dfcc_obeys_contract.h"
11
12#include <util/cprover_prefix.h>
13#include <util/pointer_expr.h>
14#include <util/prefix.h>
15#include <util/symbol.h>
16
18
19#include "dfcc_cfg_info.h"
20#include "dfcc_library.h"
21
23 dfcc_libraryt &library,
24 message_handlert &message_handler)
25 : library(library), message_handler(message_handler), log(message_handler)
26{
27}
28
30 goto_programt &program,
31 dfcc_cfg_infot &cfg_info,
32 std::set<irep_idt> &function_pointer_contracts)
33{
35 program,
36 program.instructions.begin(),
37 program.instructions.end(),
38 cfg_info,
39 function_pointer_contracts);
40}
41
43 const exprt &expr,
44 std::set<irep_idt> &function_pointer_contracts)
45{
46 PRECONDITION(expr.id() == ID_typecast || expr.id() == ID_address_of);
47
48 if(expr.id() == ID_typecast)
49 {
50 get_contract_name(to_typecast_expr(expr).op(), function_pointer_contracts);
51 }
52 else
53 {
55 to_address_of_expr(expr).object().id() == ID_symbol,
56 "symbol expression expected");
57 function_pointer_contracts.insert(
58 to_symbol_expr(to_address_of_expr(expr).object()).get_identifier());
59 }
60}
61
63 goto_programt &program,
66 dfcc_cfg_infot &cfg_info,
67 std::set<irep_idt> &function_pointer_contracts)
68{
69 for(auto &target = first_instruction; target != last_instruction; target++)
70 {
71 if(target->is_function_call())
72 {
73 const auto &function = target->call_function();
74
75 if(function.id() == ID_symbol)
76 {
77 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
78
79 if(has_prefix(id2string(fun_name), CPROVER_PREFIX "obeys_contract"))
80 {
81 // add address_of on first operand
82 target->call_arguments()[0] =
83 address_of_exprt(target->call_arguments()[0]);
84
85 // fix the function name.
86 to_symbol_expr(target->call_function())
87 .set_identifier(
89
90 // pass the write_set
91 target->call_arguments().push_back(cfg_info.get_write_set(target));
92
93 // record discovered function contract
95 target->call_arguments()[1], function_pointer_contracts);
96 }
97 }
98 }
99 }
100}
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable for that instruction.
Class interface to library types and functions defined in cprover_contracts.c.
std::map< dfcc_funt, symbolt > dfcc_fun_symbol
Maps enum values to the actual function symbols (dynamically loaded)
dfcc_obeys_contractt(dfcc_libraryt &library, message_handlert &message_handler)
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Rewrites calls to obeys_contract predicates into calls to the library implementation in the given pro...
void get_contract_name(const exprt &expr, std::set< irep_idt > &function_pointer_contracts)
Extracts the name from the second argument of a call to obeys_contract (modulo any intermediate typec...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
const irep_idt & id() const
Definition irep.h:396
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Dynamic frame condition checking library loading.
Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clause...
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
Symbol table entry.