edmcman

===================================================================
--- gentrace.cpp	(revision 6904)
+++ gentrace.cpp	(working copy)
@@ -478,6 +478,17 @@
         return 32;
         break;
 
+    case REG_MM0:
+    case REG_MM1:
+    case REG_MM2:

edmcman

===================================================================
--- libasmir/src/traces/pin_taint.cpp	(revision 6904)
+++ libasmir/src/traces/pin_taint.cpp	(working copy)
@@ -779,16 +779,19 @@
         if (bytes == STATUS_SUCCESS) {
           WINDOWS::PIO_STATUS_BLOCK psb = reinterpret_cast<WINDOWS::PIO_STATUS_BLOCK> (args[4]);
           assert(psb);
-          assert(psb->Information);
-          length = psb->Information;
-          addr = args[5];

edmcman

Index: utils/iltrans.ml
===================================================================
--- utils/iltrans.ml	(revision 7125)
+++ utils/iltrans.ml	(working copy)
@@ -103,6 +103,15 @@
 let ast_coalesce = Coalesce.coalesce_ast
 let ssa_coalesce = Coalesce.coalesce_ssa
 
+let vsa_print g =
+  let g = Hacks.ssa_remove_indirect g in

edmcman

(** Value-Set Analysis / Value-Set Arithmetic

    See Gogul Balakrishnan's thesis at
    http://pages.cs.wisc.edu/~bgogul/Research/Thesis/thesis.html

    TODO:
    * Alternate memstore implementation
    * Add a real interface; automatically call simplify_cond
    * Big int support
    * Idea: Use copy propagation information to maintain equivalence

edmcman

#!/bin/bash
# Build Klee on Ubuntu 12.04 LTS

set -e
set -x
 
sudo apt-get -y install g++ curl dejagnu subversion bison flex
test -e /usr/lib/i686-pc-linux-gnu/4.2.1 || sudo ln -s /usr/lib/i386-linux-gnu /usr/lib/i686-pc-linux-gnu/4.2.1
rm -rf work
mkdir work

edmcman

match x with
| 1 ->
  (match y with
  | 1 -> Foo
  | 2 -> Bar)
| 2 ->

match x with
| 1 ->
  (match y with

edmcman

--- Makefile.in (revision 7331)
+++ Makefile.in (revision 7332)
@@ -143,7 +143,7 @@
 export OCAMLMKLIB_FLAGS = $(LDFLAGS)
 export PPFLAGS = $(SOLVER_PPFLAGS) @LLVM_PPFLAGS@
 export INCDIRS = $(BIGINT) $(BATT) $(OUNIT) $(PCRE) $(OCAMLGRAPH) $(OBJSIZE) $(LIBTRACE) $(LIBTRACE)/piqi
-export LIBS =
+export LIBS = zarith batteries objsize oUnit graph pcre libtrace
 export RESULTDEPS = $(LIBASMIR)/src/libasmir.a $(VEX_DIR)/libvex.a $(LIBTRACE)/libtrace.cmxa
 export LIBDIRS = $(LIBASMIR)/src $(VEX_DIR)

edmcman

message program {
    repeated stmt elem = 1;
}

message stmt {
    optional move move = 1;
    optional jmp jmp = 2;
    optional cjmp cjmp = 3;
    optional label_stmt label_stmt = 4;

edmcman

Index: ocaml/llvm_codegen.ml
===================================================================
--- ocaml/llvm_codegen.ml	(revision 7607)
+++ ocaml/llvm_codegen.ml	(revision 7608)
@@ -25,7 +25,7 @@
   vars: llvalue VH.t;
   letvars: llvalue VH.t;
   mutable allocbb: llbasicblock option
-           }
+}

edmcman

Index: ocaml/cfg_ast.ml
===================================================================
--- ocaml/cfg_ast.ml	(revision 7629)
+++ ocaml/cfg_ast.ml	(working copy)
@@ -13,7 +13,7 @@
 module C = Cfg.AST
 
 
-module D = Debug.Make(struct let name = "CFG_AST" and default=`NoDebug end)
+module D = Debug.Make(struct let name = "Cfg_ast" and default=`NoDebug end)