CBMC
Loading...
Searching...
No Matches
rewrite_rw_ok.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Rewrite {r,w,rw}_ok expressions as required by symbolic execution
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
9#include "rewrite_rw_ok.h"
10
11#include <util/expr_iterator.h>
12#include <util/pointer_expr.h>
13
15
16static std::optional<exprt> rewrite_rw_ok(exprt expr, const namespacet &ns)
17{
18 bool unchanged = true;
19
20 for(auto it = expr.depth_begin(), itend = expr.depth_end();
21 it != itend;) // no ++it
22 {
24 {
25 const auto &id = it->id();
31 r_or_w_ok->pointer(),
32 r_or_w_ok->size(),
33 ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
34 ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
35 .with_source_location(*it);
36
37 it.mutate() = std::move(replacement);
38 unchanged = false;
39 it.next_sibling_or_parent();
40 }
41 else if(
42 auto pointer_in_range =
44 {
47 pointer_in_range->lower_bound(),
48 pointer_in_range->pointer(),
49 pointer_in_range->upper_bound(),
50 ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
51 ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
52 .with_source_location(*it);
53
54 it.mutate() = std::move(replacement);
55 unchanged = false;
56 it.next_sibling_or_parent();
57 }
58 else
59 ++it;
60 }
61
62 if(unchanged)
63 return {};
64 else
65 return std::move(expr);
66}
67
68static void rewrite_rw_ok(
70 const namespacet &ns)
71{
72 for(auto &instruction : goto_function.body.instructions)
73 instruction.transform(
74 [&ns](exprt expr) { return rewrite_rw_ok(expr, ns); });
75}
76
77void rewrite_rw_ok(goto_modelt &goto_model)
78{
79 const namespacet ns(goto_model.symbol_table);
80
81 for(auto &gf_entry : goto_model.goto_functions.function_map)
82 rewrite_rw_ok(gf_entry.second, ns);
83}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
A base class for a predicate that indicates that an address range is ok to read or write or both.
#define CPROVER_PREFIX
Forward depth-first search iterators These iterators' copy operations are expensive,...
Symbol Table + CFG.
API to expression classes for Pointers.
static std::optional< exprt > rewrite_rw_ok(exprt expr, const namespacet &ns)
Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.