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 <cassert>
17 #include <ctime>
18 
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  assert(expr.operands().size()==1);
59  return as_vcd_binary(expr.op0(), ns);
60  }
61 
62  // build "xxx"
63 
64  const mp_integer width = pointer_offset_bits(type, ns);
65 
66  if(width>=0)
67  return std::string(integer2size_t(width), 'x');
68 
69  return "";
70 }
71 
73  const namespacet &ns,
74  const goto_tracet &goto_trace,
75  std::ostream &out)
76 {
77  time_t t;
78  time(&t);
79  out << "$date\n " << ctime(&t) << "$end" << "\n";
80 
81  // this is pretty arbitrary
82  out << "$timescale 1 ns $end" << "\n";
83 
84  // we first collect all variables that are assigned
85 
87 
88  for(const auto &step : goto_trace.steps)
89  {
90  if(step.is_assignment())
91  {
92  irep_idt identifier=step.lhs_object.get_identifier();
93  const typet &type=step.lhs_object.type();
94 
95  const auto number=n.number(identifier);
96 
97  const mp_integer width = pointer_offset_bits(type, ns);
98 
99  if(width>=1)
100  out << "$var reg " << width << " V" << number << " "
101  << identifier << " $end" << "\n";
102  }
103  }
104 
105  // end of header
106  out << "$enddefinitions $end" << "\n";
107 
108  unsigned timestamp=0;
109 
110  for(const auto &step : goto_trace.steps)
111  {
112  switch(step.type)
113  {
115  {
116  irep_idt identifier=step.lhs_object.get_identifier();
117  const typet &type=step.lhs_object.type();
118 
119  out << '#' << timestamp << "\n";
120  timestamp++;
121 
122  const auto number=n.number(identifier);
123 
124  // booleans are special in VCD
125  if(type.id()==ID_bool)
126  {
127  if(step.lhs_object_value.is_true())
128  out << "1" << "V" << number << "\n";
129  else if(step.lhs_object_value.is_false())
130  out << "0" << "V" << number << "\n";
131  else
132  out << "x" << "V" << number << "\n";
133  }
134  else
135  {
136  std::string binary=as_vcd_binary(step.lhs_object_value, ns);
137 
138  if(binary!="")
139  out << "b" << binary << " V" << number << " " << "\n";
140  }
141  }
142  break;
143 
144  default:
145  {
146  }
147  }
148  }
149 }
The type of an expression.
Definition: type.h:22
std::string as_vcd_binary(const exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: mp_arith.h:22
number_type number(const key_type &a)
Definition: numbering.h:37
exprt & op0()
Definition: expr.h:72
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
stepst steps
Definition: goto_trace.h:156
Traces of GOTO Programs in VCD (Value Change Dump) Format.
const irep_idt & id() const
Definition: irep.h:259
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define forall_operands(it, expr)
Definition: expr.h:17
const typet & follow(const typet &) const
Definition: namespace.cpp:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void output_vcd(const namespacet &ns, const goto_tracet &goto_trace, std::ostream &out)
Pointer Logic.
Base class for all expressions.
Definition: expr.h:42
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
operandst & operands()
Definition: expr.h:66