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 #include <ostream>
18 #include <cassert>
19 
20 #include <util/arith_tools.h>
22 #include <util/numbering.h>
23 
24 std::string as_vcd_binary(
25  const exprt &expr,
26  const namespacet &ns)
27 {
28  const typet &type=ns.follow(expr.type());
29 
30  if(expr.id()==ID_constant)
31  {
32  if(type.id()==ID_unsignedbv ||
33  type.id()==ID_signedbv ||
34  type.id()==ID_bv ||
35  type.id()==ID_fixedbv ||
36  type.id()==ID_floatbv ||
37  type.id()==ID_pointer)
38  return expr.get_string(ID_value);
39  }
40  else if(expr.id()==ID_array)
41  {
42  std::string result;
43 
44  forall_operands(it, expr)
45  result+=as_vcd_binary(*it, ns);
46 
47  return result;
48  }
49  else if(expr.id()==ID_struct)
50  {
51  std::string result;
52 
53  forall_operands(it, expr)
54  result+=as_vcd_binary(*it, ns);
55 
56  return result;
57  }
58  else if(expr.id()==ID_union)
59  {
60  assert(expr.operands().size()==1);
61  return as_vcd_binary(expr.op0(), ns);
62  }
63 
64  // build "xxx"
65 
66  mp_integer width;
67 
68  if(type.id()==ID_unsignedbv ||
69  type.id()==ID_signedbv ||
70  type.id()==ID_floatbv ||
71  type.id()==ID_fixedbv ||
72  type.id()==ID_pointer ||
73  type.id()==ID_bv)
74  width=string2integer(type.get_string(ID_width));
75  else
76  width=pointer_offset_size(type, ns)*8;
77 
78  if(width>=0)
79  return std::string(integer2size_t(width), 'x');
80 
81  return "";
82 }
83 
85  const namespacet &ns,
86  const goto_tracet &goto_trace,
87  std::ostream &out)
88 {
89  time_t t;
90  time(&t);
91  out << "$date\n " << ctime(&t) << "$end" << "\n";
92 
93  // this is pretty arbitrary
94  out << "$timescale 1 ns $end" << "\n";
95 
96  // we first collect all variables that are assigned
97 
99 
100  for(const auto &step : goto_trace.steps)
101  {
102  if(step.is_assignment())
103  {
104  irep_idt identifier=step.lhs_object.get_identifier();
105  const typet &type=step.lhs_object.type();
106 
107  const auto number=n.number(identifier);
108 
109  mp_integer width;
110 
111  if(type.id()==ID_bool)
112  width=1;
113  else
114  width=pointer_offset_bits(type, ns);
115 
116  if(width>=1)
117  out << "$var reg " << width << " V" << number << " "
118  << identifier << " $end" << "\n";
119  }
120  }
121 
122  // end of header
123  out << "$enddefinitions $end" << "\n";
124 
125  unsigned timestamp=0;
126 
127  for(const auto &step : goto_trace.steps)
128  {
129  switch(step.type)
130  {
132  {
133  irep_idt identifier=step.lhs_object.get_identifier();
134  const typet &type=step.lhs_object.type();
135 
136  out << '#' << timestamp << "\n";
137  timestamp++;
138 
139  const auto number=n.number(identifier);
140 
141  // booleans are special in VCD
142  if(type.id()==ID_bool)
143  {
144  if(step.lhs_object_value.is_true())
145  out << "1" << "V" << number << "\n";
146  else if(step.lhs_object_value.is_false())
147  out << "0" << "V" << number << "\n";
148  else
149  out << "x" << "V" << number << "\n";
150  }
151  else
152  {
153  std::string binary=as_vcd_binary(step.lhs_object_value, ns);
154 
155  if(binary!="")
156  out << "b" << binary << " V" << number << " " << "\n";
157  }
158  }
159  break;
160 
161  default:
162  {
163  }
164  }
165  }
166 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
std::string as_vcd_binary(const exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: mp_arith.h:19
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
exprt & op0()
Definition: expr.h:84
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:60
stepst steps
Definition: goto_trace.h:150
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Traces of GOTO Programs in VCD (Value Change Dump) Format.
const irep_idt & id() const
Definition: irep.h:189
TO_BE_DOCUMENTED.
Definition: namespace.h:62
#define forall_operands(it, expr)
Definition: expr.h:17
void output_vcd(const namespacet &ns, const goto_tracet &goto_trace, std::ostream &out)
Pointer Logic.
Base class for all expressions.
Definition: expr.h:46
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
number_type number(const T &a)
Definition: numbering.h:27
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
operandst & operands()
Definition: expr.h:70