vcd

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@117 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/goto-symex/Makefile

@@ -4,7 +4,7 @@ SRC = symex_target.cpp symex_target_equation.cpp basic_symex.cpp \
       symex_goto.cpp builtin_functions.cpp slice.cpp symex_other.cpp \
       slice_by_trace.cpp xml_goto_trace.cpp symex_decl.cpp \
       precondition.cpp postcondition.cpp symex_clean_expr.cpp \
-      symex_dereference_state.cpp
+      symex_dereference_state.cpp vcd_goto_trace.cpp
 
 OBJ = $(SRC:.cpp=$(OBJEXT))
 

src/goto-symex/vcd_goto_trace.cpp

@@ -0,0 +1,207 @@
+/*******************************************************************\
+
+Module: Traces of GOTO Programs in VCD (Value Change Dump) Format
+
+Author: Daniel Kroening
+
+Date: June 2011
+
+\*******************************************************************/
+
+#include <time.h>
+#include <assert.h>
+
+#include <arith_tools.h>
+#include <pointer_offset_size.h>
+
+#include <numbering.h>
+
+#include "vcd_goto_trace.h"
+
+/*******************************************************************\
+
+Function: output_vcd
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string as_vcd_binary(
+  const exprt &expr,
+  const namespacet &ns)
+{
+  const typet &type=ns.follow(expr.type());
+  
+  if(expr.id()==ID_constant)
+  {
+    if(type.id()==ID_unsignedbv ||
+       type.id()==ID_signedbv ||
+       type.id()==ID_bv ||
+       type.id()==ID_fixedbv ||
+       type.id()==ID_floatbv ||
+       type.id()==ID_pointer)
+      return expr.get_string(ID_value);
+  }
+  else if(expr.id()==ID_array)
+  {
+    std::string result;
+
+    forall_operands(it, expr)
+      result+=as_vcd_binary(*it, ns);
+    
+    return result;
+  }
+  else if(expr.id()==ID_struct)
+  {
+    std::string result;
+
+    forall_operands(it, expr)
+      result+=as_vcd_binary(*it, ns);
+    
+    return result;
+  }
+  else if(expr.id()==ID_union)
+  { 
+    assert(expr.operands().size()==1);
+    return as_vcd_binary(expr.op0(), ns);
+  }
+  
+  // build "xxx"
+
+  mp_integer width;
+
+  if(type.id()==ID_unsignedbv ||
+     type.id()==ID_signedbv ||
+     type.id()==ID_floatbv ||
+     type.id()==ID_fixedbv ||
+     type.id()==ID_pointer ||
+     type.id()==ID_bv)
+    width=string2integer(type.get_string(ID_width));
+  else
+    width=pointer_offset_size(ns, type)*8;
+
+  if(width>=0)
+  {
+    std::string result;
+
+    for(; width!=0; --width)
+      result+='x';
+
+    return result;
+  }
+  
+  return "";
+}
+
+/*******************************************************************\
+
+Function: output_vcd
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void output_vcd(
+  const namespacet &ns,
+  const goto_tracet &goto_trace,
+  std::ostream &out)
+{
+  time_t t;
+  time(&t);
+  out << "$date\n  " << ctime(&t) << "$end" << std::endl;
+  
+  // this is pretty arbitrary
+  out << "$timescale 1 ns $end" << std::endl;
+
+  // we first collect all variables that are assigned
+  
+  numbering<irep_idt> n;
+
+  for(goto_tracet::stepst::const_iterator
+      it=goto_trace.steps.begin();
+      it!=goto_trace.steps.end();
+      it++)
+  {
+    if(it->is_assignment())
+    {
+      exprt lhs=it->original_lhs.is_not_nil()?it->original_lhs:it->lhs;
+      irep_idt identifier=lhs.get(ID_identifier);
+      const typet &type=lhs.type();
+        
+      unsigned number=n.number(identifier);
+
+      mp_integer width;
+
+      if(type.id()==ID_bool)
+        width=1;
+      else if(type.id()==ID_unsignedbv ||
+              type.id()==ID_signedbv ||
+              type.id()==ID_floatbv ||
+              type.id()==ID_fixedbv ||
+              type.id()==ID_pointer ||
+              type.id()==ID_bv)
+        width=string2integer(type.get_string(ID_width));
+      else
+        width=pointer_offset_size(ns, lhs.type())*8;
+        
+      if(width>=1)
+        out << "$var reg " << width << " V" << number << " "
+            << identifier << " $end" << std::endl;
+    }
+  }  
+
+  // end of header
+  out << "$enddefinitions $end" << std::endl;
+
+  unsigned timestamp=0;
+
+  for(goto_tracet::stepst::const_iterator
+      it=goto_trace.steps.begin();
+      it!=goto_trace.steps.end();
+      it++)
+  {
+    switch(it->type)
+    {
+    case goto_trace_stept::ASSIGNMENT:
+      {
+        exprt lhs=it->original_lhs.is_not_nil()?it->original_lhs:it->lhs;
+        irep_idt identifier=lhs.get(ID_identifier);
+        const typet &type=lhs.type();
+
+        out << '#' << timestamp << std::endl;
+        timestamp++;
+
+        unsigned number=n.number(identifier);
+        
+        // booleans are special in VCD
+        if(type.id()==ID_bool)
+        {
+          if(it->value.is_true())
+            out << "1" << "V" << number << std::endl;
+          else if(it->value.is_false())
+            out << "0" << "V" << number << std::endl;
+          else
+            out << "x" << "V" << number << std::endl;
+        }
+        else
+        {
+          std::string binary=as_vcd_binary(it->value, ns);
+
+          if(binary!="")
+            out << "b" << binary << " V" << number << " " << std::endl;
+        }
+      }
+      break;
+      
+    default:;
+    }
+  }
+}

src/goto-symex/vcd_goto_trace.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Traces of GOTO Programs in VCD (Value Change Dump) Format
+
+Author: Daniel Kroening
+
+Date: June 2011
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_SYMEX_VCD_GOTO_TRACE_H
+#define CPROVER_GOTO_SYMEX_VCD_GOTO_TRACE_H
+
+#include <iostream>
+
+#include <namespace.h>
+
+#include "goto_trace.h"
+
+void output_vcd(
+  const namespacet &ns,
+  const goto_tracet &goto_trace,
+  std::ostream &out);
+
+#endif