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 = 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  if(step.is_assignment())
117  {
118  auto lhs_object = step.get_lhs_object();
119  if(lhs_object.has_value())
120  {
121  irep_idt identifier = lhs_object->get_identifier();
122  const typet &type = lhs_object->type();
123 
124  out << '#' << timestamp << "\n";
125  timestamp++;
126 
127  const auto number = n.number(identifier);
128 
129  // booleans are special in VCD
130  if(type.id() == ID_bool)
131  {
132  if(step.full_lhs_value.is_true())
133  out << "1"
134  << "V" << number << "\n";
135  else if(step.full_lhs_value.is_false())
136  out << "0"
137  << "V" << number << "\n";
138  else
139  out << "x"
140  << "V" << number << "\n";
141  }
142  else
143  {
144  std::string binary = as_vcd_binary(step.full_lhs_value, ns);
145 
146  if(!binary.empty())
147  out << "b" << binary << " V" << number << " "
148  << "\n";
149  }
150  }
151  }
152  }
153 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:29
template_numberingt
Definition: numbering.h:22
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
exprt
Base class for all expressions.
Definition: expr.h:53
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1613
as_vcd_binary
std::string as_vcd_binary(const exprt &expr, const namespacet &ns)
Definition: vcd_goto_trace.cpp:22
vcd_goto_trace.h
Traces of GOTO Programs in VCD (Value Change Dump) Format.
template_numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
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
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
irept::id
const irep_idt & id() const
Definition: irep.h:418
numbering.h
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:431
output_vcd
void output_vcd(const namespacet &ns, const goto_tracet &goto_trace, std::ostream &out)
Definition: vcd_goto_trace.cpp:71
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:204
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171