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_util.h>
17 #include <util/pointer_expr.h>
18 #include <util/simplify_expr.h>
19 #include <util/std_expr.h>
20 
21 bool check_symbol_structure(const exprt &expr)
22 {
23  const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr);
24  return symbol && !symbol->get_identifier().empty();
25 }
26 
29 static 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 
77 bool can_evaluate_to_constant(const exprt &expression)
78 {
79  return can_cast_expr<constant_exprt>(skip_typecast(expression)) ||
82 }
83 
84 bool check_index_structure(const exprt &index_expr)
85 {
86  return (can_cast_expr<index_exprt>(index_expr) ||
87  can_cast_expr<byte_extract_exprt>(index_expr)) &&
88  index_expr.operands().size() == 2 &&
89  check_symbol_structure(to_binary_expr(index_expr).op0()) &&
90  can_evaluate_to_constant(to_binary_expr(index_expr).op1());
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 
119 bool 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) ||
126  can_cast_expr<plus_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,
180  check_index_structure(*byte),
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
244  else if(can_cast_expr<array_list_exprt>(rhs))
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
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
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)
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,...
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)
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
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:937
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2829
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
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< 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