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 #include <util/byte_operators.h>
15 #include <util/expr.h>
16 #include <util/expr_util.h>
17 #include <util/simplify_expr.h>
18 #include <util/std_expr.h>
19 
20 bool check_symbol_structure(const exprt &expr)
21 {
22  const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr);
23  return symbol && !symbol->get_identifier().empty();
24 }
25 
28 static bool may_be_lvalue(const exprt &expr)
29 {
30  return can_cast_expr<member_exprt>(expr) ||
36 }
37 
39 {
40  while(expr.has_operands())
41  {
42  expr = to_multi_ary_expr(expr).op0();
43  if(!may_be_lvalue(expr))
44  return {};
45  }
46  if(!check_symbol_structure(expr))
47  return {};
48  return *expr_try_dynamic_cast<symbol_exprt>(expr);
49 }
50 
52 {
53  if(!expr.has_operands())
54  return false;
55  const auto symbol_operand = get_inner_symbol_expr(expr);
56  return symbol_operand.has_value();
57 }
58 
60 {
64 }
65 
67 {
74 }
75 
76 bool can_evaluate_to_constant(const exprt &expression)
77 {
78  return can_cast_expr<constant_exprt>(skip_typecast(expression)) ||
81 }
82 
83 bool check_index_structure(const exprt &index_expr)
84 {
85  return (can_cast_expr<index_exprt>(index_expr) ||
86  can_cast_expr<byte_extract_exprt>(index_expr)) &&
87  index_expr.operands().size() == 2 &&
88  check_symbol_structure(to_binary_expr(index_expr).op0()) &&
90 }
91 
93 {
94  if(!expr.has_operands())
95  return false;
96  if(const auto sub_struct = expr_try_dynamic_cast<struct_exprt>(expr.op0()))
97  check_struct_structure(*sub_struct);
98  else if(!can_cast_expr<constant_exprt>(expr.op0()))
99  return false;
100  if(
101  expr.operands().size() > 1 &&
102  std::any_of(
103  ++expr.operands().begin(),
104  expr.operands().end(),
105  [&](const exprt &operand) { return operand.id() != ID_constant; }))
106  {
107  return false;
108  }
109  return true;
110 }
111 
113 {
114  const auto symbol_expr = get_inner_symbol_expr(address);
115  return symbol_expr && check_symbol_structure(*symbol_expr);
116 }
117 
118 bool check_constant_structure(const constant_exprt &constant_expr)
119 {
120  if(constant_expr.has_operands())
121  {
122  const auto &operand = skip_typecast(constant_expr.operands()[0]);
123  return can_cast_expr<constant_exprt>(operand) ||
125  can_cast_expr<plus_exprt>(operand);
126  }
127  // All value types used in Java must be non-empty except string_typet:
128  return !constant_expr.get_value().empty() ||
129  constant_expr.type() == string_typet();
130 }
131 
133  const exprt &lhs,
134  const namespacet &ns,
135  const validation_modet vm)
136 {
138  vm,
140  "LHS",
141  lhs.pretty(),
142  "Unsupported expression.");
143  // check member lhs structure
144  if(const auto member = expr_try_dynamic_cast<member_exprt>(lhs))
145  {
147  vm,
148  check_member_structure(*member),
149  "LHS",
150  lhs.pretty(),
151  "Expecting a member with nested symbol operand.");
152  }
153  // check symbol lhs structure
154  else if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(lhs))
155  {
157  vm,
158  check_symbol_structure(*symbol),
159  "LHS",
160  lhs.pretty(),
161  "Expecting a symbol with non-empty identifier.");
162  }
163  // check index lhs structure
164  else if(const auto index = expr_try_dynamic_cast<index_exprt>(lhs))
165  {
167  vm,
168  check_index_structure(*index),
169  "LHS",
170  lhs.pretty(),
171  "Expecting an index expression with a symbol array and constant or "
172  "symbol index value.");
173  }
174  // check byte extract lhs structure
175  else if(const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(lhs))
176  {
178  vm,
179  check_index_structure(*byte),
180  "LHS",
181  lhs.pretty(),
182  "Expecting a byte extract expression with a symbol array and constant or "
183  "symbol index value.");
184  }
185  else
186  {
188  vm,
189  false,
190  "LHS",
191  lhs.pretty(),
192  "Expression does not meet any trace assumptions.");
193  }
194 }
195 
197  const exprt &rhs,
198  const namespacet &ns,
199  const validation_modet vm)
200 {
202  vm,
204  "RHS",
205  rhs.pretty(),
206  "Unsupported expression.");
207  // check address_of rhs structure (String only)
208  if(const auto address = expr_try_dynamic_cast<address_of_exprt>(rhs))
209  {
211  vm,
212  check_address_structure(*address),
213  "RHS",
214  rhs.pretty(),
215  "Expecting an address of with nested symbol.");
216  }
217  // check symbol rhs structure (String only)
218  else if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(rhs))
219  {
221  vm,
222  check_symbol_structure(*symbol_expr),
223  "RHS",
224  rhs.pretty(),
225  "Expecting a symbol with non-empty identifier.");
226  }
227  // check struct rhs structure
228  else if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(rhs))
229  {
231  vm,
232  check_struct_structure(*struct_expr),
233  "RHS",
234  rhs.pretty(),
235  "Expecting all non-base class operands to be constants.");
236  }
237  // check array rhs structure
238  else if(can_cast_expr<array_exprt>(rhs))
239  {
240  // seems no check is required.
241  }
242  // check array rhs structure
243  else if(can_cast_expr<array_list_exprt>(rhs))
244  {
245  // seems no check is required.
246  }
247  // check constant rhs structure
248  else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(rhs))
249  {
251  vm,
252  check_constant_structure(*constant_expr),
253  "RHS",
254  rhs.pretty(),
255  "Expecting the first operand of a constant expression to be a constant, "
256  "address_of or plus expression, or no operands and a non-empty value.");
257  }
258  // check byte extract rhs structure
259  else if(const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(rhs))
260  {
262  vm,
263  byte->operands().size() == 2,
264  "RHS",
265  rhs.pretty(),
266  "Expecting a byte extract with two operands.");
268  vm,
270  "RHS",
271  rhs.pretty(),
272  "Expecting a byte extract with constant value.");
274  vm,
275  can_cast_expr<constant_exprt>(simplify_expr(byte->offset(), ns)),
276  "RHS",
277  rhs.pretty(),
278  "Expecting a byte extract with constant index.");
279  }
280  else
281  {
283  vm,
284  false,
285  "RHS",
286  rhs.pretty(),
287  "Expression does not meet any trace assumptions.");
288  }
289 }
290 
292  const goto_trace_stept &step,
293  const namespacet &ns,
294  const validation_modet vm)
295 {
296  if(!step.is_assignment() && !step.is_decl())
297  return;
300 }
301 
303  const goto_tracet &trace,
304  const namespacet &ns,
305  const messaget &log,
306  const bool run_check,
307  const validation_modet vm)
308 {
309  if(!run_check)
310  return;
311  for(const auto &step : trace.steps)
312  check_step_assumptions(step, ns, vm);
313  log.status() << "Trace validation successful" << messaget::eom;
314 }
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:161
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:302
goto_trace_stept::full_lhs_value
exprt full_lhs_value
Definition: goto_trace.h:132
can_cast_expr< array_list_exprt >
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1503
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
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:38
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:291
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
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:92
valid_lhs_expr_high_level
bool valid_lhs_expr_high_level(const exprt &lhs)
Definition: java_trace_validation.cpp:59
check_symbol_structure
bool check_symbol_structure(const exprt &expr)
Definition: java_trace_validation.cpp:20
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
exprt
Base class for all expressions.
Definition: expr.h:53
exprt::op0
exprt & op0()
Definition: expr.h:102
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:50
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:1451
can_cast_expr< member_exprt >
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:3473
goto_trace_stept::is_decl
bool is_decl() const
Definition: goto_trace.h:65
check_lhs_assumptions
static void check_lhs_assumptions(const exprt &lhs, const namespacet &ns, const validation_modet vm)
Definition: java_trace_validation.cpp:132
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
expr.h
goto_trace_stept::is_assignment
bool is_assignment() const
Definition: goto_trace.h:55
goto_trace.h
Traces of GOTO Programs.
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
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:81
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:83
can_evaluate_to_constant
bool can_evaluate_to_constant(const exprt &expression)
Definition: java_trace_validation.cpp:76
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
can_cast_expr< address_of_exprt >
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:2807
can_cast_expr< plus_exprt >
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:904
goto_trace_stept::full_lhs
exprt full_lhs
Definition: goto_trace.h:126
check_member_structure
bool check_member_structure(const member_exprt &expr)
Definition: java_trace_validation.cpp:51
exprt::op1
exprt & op1()
Definition: expr.h:105
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
check_rhs_assumptions
static void check_rhs_assumptions(const exprt &rhs, const namespacet &ns, const validation_modet vm)
Definition: java_trace_validation.cpp:196
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:112
simplify_expr.h
can_cast_expr< index_exprt >
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1331
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
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:66
may_be_lvalue
static bool may_be_lvalue(const exprt &expr)
Definition: java_trace_validation.cpp:28
string_typet
String type.
Definition: std_types.h:1655
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
can_cast_expr< typecast_exprt >
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2031
check_constant_structure
bool check_constant_structure(const constant_exprt &constant_expr)
Definition: java_trace_validation.cpp:118
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:3928
exprt::operands
operandst & operands()
Definition: expr.h:95
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
can_cast_expr< struct_exprt >
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1645
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:866
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914