cprover
Loading...
Searching...
No Matches
java_trace_validation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java trace validation
4
5Author: Jeannie Moulton
6
7\*******************************************************************/
8
10
11#include <algorithm>
12
14
15#include <util/byte_operators.h>
16#include <util/expr_util.h>
17#include <util/pointer_expr.h>
18#include <util/simplify_expr.h>
19#include <util/std_expr.h>
20
22{
23 const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr);
24 return symbol && !symbol->get_identifier().empty();
25}
26
29static bool may_be_lvalue(const exprt &expr)
30{
31 return can_cast_expr<member_exprt>(expr) ||
37}
38
40{
41 while(expr.has_operands())
42 {
43 expr = to_multi_ary_expr(expr).op0();
44 if(!may_be_lvalue(expr))
45 return {};
46 }
47 if(!check_symbol_structure(expr))
48 return {};
49 return *expr_try_dynamic_cast<symbol_exprt>(expr);
50}
51
53{
54 if(!expr.has_operands())
55 return false;
56 const auto symbol_operand = get_inner_symbol_expr(expr);
57 return symbol_operand.has_value();
58}
59
61{
65}
66
68{
75}
76
77bool can_evaluate_to_constant(const exprt &expression)
78{
79 return can_cast_expr<constant_exprt>(skip_typecast(expression)) ||
82}
83
84bool check_index_structure(const exprt &index_expr)
85{
86 return (can_cast_expr<index_exprt>(index_expr) ||
88 index_expr.operands().size() == 2 &&
89 check_symbol_structure(to_binary_expr(index_expr).op0()) &&
91}
92
94{
95 if(!expr.has_operands())
96 return false;
97 if(const auto sub_struct = expr_try_dynamic_cast<struct_exprt>(expr.op0()))
98 check_struct_structure(*sub_struct);
99 else if(!can_cast_expr<constant_exprt>(expr.op0()))
100 return false;
101 if(
102 expr.operands().size() > 1 &&
103 std::any_of(
104 ++expr.operands().begin(),
105 expr.operands().end(),
106 [&](const exprt &operand) { return operand.id() != ID_constant; }))
107 {
108 return false;
109 }
110 return true;
111}
112
114{
115 const auto symbol_expr = get_inner_symbol_expr(address);
116 return symbol_expr && check_symbol_structure(*symbol_expr);
117}
118
119bool check_constant_structure(const constant_exprt &constant_expr)
120{
121 if(constant_expr.has_operands())
122 {
123 const auto &operand = skip_typecast(constant_expr.operands()[0]);
124 return can_cast_expr<constant_exprt>(operand) ||
127 }
128 // All value types used in Java must be non-empty except string_typet:
129 return !constant_expr.get_value().empty() ||
130 constant_expr.type() == string_typet();
131}
132
134 const exprt &lhs,
135 const namespacet &ns,
136 const validation_modet vm)
137{
139 vm,
141 "LHS",
142 lhs.pretty(),
143 "Unsupported expression.");
144 // check member lhs structure
145 if(const auto member = expr_try_dynamic_cast<member_exprt>(lhs))
146 {
148 vm,
149 check_member_structure(*member),
150 "LHS",
151 lhs.pretty(),
152 "Expecting a member with nested symbol operand.");
153 }
154 // check symbol lhs structure
155 else if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(lhs))
156 {
158 vm,
159 check_symbol_structure(*symbol),
160 "LHS",
161 lhs.pretty(),
162 "Expecting a symbol with non-empty identifier.");
163 }
164 // check index lhs structure
165 else if(const auto index = expr_try_dynamic_cast<index_exprt>(lhs))
166 {
168 vm,
169 check_index_structure(*index),
170 "LHS",
171 lhs.pretty(),
172 "Expecting an index expression with a symbol array and constant or "
173 "symbol index value.");
174 }
175 // check byte extract lhs structure
176 else if(const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(lhs))
177 {
179 vm,
181 "LHS",
182 lhs.pretty(),
183 "Expecting a byte extract expression with a symbol array and constant or "
184 "symbol index value.");
185 }
186 else
187 {
189 vm,
190 false,
191 "LHS",
192 lhs.pretty(),
193 "Expression does not meet any trace assumptions.");
194 }
195}
196
198 const exprt &rhs,
199 const namespacet &ns,
200 const validation_modet vm)
201{
203 vm,
205 "RHS",
206 rhs.pretty(),
207 "Unsupported expression.");
208 // check address_of rhs structure (String only)
209 if(const auto address = expr_try_dynamic_cast<address_of_exprt>(rhs))
210 {
212 vm,
213 check_address_structure(*address),
214 "RHS",
215 rhs.pretty(),
216 "Expecting an address of with nested symbol.");
217 }
218 // check symbol rhs structure (String only)
219 else if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(rhs))
220 {
222 vm,
223 check_symbol_structure(*symbol_expr),
224 "RHS",
225 rhs.pretty(),
226 "Expecting a symbol with non-empty identifier.");
227 }
228 // check struct rhs structure
229 else if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(rhs))
230 {
232 vm,
233 check_struct_structure(*struct_expr),
234 "RHS",
235 rhs.pretty(),
236 "Expecting all non-base class operands to be constants.");
237 }
238 // check array rhs structure
239 else if(can_cast_expr<array_exprt>(rhs))
240 {
241 // seems no check is required.
242 }
243 // check array rhs structure
245 {
246 // seems no check is required.
247 }
248 // check constant rhs structure
249 else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(rhs))
250 {
252 vm,
253 check_constant_structure(*constant_expr),
254 "RHS",
255 rhs.pretty(),
256 "Expecting the first operand of a constant expression to be a constant, "
257 "address_of or plus expression, or no operands and a non-empty value.");
258 }
259 // check byte extract rhs structure
260 else if(const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(rhs))
261 {
263 vm,
264 byte->operands().size() == 2,
265 "RHS",
266 rhs.pretty(),
267 "Expecting a byte extract with two operands.");
269 vm,
271 "RHS",
272 rhs.pretty(),
273 "Expecting a byte extract with constant value.");
275 vm,
276 can_cast_expr<constant_exprt>(simplify_expr(byte->offset(), ns)),
277 "RHS",
278 rhs.pretty(),
279 "Expecting a byte extract with constant index.");
280 }
281 else
282 {
284 vm,
285 false,
286 "RHS",
287 rhs.pretty(),
288 "Expression does not meet any trace assumptions.");
289 }
290}
291
293 const goto_trace_stept &step,
294 const namespacet &ns,
295 const validation_modet vm)
296{
297 if(!step.is_assignment() && !step.is_decl())
298 return;
301}
302
304 const goto_tracet &trace,
305 const namespacet &ns,
306 const messaget &log,
307 const bool run_check,
308 const validation_modet vm)
309{
310 if(!run_check)
311 return;
312 for(const auto &step : trace.steps)
313 check_step_assumptions(step, ns, vm);
314 log.status() << "Trace validation successful" << messaget::eom;
315}
Expression classes for byte-level operators.
bool can_cast_expr< byte_extract_exprt >(const exprt &base)
Operator to return the address of an object.
Definition: pointer_expr.h:361
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
bool is_assignment() const
Definition: goto_trace.h:55
exprt full_lhs_value
Definition: goto_trace.h:132
bool is_decl() const
Definition: goto_trace.h:65
Trace of a GOTO program.
Definition: goto_trace.h:175
stepst steps
Definition: goto_trace.h:178
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
Extract member of struct or union.
Definition: std_expr.h:2667
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
exprt & op0()
Definition: std_expr.h:844
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
String type.
Definition: std_types.h:901
Struct constructor from list of elements.
Definition: std_expr.h:1722
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
Deprecated expression utility functions.
Traces of GOTO Programs.
bool valid_lhs_expr_high_level(const exprt &lhs)
static void check_step_assumptions(const goto_trace_stept &step, const namespacet &ns, const validation_modet vm)
bool check_address_structure(const address_of_exprt &address)
bool valid_rhs_expr_high_level(const exprt &rhs)
optionalt< symbol_exprt > get_inner_symbol_expr(exprt expr)
Recursively extracts the first operand of an expression until it reaches a symbol and returns it,...
bool check_member_structure(const member_exprt &expr)
bool check_index_structure(const exprt &index_expr)
bool check_symbol_structure(const exprt &expr)
static bool may_be_lvalue(const exprt &expr)
void check_trace_assumptions(const goto_tracet &trace, const namespacet &ns, const messaget &log, const bool run_check, const validation_modet vm)
Checks that the structure of each step of the trace matches certain criteria.
bool check_constant_structure(const constant_exprt &constant_expr)
static void check_lhs_assumptions(const exprt &lhs, const namespacet &ns, const validation_modet vm)
static void check_rhs_assumptions(const exprt &rhs, const namespacet &ns, const validation_modet vm)
bool can_evaluate_to_constant(const exprt &expression)
bool check_struct_structure(const struct_exprt &expr)
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:382
exprt simplify_expr(exprt src, const namespacet &ns)
API to expression classes.
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:1938
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1734
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:937
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2829
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1375
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:173
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:2735
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1547
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1495
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Definition: validate.h:37
validation_modet