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 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)
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:39
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:137
const irep_idt & get_identifier() const
Definition std_expr.h:142
#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:222
Symbol table entry.