CBMC
Loading...
Searching...
No Matches
graphml_witness.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Witnesses for Traces and Proofs
4
5Author: Daniel Kroening
6
7\*******************************************************************/
8
11
12#include "graphml_witness.h"
13
14#include <util/arith_tools.h>
15#include <util/byte_operators.h>
16#include <util/c_types.h>
17#include <util/cprover_prefix.h>
18#include <util/namespace.h>
20#include <util/prefix.h>
21#include <util/ssa_expr.h>
23#include <util/symbol.h>
24
25#include <ansi-c/expr2c.h>
28#include <langapi/mode.h>
29
30#include "goto_program.h"
31#include "goto_trace.h"
32
33static std::string
34expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
35{
36 if(get_mode_from_identifier(ns, id) == ID_C)
38 else
39 return from_expr(ns, id, expr);
40}
41
43{
44 if(expr.id()==ID_symbol)
45 {
46 if(is_ssa_expr(expr))
47 expr=to_ssa_expr(expr).get_original_expr();
48 else
49 {
50 std::string identifier=
51 id2string(to_symbol_expr(expr).get_identifier());
52
53 std::string::size_type l0_l1=identifier.find_first_of("!@");
54 if(l0_l1!=std::string::npos)
55 {
56 identifier.resize(l0_l1);
57 to_symbol_expr(expr).set_identifier(identifier);
58 }
59 }
60
61 return;
62 }
63 else if(expr.id() == ID_string_constant)
64 {
65 std::string output_string = expr_to_string(ns, "", expr);
67 expr = to_string_constant(expr).to_array_expr();
68 }
69
70 Forall_operands(it, expr)
71 remove_l0_l1(*it);
72}
73
75 const irep_idt &identifier,
76 const code_assignt &assign)
77{
78 const auto cit = cache.find({identifier.get_no(), &assign.read()});
79 if(cit != cache.end())
80 return cit->second;
81
82 std::string result;
83
84 if(assign.rhs().id() == ID_array_list)
85 {
87 const auto &ops = array_list.operands();
88
89 for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2)
90 {
91 const index_exprt index{assign.lhs(), ops[listidx]};
92 if(!result.empty())
93 result += ' ';
94 result +=
95 convert_assign_rec(identifier, code_assignt{index, ops[listidx + 1]});
96 }
97 }
98 else if(assign.rhs().id() == ID_array)
99 {
100 const array_typet &type = to_array_type(assign.rhs().type());
101
102 unsigned i=0;
103 for(const auto &op : assign.rhs().operands())
104 {
105 index_exprt index(
106 assign.lhs(), from_integer(i++, c_index_type()), type.element_type());
107 if(!result.empty())
108 result+=' ';
109 result += convert_assign_rec(identifier, code_assignt(index, op));
110 }
111 }
112 else if(assign.rhs().id()==ID_struct ||
113 assign.rhs().id()==ID_union)
114 {
115 // dereferencing may have resulted in an lhs that is the first
116 // struct member; undo this
117 if(
118 assign.lhs().id() == ID_member &&
119 assign.lhs().type() != assign.rhs().type())
120 {
121 code_assignt tmp=assign;
122 tmp.lhs()=to_member_expr(assign.lhs()).struct_op();
123
124 return convert_assign_rec(identifier, tmp);
125 }
126 else if(assign.lhs().id()==ID_byte_extract_little_endian ||
128 {
129 code_assignt tmp=assign;
130 tmp.lhs()=to_byte_extract_expr(assign.lhs()).op();
131
132 return convert_assign_rec(identifier, tmp);
133 }
134
135 const typet &lhs_type = assign.lhs().type();
136 const struct_union_typet::componentst &components =
137 (lhs_type.id() == ID_struct_tag || lhs_type.id() == ID_union_tag)
138 ? ns.follow_tag(to_struct_or_union_tag_type(lhs_type)).components()
139 : to_struct_union_type(lhs_type).components();
140
141 exprt::operandst::const_iterator it=
142 assign.rhs().operands().begin();
143 for(const auto &comp : components)
144 {
146 comp.type().id() != ID_code, "struct member must not be of code type");
147 if(
148 comp.get_is_padding() ||
149 // for some reason #is_padding gets lost in *some* cases
150 comp.get_name().starts_with("$pad"))
151 continue;
152
153 INVARIANT(
154 it != assign.rhs().operands().end(), "expression must have operands");
155
156 member_exprt member(
157 assign.lhs(),
158 comp.get_name(),
159 it->type());
160 if(!result.empty())
161 result+=' ';
162 result+=convert_assign_rec(identifier, code_assignt(member, *it));
163 ++it;
164
165 // for unions just assign to the first member
166 if(assign.rhs().id()==ID_union)
167 break;
168 }
169 }
170 else if(assign.rhs().id() == ID_with)
171 {
172 const with_exprt &with_expr = to_with_expr(assign.rhs());
173
174 if(!result.empty())
175 result += ' ';
176
177 if(with_expr.where().id() == ID_member_name)
178 {
179 const member_exprt member{
180 assign.lhs(),
181 with_expr.where().get(ID_component_name),
182 with_expr.new_value().type()};
183 result += convert_assign_rec(
184 identifier, code_assignt(member, with_expr.new_value()));
185 }
186 else
187 {
188 const index_exprt index{assign.lhs(), with_expr.where()};
189 result += convert_assign_rec(
190 identifier, code_assignt(index, with_expr.new_value()));
191 }
192 }
193 else
194 {
195 exprt clean_rhs=assign.rhs();
197
198 exprt clean_lhs = assign.lhs();
200 std::string lhs = expr_to_string(ns, identifier, clean_lhs);
201
202 if(
203 lhs.find("#return_value") != std::string::npos ||
204 (lhs.find('$') != std::string::npos &&
205 has_prefix(lhs, "return_value___VERIFIER_nondet_")))
206 {
207 lhs="\\result";
208 }
209
210 result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
211 }
212
213 cache.insert({{identifier.get_no(), &assign.read()}, result});
214 return result;
215}
216
217static bool filter_out(
218 const goto_tracet &goto_trace,
219 const goto_tracet::stepst::const_iterator &prev_it,
220 goto_tracet::stepst::const_iterator &it)
221{
222 if(
223 it->hidden &&
224 (!it->pc->is_assign() || it->pc->assign_rhs().id() != ID_side_effect ||
225 it->pc->assign_rhs().get(ID_statement) != ID_nondet))
226 return true;
227
228 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
229 return true;
230
231 // we filter out steps with the same source location
232 // TODO: if these are assignments we should accumulate them into
233 // a single edge
234 if(
235 prev_it != goto_trace.steps.end() &&
236 prev_it->pc->source_location() == it->pc->source_location())
237 return true;
238
239 if(it->is_goto() && it->pc->condition().is_true())
240 return true;
241
242 const source_locationt &source_location = it->pc->source_location();
243
244 if(source_location.is_nil() ||
245 source_location.get_file().empty() ||
246 source_location.is_built_in() ||
247 source_location.get_line().empty())
248 {
249 const irep_idt id = source_location.get_function();
250 // Do not filter out assertions in functions the name of which starts with
251 // CPROVER_PREFIX, because we need to maintain those as violation nodes:
252 // these are assertions generated, for examples, for memory leaks.
253 if(!id.starts_with(CPROVER_PREFIX) || !it->is_assert())
254 return true;
255 }
256
257 return false;
258}
259
260static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
261{
262 if(
263 expr.id() == ID_symbol &&
264 to_symbol_expr(expr).get_identifier().starts_with(prefix))
265 {
266 return true;
267 }
268
269 for(const auto &op : expr.operands())
270 {
271 if(contains_symbol_prefix(op, prefix))
272 return true;
273 }
274 return false;
275}
276
279{
280 unsigned int max_thread_idx = 0;
281 bool trace_has_violation = false;
282 for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin();
283 it != goto_trace.steps.end();
284 ++it)
285 {
286 if(it->thread_nr > max_thread_idx)
287 max_thread_idx = it->thread_nr;
288 if(it->is_assert() && !it->cond_value)
289 trace_has_violation = true;
290 }
291
292 graphml.key_values["sourcecodelang"]="C";
293
295 graphml[sink].node_name="sink";
296 graphml[sink].is_violation=false;
297 graphml[sink].has_invariant=false;
298
300 {
301 std::vector<graphmlt::node_indext> nodes;
302
303 for(unsigned int i = 0; i <= max_thread_idx + 1; ++i)
304 {
305 nodes.push_back(graphml.add_node());
306 graphml[nodes.back()].node_name = "N" + std::to_string(i);
307 graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
308 graphml[nodes.back()].has_invariant = false;
309 }
310
311 for(auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
312 {
313 xmlt edge("edge");
314 edge.set_attribute("source", graphml[*it].node_name);
315 edge.set_attribute("target", graphml[*std::next(it)].node_name);
316 const auto thread_id = std::distance(nodes.cbegin(), it);
317 xmlt &data = edge.new_element("data");
318 data.set_attribute("key", "createThread");
319 data.data = std::to_string(thread_id);
320 if(thread_id == 0)
321 {
322 xmlt &data = edge.new_element("data");
323 data.set_attribute("key", "enterFunction");
324 data.data = "main";
325 }
326 graphml[*std::next(it)].in[*it].xml_node = edge;
327 graphml[*it].out[*std::next(it)].xml_node = edge;
328 }
329
330 // we do not provide any further details as CPAchecker does not seem to
331 // handle more detailed concurrency witnesses
332 return;
333 }
334
335 // step numbers start at 1
336 std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
337
338 goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end();
339 for(goto_tracet::stepst::const_iterator
340 it=goto_trace.steps.begin();
341 it!=goto_trace.steps.end();
342 it++) // we cannot replace this by a ranged for
343 {
345 {
346 step_to_node[it->step_nr]=sink;
347
348 continue;
349 }
350
351 // skip declarations followed by an immediate assignment
352 goto_tracet::stepst::const_iterator next=it;
353 ++next;
354 if(
355 next != goto_trace.steps.end() &&
357 it->full_lhs == next->full_lhs &&
358 it->pc->source_location() == next->pc->source_location())
359 {
360 step_to_node[it->step_nr]=sink;
361
362 continue;
363 }
364
365 prev_it=it;
366
367 const source_locationt &source_location = it->pc->source_location();
368
370 graphml[node].node_name=
371 std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
372 graphml[node].file=source_location.get_file();
373 graphml[node].line=source_location.get_line();
374 graphml[node].is_violation=
375 it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
376 graphml[node].has_invariant=false;
377
378 step_to_node[it->step_nr]=node;
379 }
380
381 unsigned thread_id = 0;
382
383 // build edges
384 for(goto_tracet::stepst::const_iterator
385 it=goto_trace.steps.begin();
386 it!=goto_trace.steps.end();
387 ) // no ++it
388 {
389 const std::size_t from=step_to_node[it->step_nr];
390
391 // no outgoing edges from sinks or violation nodes
392 if(from == sink || graphml[from].is_violation)
393 {
394 ++it;
395 continue;
396 }
397
398 auto next = std::next(it);
399 for(; next != goto_trace.steps.end() &&
400 (step_to_node[next->step_nr] == sink ||
401 pointee_address_equalt{}(it->pc, next->pc)); // NOLINT
402 ++next)
403 {
404 // advance
405 }
406 const std::size_t to=
407 next==goto_trace.steps.end()?
408 sink:step_to_node[next->step_nr];
409
410 switch(it->type)
411 {
416 {
417 xmlt edge(
418 "edge",
419 {{"source", graphml[from].node_name},
420 {"target", graphml[to].node_name}},
421 {});
422
423 {
424 xmlt &data_f = edge.new_element("data");
425 data_f.set_attribute("key", "originfile");
426 data_f.data = id2string(graphml[from].file);
427
428 xmlt &data_l = edge.new_element("data");
429 data_l.set_attribute("key", "startline");
430 data_l.data = id2string(graphml[from].line);
431
432 xmlt &data_t = edge.new_element("data");
433 data_t.set_attribute("key", "threadId");
434 data_t.data = std::to_string(it->thread_nr);
435 }
436
437 const auto lhs_object = it->get_lhs_object();
438 if(
440 lhs_object.has_value())
441 {
442 const std::string &lhs_id = id2string(lhs_object->get_identifier());
443 if(lhs_id.find("pthread_create::thread") != std::string::npos)
444 {
445 xmlt &data_t = edge.new_element("data");
446 data_t.set_attribute("key", "createThread");
447 data_t.data = std::to_string(++thread_id);
448 }
449 else if(
451 it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "::dynamic_object") &&
453 it->full_lhs, SYMEX_DYNAMIC_PREFIX "::dynamic_object") &&
454 lhs_id.find("thread") == std::string::npos &&
455 lhs_id.find("mutex") == std::string::npos &&
456 (!it->full_lhs_value.is_constant() ||
457 !it->full_lhs_value.has_operands() ||
458 !has_prefix(
459 id2string(
460 to_multi_ary_expr(it->full_lhs_value).op0().get(ID_value)),
461 "INVALID-")))
462 {
463 xmlt &val = edge.new_element("data");
464 val.set_attribute("key", "assumption");
465
466 code_assignt assign{it->full_lhs, it->full_lhs_value};
467 val.data = convert_assign_rec(lhs_id, assign);
468
469 if(!it->function_id.empty())
470 {
471 xmlt &val_s = edge.new_element("data");
472 val_s.set_attribute("key", "assumption.scope");
473 irep_idt function_id = it->function_id;
474 const symbolt *symbol_ptr = nullptr;
475 if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter)
476 {
477 function_id = lhs_id.substr(0, lhs_id.find("::"));
478 }
479 val_s.data = id2string(function_id);
480 }
481
482 if(has_prefix(val.data, "\\result ="))
483 {
484 xmlt &val_f = edge.new_element("data");
485 val_f.set_attribute("key", "assumption.resultfunction");
486 val_f.data = id2string(it->function_id);
487 }
488 }
489 }
490 else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
491 {
492 }
493
494 graphml[to].in[from].xml_node = edge;
495 graphml[from].out[to].xml_node = edge;
496
497 break;
498 }
499
515 // ignore
516 break;
517 }
518
519 it=next;
520 }
521}
522
525{
526 graphml.key_values["sourcecodelang"]="C";
527
529 graphml[sink].node_name="sink";
530 graphml[sink].is_violation=false;
531 graphml[sink].has_invariant=false;
532
533 // step numbers start at 1
534 std::vector<std::size_t> step_to_node(equation.SSA_steps.size()+1, 0);
535
536 std::size_t step_nr=1;
537 for(symex_target_equationt::SSA_stepst::const_iterator
538 it=equation.SSA_steps.begin();
539 it!=equation.SSA_steps.end();
540 it++, step_nr++) // we cannot replace this by a ranged for
541 {
542 const source_locationt &source_location = it->source.pc->source_location();
543
544 if(
545 it->hidden ||
546 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
547 (it->is_goto() && it->source.pc->condition().is_true()) ||
548 source_location.is_nil() || source_location.is_built_in() ||
549 source_location.get_line().empty())
550 {
551 step_to_node[step_nr]=sink;
552
553 continue;
554 }
555
556 // skip declarations followed by an immediate assignment
557 symex_target_equationt::SSA_stepst::const_iterator next=it;
558 ++next;
559 if(
560 next != equation.SSA_steps.end() && next->is_assignment() &&
561 it->ssa_full_lhs == next->ssa_full_lhs &&
562 it->source.pc->source_location() == next->source.pc->source_location())
563 {
564 step_to_node[step_nr]=sink;
565
566 continue;
567 }
568
570 graphml[node].node_name=
571 std::to_string(it->source.pc->location_number)+"."+
572 std::to_string(step_nr);
573 graphml[node].file=source_location.get_file();
574 graphml[node].line=source_location.get_line();
575 graphml[node].is_violation=false;
576 graphml[node].has_invariant=false;
577
578 step_to_node[step_nr]=node;
579 }
580
581 // build edges
582 step_nr=1;
583 for(symex_target_equationt::SSA_stepst::const_iterator
584 it=equation.SSA_steps.begin();
585 it!=equation.SSA_steps.end();
586 ) // no ++it
587 {
588 const std::size_t from=step_to_node[step_nr];
589
590 if(from==sink)
591 {
592 ++it;
593 ++step_nr;
594 continue;
595 }
596
597 symex_target_equationt::SSA_stepst::const_iterator next=it;
598 std::size_t next_step_nr=step_nr;
599 for(++next, ++next_step_nr;
600 next!=equation.SSA_steps.end() &&
601 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
602 ++next, ++next_step_nr)
603 {
604 // advance
605 }
606 const std::size_t to=
607 next==equation.SSA_steps.end()?
609
610 switch(it->type)
611 {
616 {
617 xmlt edge(
618 "edge",
619 {{"source", graphml[from].node_name},
620 {"target", graphml[to].node_name}},
621 {});
622
623 {
624 xmlt &data_f = edge.new_element("data");
625 data_f.set_attribute("key", "originfile");
626 data_f.data = id2string(graphml[from].file);
627
628 xmlt &data_l = edge.new_element("data");
629 data_l.set_attribute("key", "startline");
630 data_l.data = id2string(graphml[from].line);
631 }
632
633 if(
634 (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
635 it->ssa_full_lhs.is_not_nil())
636 {
637 irep_idt identifier = it->ssa_lhs.get_object_name();
638
639 graphml[to].has_invariant = true;
640 code_assignt assign(it->ssa_lhs, it->ssa_rhs);
641 graphml[to].invariant = convert_assign_rec(identifier, assign);
642 graphml[to].invariant_scope = id2string(it->source.function_id);
643 }
644
645 graphml[to].in[from].xml_node = edge;
646 graphml[from].out[to].xml_node = edge;
647
648 break;
649 }
650
666 // ignore
667 break;
668 }
669
670 it=next;
671 step_nr=next_step_nr;
672 }
673}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet c_index_type()
Definition c_types.cpp:16
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition std_expr.h:1681
Arrays with given size.
Definition std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
A goto_instruction_codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
unsigned get_no() const
Definition dstring.h:182
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
Trace of a GOTO program.
Definition goto_trace.h:177
const namespacet & ns
void operator()(const goto_tracet &goto_trace)
counterexample witness
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
void remove_l0_l1(exprt &expr)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
key_valuest key_values
Definition graphml.h:67
nodet::node_indext node_indext
Definition graph.h:173
const edgest & out(node_indext n) const
Definition graph.h:227
node_indext add_node(arguments &&... values)
Definition graph.h:180
const edgest & in(node_indext n) const
Definition graph.h:222
Array index operator.
Definition std_expr.h:1470
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Extract member of struct or union.
Definition std_expr.h:2972
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const dt & read() const
Definition irep.h:240
const irep_idt & get_function() const
const irep_idt & get_file() const
const irep_idt & get_line() const
static bool is_built_in(const std::string &s)
std::vector< componentt > componentst
Definition std_types.h:140
Symbol table entry.
Definition symbol.h:28
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
The type of an expression, extends irept.
Definition type.h:29
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
Definition xml.h:21
xmlt & new_element(const std::string &key)
Definition xml.h:95
void set_attribute(const std::string &attribute, unsigned value)
Definition xml.cpp:198
std::string data
Definition xml.h:39
static bool is_printable_xml(const std::string &s)
Determine whether s does not contain any characters that cannot be escaped in XML 1....
Definition xml.cpp:160
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4190
#define Forall_operands(it, expr)
Definition expr.h:27
Concrete Goto Program.
Traces of GOTO Programs.
static std::string expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
Witnesses for Traces and Proofs.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
const std::string thread_id
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier)
Get the mode of the given identifier's symbol.
Definition mode.cpp:66
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition std_expr.h:1716
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2661
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
const string_constantt & to_string_constant(const exprt &expr)
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition expr2c.h:52
Functor to check whether iterators from different collections point at the same object.
Symbol table entry.
Generate Equation using Symbolic Execution.