cprover
vcd_goto_trace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Traces of GOTO Programs in VCD (Value Change Dump) Format
4 
5 Author: Daniel Kroening
6 
7 Date: June 2011
8 
9 \*******************************************************************/
10 
13 
14 #include "vcd_goto_trace.h"
15 
16 #include <ctime>
17 
18 #include <util/arith_tools.h>
19 #include <util/numbering.h>
21 
22 std::string as_vcd_binary(
23  const exprt &expr,
24  const namespacet &ns)
25 {
26  const typet &type=ns.follow(expr.type());
27 
28  if(expr.id()==ID_constant)
29  {
30  if(type.id()==ID_unsignedbv ||
31  type.id()==ID_signedbv ||
32  type.id()==ID_bv ||
33  type.id()==ID_fixedbv ||
34  type.id()==ID_floatbv ||
35  type.id()==ID_pointer)
36  return expr.get_string(ID_value);
37  }
38  else if(expr.id()==ID_array)
39  {
40  std::string result;
41 
42  forall_operands(it, expr)
43  result+=as_vcd_binary(*it, ns);
44 
45  return result;
46  }
47  else if(expr.id()==ID_struct)
48  {
49  std::string result;
50 
51  forall_operands(it, expr)
52  result+=as_vcd_binary(*it, ns);
53 
54  return result;
55  }
56  else if(expr.id()==ID_union)
57  {
58  return as_vcd_binary(to_union_expr(expr).op(), ns);
59  }
60 
61  // build "xxx"
62 
63  const auto width = pointer_offset_bits(type, ns);
64 
65  if(width.has_value())
66  return std::string(numeric_cast_v<std::size_t>(*width), 'x');
67  else
68  return "";
69 }
70 
72  const namespacet &ns,
73  const goto_tracet &goto_trace,
74  std::ostream &out)
75 {
76  time_t t;
77  time(&t);
78  out << "$date\n " << ctime(&t) << "$end" << "\n";
79 
80  // this is pretty arbitrary
81  out << "$timescale 1 ns $end" << "\n";
82 
83  // we first collect all variables that are assigned
84 
86 
87  for(const auto &step : goto_trace.steps)
88  {
89  if(step.is_assignment())
90  {
91  auto lhs_object=step.get_lhs_object();
92  if(lhs_object.has_value())
93  {
94  irep_idt identifier=lhs_object->get_identifier();
95  const typet &type=lhs_object->type();
96 
97  const auto number=n.number(identifier);
98 
99  const auto width = pointer_offset_bits(type, ns);
100 
101  if(width.has_value() && (*width) >= 1)
102  out << "$var reg " << (*width) << " V" << number << " " << identifier
103  << " $end"
104  << "\n";
105  }
106  }
107  }
108 
109  // end of header
110  out << "$enddefinitions $end" << "\n";
111 
112  unsigned timestamp=0;
113 
114  for(const auto &step : goto_trace.steps)
115  {
116  switch(step.type)
117  {
119  {
120  auto lhs_object=step.get_lhs_object();
121  if(lhs_object.has_value())
122  {
123  irep_idt identifier=lhs_object->get_identifier();
124  const typet &type=lhs_object->type();
125 
126  out << '#' << timestamp << "\n";
127  timestamp++;
128 
129  const auto number=n.number(identifier);
130 
131  // booleans are special in VCD
132  if(type.id()==ID_bool)
133  {
134  if(step.full_lhs_value.is_true())
135  out << "1" << "V" << number << "\n";
136  else if(step.full_lhs_value.is_false())
137  out << "0" << "V" << number << "\n";
138  else
139  out << "x" << "V" << number << "\n";
140  }
141  else
142  {
143  std::string binary=as_vcd_binary(step.full_lhs_value, ns);
144 
145  if(binary!="")
146  out << "b" << binary << " V" << number << " " << "\n";
147  }
148  }
149  }
150  break;
151 
152  default:
153  {
154  }
155  }
156  }
157 }
The type of an expression, extends irept.
Definition: type.h:27
std::string as_vcd_binary(const exprt &expr, const namespacet &ns)
number_type number(const key_type &a)
Definition: numbering.h:37
typet & type()
Return the type of the expression.
Definition: expr.h:68
stepst steps
Definition: goto_trace.h:154
Traces of GOTO Programs in VCD (Value Change Dump) Format.
const irep_idt & id() const
Definition: irep.h:259
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define forall_operands(it, expr)
Definition: expr.h:20
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
void output_vcd(const namespacet &ns, const goto_tracet &goto_trace, std::ostream &out)
Pointer Logic.
Base class for all expressions.
Definition: expr.h:54
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1890
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:224
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)