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