cprover
Loading...
Searching...
No Matches
dfcc_pointer_in_range.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
11
12#include <util/cprover_prefix.h>
13#include <util/pointer_expr.h>
14#include <util/replace_expr.h>
15#include <util/std_code.h>
16#include <util/symbol.h>
17
18#include "dfcc_cfg_info.h"
19#include "dfcc_library.h"
20
22 dfcc_libraryt &library,
23 message_handlert &message_handler)
24 : library(library), message_handler(message_handler), log(message_handler)
25{
26}
27
29 goto_programt &program,
30 dfcc_cfg_infot cfg_info)
31{
33 program,
34 program.instructions.begin(),
35 program.instructions.end(),
36 cfg_info);
37}
38
40 goto_programt &program,
41 goto_programt::targett first_instruction,
42 const goto_programt::targett &last_instruction,
43 dfcc_cfg_infot cfg_info)
44{
45 auto &target = first_instruction;
46 while(target != last_instruction)
47 {
48 if(target->is_function_call())
49 {
50 const auto &function = target->call_function();
51
52 if(function.id() == ID_symbol)
53 {
54 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
55
56 if(fun_name == CPROVER_PREFIX "pointer_in_range_dfcc")
57 {
58 // add address on second operand
59 target->call_arguments()[1] =
60 address_of_exprt(target->call_arguments()[1]);
61
62 // fix the function name.
63 to_symbol_expr(target->call_function())
66
67 // pass the write_set
68 target->call_arguments().push_back(cfg_info.get_write_set(target));
69 }
70 }
71 }
72 target++;
73 }
74}
Operator to return the address of an object.
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 to use for the given instruction Returns the write set for the loop,...
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)
void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info)
Rewrites calls to pointer_in_range predicates into calls to the library implementation in the given p...
dfcc_pointer_in_ranget(dfcc_libraryt &library, message_handlert &message_handler)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:155
const irep_idt & get_identifier() const
Definition std_expr.h:160
#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.
@ POINTER_IN_RANGE_DFCC
Instruments occurrences of pointer_in_range predicates in programs encoding requires and ensures clau...
API to expression classes for Pointers.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
Symbol table entry.