Commits

Zachary Anderson committed cdfe7bf

Added automated test generation example

  • Participants
  • Parent commits cdebbac

Comments (0)

Files changed (21)

   BUILD_TUT11 = @BUILD_TUT11@
 endif
 
+ifndef BUILD_TUT15
+	BUILD_TUT15 = @BUILD_TUT15@
+endif
+
 prefix = @prefix@
 exec_prefix = @exec_prefix@
 libdir = @libdir@
 # Add additional modules here. Order matters. If module x depends on module y,
 # then x has to come after y in the list.
 MODULES = tututil ciltutoptions \
-          tut0 tut1 tut2 tut3 tut4 tut5 tut6 tut7 tut8 tut9 tut10 tut11 tut12 tut13 tut14 main
+          tut0 tut1 tut2 tut3 tut4 tut5 tut6 tut7 tut8 tut9 tut10 tut11 tut12 tut13 tut14 tut15 main
 
 OCAMLFIND = @OCAMLFIND@
 CILINC = $(shell $(OCAMLFIND) query cil)
   LINKFLAGS += -I +why3
   PREPROC_ARG = -DBUILD_TUT11
 endif
+
+ifeq ($(BUILD_TUT15),true)
+	PREPROC_ARG += -DBUILD_TUT15
+endif
+
 PREPROC = camlp4o pa_macro.cmo $(PREPROC_ARG)
 
 include Makefile.ocaml
 . theorem provers (e.g. alt-ergo)
 . pass --disable-tut11 to the configure script to disable tut11
 
+Dependencies only for the automated test generation example (tut15.ml):
+. Yices SMT solver (http://yices.csl.sri.com/)
+. ocamlyices (https://github.com/polazarus/ocamlyices)
+
 After obtaining the code, enter the directory and do the following:
 
 $ ./configure

ciltut-include/ciltut.h

 
 #define arg_assert(e) (void *__attribute__((ciltut_assert((e)))))0
 
+
+#define autotest    __attribute__((autotest))
+#define instrument  __attribute__((instrument))
+#define input       __attribute__((input))
+#define inputarr(s) __attribute__((inputarr(s)))
+#define inputnt     __attribute__((inputnt))
+
+void assign(uint64_t lhs, uint64_t op, int opk, uint64_t opv);
+void assgn_bop(uint64_t lhs, uint64_t lhsv, int bop,
+               uint64_t op1, int op1k, uint64_t op1v,
+               uint64_t op2, int op2k, uint64_t op2v);
+void assgn_uop(uint64_t lhs, uint64_t lhsv, int uop,
+               uint64_t op, int opk, uint64_t opv);
+
+void cond(int cid, int r, uint64_t op, int opk, uint64_t opv);
+void cond_bop(int cid, int bop, int r,
+              uint64_t op1, int op1k, uint64_t op1v,
+              uint64_t op2, int op2k, uint64_t op2v);
+void cond_uop(int cid, int uop, int r,
+              uint64_t op, int opk, uint64_t opv);
+
+void register_input(char *name, uint64_t addr, int bits);
+void register_arr_input(char *name, uint64_t start, int sz, int cnt);
+void register_nt_input(char *name, char *start);
+
+#pragma cilnoremove("autotest_finished")
+extern int autotest_finished;
+void gen_new_input();
+
+void val_push(uint64_t v);
+uint64_t val_pop(char *name);
+void pop_array(char *name, char *base, int cnt, int sz);
+void pop_nt(char * name, char *base);
+
+void return_push(uint64_t p, uint64_t v);
+void return_pop(uint64_t p, uint64_t v);
+
+void autotest_reset();
+
 #endif 
 
 

ciltut-lib/CMakeLists.txt

 
 include_directories("${PROJECT_BINARY_DIR}/../ciltut-include")
 link_directories("${PROJECT_BINARY_DIR}/src")
+link_directories("${PROJECT_BINARY_DIR}/src/concolic")
 
 add_subdirectory(src)
 

ciltut-lib/Makefile.dummy.in

 	rm -rf `find . -name CMakeFiles`
 	rm -rf `find . -name CMakeCache.txt`
 	rm -rf `find . -name cmake_install.cmake`
+	rm -rf `find . -name \*.cmi`
+	rm -rf `find . -name \*.cmo`
 
 distclean: clean
 

ciltut-lib/src/CMakeLists.txt

 	"${PROJECT_BINARY_DIR}/src/config.h"
 )
 
-set(SHELTER_SRCS ciltut_libc.c tut4.c tut8.c tut6.c tut10.c)
+set(OCAML_COMPILE ocamlc)
 
-add_library(ciltut-static ${SHELTER_SRCS})
+execute_process(
+  COMMAND ocamlfind query ocamlyices
+  OUTPUT_VARIABLE OCAML_YICES OUTPUT_STRIP_TRAILING_WHITESPACE
+)
+
+set(CONC_SRCS
+ concolic/concolic_util.ml
+ concolic/concolic_exp.ml
+ concolic/concolic_ctxt.ml
+ concolic/concolic_paths.ml
+ concolic/concolic_callbacks.ml)
+
+add_custom_target(concolic_callbacks ${CONC_SRCS})
+add_custom_command(
+  SOURCE  ${CONC_SRCS}
+  COMMAND ${OCAML_COMPILE}
+  ARGS    -custom -output-obj -o concolic_callbacks.o -I concolic/ -I ${OCAML_YICES} -I +gmp gmp.cma nums.cma ocamlyices.cma ${CONC_SRCS}
+  TARGET  concolic_callbacks
+  OUTPUTS concolic_callbacks.o
+  DEPENDS ${CONC_SRCS}
+)
+add_custom_command(
+  SOURCE  concolic_callbacks
+  TARGET  concolic_callbacks
+  DEPENDS concolic_callbacks.o
+)
+
+set(SHELTER_SRCS ciltut_libc.c tut4.c tut8.c tut6.c tut10.c tut15.c)
+
+add_library(ciltut-static ${SHELTER_SRCS} concolic_callbacks.o)
 set_target_properties(ciltut-static PROPERTIES
   COMPILE_FLAGS "-O2 -ggdb"
 )
   PROPERTIES OUTPUT_NAME ciltut
   CLEAN_DIRECT_OUTPUT 1)
 
-add_library(ciltut-shared SHARED ${SHELTER_SRCS})
+add_library(ciltut-shared SHARED ${SHELTER_SRCS} concolic_callbacks.o)
 set_target_properties(ciltut-shared PROPERTIES
   COMPILE_FLAGS "-O2 -ggdb"
 )

ciltut-lib/src/concolic/concolic_callbacks.ml

+open Concolic_util
+
+module C = Concolic_ctxt
+module E = Concolic_exp
+module P = Concolic_paths
+
+module Y = Yices
+module L = List
+module A = Array
+module H = Hashtbl
+module S = String
+
+let assign (lhs : int64) (op : int64) (opk : int) (opv : int64) : unit =
+	C.addState lhs (E.mkOpExp op opk opv)
+
+let assgn_bop (lhs : int64) (lhsv : int64) (bop : int)
+              (op1 : int64) (op1k : int) (op1v : int64)
+              (op2 : int64) (op2k : int) (op2v : int64)
+              : unit =
+	let e1 = E.mkOpExp op1 op1k op1v in
+	let e2 = E.mkOpExp op2 op2k op2v in
+	C.addState lhs (E.BinOp(lhsv, E.bop_of_int bop, e1, e2))
+
+let assgn_uop (lhs : int64) (lhsv : int64) (uop : int)
+              (op : int64) (opk : int) (opv : int64)
+              : unit =
+	let e = E.UnOp(lhsv, E.uop_of_int uop, E.mkOpExp op opk opv) in
+	C.addState lhs e
+
+let cond (cid : int) (r : int) (op : int64) (opk : int) (opv : int64) : unit =
+	let op =
+		if r = 1 then E.mkOpExp op opk opv |> C.simplifyExp
+		else E.UnOp(Int64.one, E.LNot, E.mkOpExp op opk opv |> C.simplifyExp)
+	in
+	P.addPathCond cid r op
+
+let cond_bop (cid : int) (bop : int) (r : int)
+             (op1 : int64) (op1k : int) (op1v : int64)
+             (op2 : int64) (op2k : int) (op2v : int64)
+             : unit =
+	let bop =
+		if r = 1 then E.bop_of_int bop
+		else bop |> E.bop_of_int |> E.opposite_test
+	in
+	let e1 = E.mkOpExp op1 op1k op1v |> C.simplifyExp in
+	let e2 = E.mkOpExp op2 op2k op2v |> C.simplifyExp in
+	let c = E.BinOp(Int64.of_int r, bop, e1, e2) in
+	P.addPathCond cid r c
+
+let cond_uop (cid : int) (uop : int) (r : int)
+             (op : int64) (opk : int) (opv : int64)
+             : unit =
+	let e = E.mkOpExp op opk opv |> C.simplifyExp in
+	let c = E.UnOp(Int64.of_int r, E.uop_of_int uop, e) in
+	if r = 1 then P.addPathCond cid r c
+	else P.addPathCond cid r (E.UnOp(Int64.one, E.LNot, c))
+
+let push_val (n : string) (v : int64) : unit = C.storeVal n v
+let pop_val (n : string) : int64 = C.getVal n
+
+let register_input (name : string) (addr : int64) (bits : int) : unit =
+	C.makeNewInput name addr bits
+
+let gen_new_input () : int = P.pathsFindNext ()
+
+let retval : E.exp ref = ref (E.Op(Int64.zero,(E.Address, Int64.zero)))
+
+let return_push (p : int64) (v : int64) : unit =
+	retval := (E.Op(v, (E.Address, p)))
+let return_pop  (p : int64) (v : int64) : unit =
+	match !retval with
+	| E.Op(v', (E.Address, v'')) when v' = Int64.zero && v'' = Int64.zero ->
+		C.addState p (E.Op(v,(E.Constant, v)))
+	| e -> C.addState p e; retval := (E.Op(Int64.zero,(E.Address, Int64.zero)))
+
+let autotest_reset() : unit =
+	C.resetContext ();
+	P.resetPaths ()
+
+let _ =
+	C.global_ctxt := Some (C.makeContext ());
+	Printf.printf "Yices version = %s\n" (Y.version ());
+	flush stdout;
+	Callback.register "assign"         assign;
+	Callback.register "assgn_bop"      assgn_bop;
+	Callback.register "assgn_uop"      assgn_uop;
+	Callback.register "cond"           cond;
+	Callback.register "cond_bop"       cond_bop;
+	Callback.register "cond_uop"       cond_uop;
+	Callback.register "register_input" register_input;
+	Callback.register "gen_new_input"  gen_new_input;
+	Callback.register "push_val"       push_val;
+	Callback.register "pop_val"        pop_val;
+	Callback.register "return_push"    return_push;
+	Callback.register "return_pop"     return_pop;
+	Callback.register "autotest_reset" autotest_reset
+

ciltut-lib/src/concolic/concolic_ctxt.ml

+open Concolic_util
+
+module E = Concolic_exp
+module Y = Yices
+module H = Hashtbl
+
+type context = {
+	mutable yctx    : Y.context;
+	mutable inv     : Y.expr list;
+	mutable input   : (int64, string * Y.var_decl) H.t;
+	mutable modelHT : (string, int64) H.t;
+	mutable memory  : (int64, E.exp) H.t;
+}
+
+let global_ctxt : context option ref = ref None
+
+let makeContext () : context =
+	let ctx = Y.mk_context() in
+	{yctx    = ctx;
+	 inv     = [];
+	 input   = H.create 256;
+	 modelHT = H.create 256;
+	 memory  = H.create 256;}
+
+let resetContext () : unit =
+	let c = !global_ctxt |> forceOption in
+	Y.del_context c.yctx;
+	c.yctx   <- Y.mk_context();
+	c.inv    <- [];
+	H.clear c.input;
+	H.clear c.modelHT;
+	H.clear c.memory
+
+let makeVarDecl (c : context) (n : string) (t : Y.typ) : Y.var_decl =
+	try Y.get_var_decl_from_name c.yctx n
+	with Failure _ -> Y.mk_var_decl c.yctx n t
+
+let makeBVLimit (c : context) (bits : int) : Y.expr =
+	if bits < 64 then
+		let maxval = Array.make 64 false in
+		maxval.(bits) <- true;
+		Y.mk_bv_constant_from_array c.yctx maxval
+	else let maxval = Array.make 64 true in
+	Y.mk_bv_constant_from_array c.yctx maxval
+
+let makeBVZero (c : context) (bits : int) : Y.expr =
+	Y.mk_bv_constant c.yctx 64 Int32.zero
+
+let makeBVOne  (c : context) (bits : int) : Y.expr =
+	Y.mk_bv_constant c.yctx 64 Int32.one
+
+let makeNewInput (name : string) (addr : int64) (bits : int) : unit =
+	let c   = !global_ctxt |> forceOption in
+	let ul  = makeBVLimit c bits in
+	let t   = Y.mk_bv_type c.yctx 64 in
+	let vd  = makeVarDecl c name t in
+	let var = Y.mk_var_from_decl c.yctx vd in
+	H.replace c.input addr (name, vd);
+	c.inv <- (Y.mk_bv_lt c.yctx var ul) :: c.inv
+
+let getInput (c : context) (addr : int64) : Y.expr =
+	addr
+	|> H.find c.input
+	|> snd
+	|> Y.mk_var_from_decl c.yctx
+
+let getState (v : int64) (a : int64) : E.exp =
+	let c = !global_ctxt |> forceOption in
+	try H.find c.memory a
+	with Not_found ->
+		if H.mem c.input a then E.Input a
+		else E.Op(v, (E.Constant, v))
+
+let rec simplifyExp (e : E.exp) : E.exp =
+	match e with
+	| E.Op(v, (E.Constant, v')) -> e
+	| E.Op(v, (E.Address, a)) -> a |> getState v |> simplifyExp
+	| E.UnOp(v, u, e') -> begin
+		let e' = simplifyExp e' in
+		match e' with
+		| E.Op(v', (E.Constant, v'')) -> E.Op(v, (E.Constant, E.apply_uop u v'))
+		| _ -> E.UnOp(v, u, e')
+	end
+	| E.BinOp(v, b, e1, e2) -> begin
+		let e1' = simplifyExp e1 in
+		let e2' = simplifyExp e2 in
+		match e1', e2' with
+		| E.Op(v1, (E.Constant, v1')), E.Op(v2, (E.Constant, v2')) ->
+			E.Op(v, (E.Constant, E.apply_bop b v1 v2))
+		| _ -> E.BinOp(v, b, e1', e2')
+	end
+	| E.Input a -> E.Input a
+
+let addState (dest : int64) (e : E.exp) : unit =
+	let c = !global_ctxt |> forceOption in
+	H.replace c.memory dest (simplifyExp e)
+
+let ctxtStoreVal (c : context) (n : string) (v : int64) : unit =
+	let c = !global_ctxt |> forceOption in
+	H.replace c.modelHT n v
+
+let storeVal (n : string) (v : int64) : unit =
+	let c = !global_ctxt |> forceOption in
+	H.replace c.modelHT n v
+
+let getVal (n : string) : int64 =
+	let c = !global_ctxt |> forceOption in
+	try H.find c.modelHT n with Not_found -> Int64.zero
+
+let rec yices_of_exp (c : context) (e : E.exp) : Y.expr =
+	match e with
+	| E.Input a -> getInput c a
+	| E.UnOp(v, u, e) -> begin
+		let ye = yices_of_exp c e in
+		match u with
+		| E.Neg  -> Y.mk_bv_minus c.yctx ye
+		| E.BNot -> Y.mk_bv_not   c.yctx ye
+		| E.LNot -> Y.mk_ite c.yctx (Y.mk_eq c.yctx ye (makeBVZero c 64))
+			                          (makeBVOne c 64) (makeBVZero c 64)
+	end
+	| E.BinOp(v, b, e1, e2) -> begin
+		let ye1 = yices_of_exp c e1 in
+		let ye2 = yices_of_exp c e2 in
+		match b with
+		| E.Plus     -> Y.mk_bv_add c.yctx ye1 ye2
+		| E.Minus    -> Y.mk_bv_sub c.yctx ye1 ye2
+		| E.Times    -> Y.mk_bv_mul c.yctx ye1 ye2
+		| E.Div      -> Y.mk_bv_constant c.yctx 64 (int32_of_int64 v)
+		| E.Mod      -> Y.mk_bv_constant c.yctx 64 (int32_of_int64 v)
+		| E.Shiftl   -> Y.mk_bv_constant c.yctx 64 (int32_of_int64 v)
+		| E.Shiftrl  -> Y.mk_bv_constant c.yctx 64 (int32_of_int64 v)
+		| E.Shiftra  -> Y.mk_bv_constant c.yctx 64 (int32_of_int64 v)
+		| E.Lt       -> Y.mk_bv_slt c.yctx ye1 ye2
+		| E.Gt       -> Y.mk_bv_sgt c.yctx ye1 ye2
+		| E.Le       -> Y.mk_bv_sle c.yctx ye1 ye2
+		| E.Ge       -> Y.mk_bv_sge c.yctx ye1 ye2
+		| E.Eq       -> Y.mk_eq     c.yctx ye1 ye2
+		| E.Ne       -> Y.mk_diseq  c.yctx ye1 ye2
+		| E.BAnd     -> Y.mk_bv_and c.yctx ye1 ye2
+		| E.BXor     -> Y.mk_bv_xor c.yctx ye1 ye2
+		| E.BOr      -> Y.mk_bv_or  c.yctx ye1 ye2
+		| E.LAnd     -> Y.mk_and    c.yctx [|ye1; ye2|]
+		| E.LOr      -> Y.mk_or     c.yctx [|ye1; ye2|]
+	end
+	| E.Op(v, (E.Constant, _)) -> Y.mk_bv_constant c.yctx 64 (int32_of_int64 v)
+	| E.Op(v, (E.Address, _)) -> failwith "Bad exp in yices_of_exp"
+

ciltut-lib/src/concolic/concolic_exp.ml

+open Concolic_util
+
+module A = Array
+module L = List
+
+type opkind = Constant | Address
+
+let opkind_of_int (i : int) : opkind =
+	match i with
+	| 0 -> Constant
+	| 1 -> Address
+	| _ -> failwith "Bad opkind"
+
+let string_of_op (op : int64) (ok : opkind) : string =
+	match ok with
+	| Constant -> Int64.to_string op
+	| Address  -> "["^(Int64.to_string op)^"]"
+
+type bop =
+	| Plus | Minus | Times | Div | Mod
+	| Shiftl | Shiftrl | Shiftra
+	| Lt | Gt | Le | Ge | Eq | Ne
+	| BAnd | BXor | BOr
+	| LAnd | LOr
+
+let bop_table = [|
+	Plus; Minus; Times; Div; Mod;
+	Shiftl; Shiftrl; Shiftra;
+	Lt; Gt; Le; Ge; Eq; Ne;
+	BAnd; BXor; BOr;
+	LAnd; LOr;
+|]
+let bop_of_int (b : int) : bop = bop_table.(b)
+let int_of_bop (b : bop) : int = b |> array_mem bop_table |> L.hd
+
+let string_of_bop (b : bop) : string =
+	match b with
+	| Plus     -> "+"  | Minus    -> "-"   | Times    -> "*"
+	| Div      -> "/"  | Mod      -> "%"   | Shiftl   -> ">>"
+	| Shiftrl  -> ">>" | Shiftra  -> ">>>" | Lt       -> "<"
+	| Gt       -> ">"  | Le       -> "<="  | Ge       -> ">="
+	| Eq       -> "==" | Ne       -> "!="  | BAnd     -> "&"
+	| BXor     -> "^"  | BOr      -> "|"   | LAnd     -> "&&"
+	| LOr      -> "||"
+
+let apply_bop (b : bop) (o1 : int64) (o2 : int64) : int64 =
+	match b with
+	| Plus     -> Int64.add o1 o2
+	| Minus    -> Int64.sub o1 o2
+	| Times    -> Int64.mul o1 o2
+	| Div      -> Int64.div o1 o2
+	| Mod      -> Int64.rem o1 o2
+	| Shiftl   -> Int64.shift_left o1 (Int64.to_int o2)
+	| Shiftrl  -> Int64.shift_right_logical o1 (Int64.to_int o2)
+	| Shiftra  -> Int64.shift_right o1 (Int64.to_int o2)
+	| Lt       -> if o1 < o2  then Int64.one else Int64.zero
+	| Gt       -> if o1 > o2  then Int64.one else Int64.zero
+	| Le       -> if o1 <= o2 then Int64.one else Int64.zero
+	| Ge       -> if o1 >= o2 then Int64.one else Int64.zero
+	| Eq       -> if o1 = o2  then Int64.one else Int64.zero
+	| Ne       -> if o1 <> o2 then Int64.one else Int64.zero
+	| BAnd     -> Int64.logand o1 o2
+	| BXor     -> Int64.logxor o1 o2
+	| BOr      -> Int64.logor  o1 o2
+	| LAnd     -> if o1 <> Int64.zero && o2 <> Int64.zero
+	              then Int64.one else Int64.zero
+	| LOr      -> if o1 <> Int64.zero || o2 <> Int64.zero
+	              then Int64.one else Int64.zero
+
+let opposite_test (b : bop) : bop =
+	match b with
+	| Lt -> Ge | Ge -> Lt | Le -> Gt | Gt -> Le | Eq -> Ne | Ne -> Eq
+	| _ -> b
+
+type uop =
+	| Neg
+	| BNot
+	| LNot
+
+let uop_table = [| Neg; BNot; LNot; |]
+let uop_of_int (u : int) : uop = uop_table.(u)
+let int_of_uop (u : uop) : int = u |> array_mem uop_table |> L.hd
+
+let string_of_uop (u : uop) : string =
+	match u with
+	| Neg  -> "-" | BNot -> "~" | LNot -> "!"
+
+let apply_uop (u : uop) (o : int64) : int64 =
+	match u with
+	| Neg  -> Int64.neg o | BNot -> Int64.lognot o
+	| LNot -> if o = Int64.zero then Int64.one else Int64.zero
+
+
+type operand = opkind * int64
+type exp =
+	| BinOp of int64 * bop * exp * exp
+	| UnOp  of int64 * uop * exp
+	| Op    of int64 * operand
+	| Input of int64
+
+let rec string_of_exp (e : exp) : string =
+	let i64s = Int64.to_string in
+	let sofe = string_of_exp in
+	match e with
+	| Input a       -> "Input("^(i64s a)^")"
+	| Op(v,(ok, o)) -> "Op("^(i64s v)^", "^(string_of_op o ok)^")"
+	| UnOp(v,u,e)   -> "UnOp("^(i64s v)^", "^(string_of_uop u)^", "^(sofe e)^")"
+	| BinOp(v,b,e1,e2) ->
+		"BinOp("^(i64s v)^", "^(string_of_bop b)^", "^(sofe e1)^", "^(sofe e2)^")"
+
+let mkOpExp (op : int64) (opk : int) (opv : int64) : exp =
+	Op(opv, (opkind_of_int opk, op))
+

ciltut-lib/src/concolic/concolic_paths.ml

+open Concolic_util
+
+module E = Concolic_exp
+module C = Concolic_ctxt
+
+module Y = Yices
+module L = List
+module A = Array
+module H = Hashtbl
+module S = String
+
+type brState = NeitherTaken | TrueTaken | FalseTaken | BothTaken
+
+type branchID = int * int
+
+type ybranch = {
+	mutable ybid : branchID;
+	mutable yexp : Y.expr;
+	mutable ybs  : brState;
+}
+
+type ebranch = {
+	mutable bid : branchID;
+	mutable exp : E.exp;
+	mutable bs  : brState;
+}
+
+type path_state = {
+	mutable branchHT     : (branchID, brState) H.t;
+	mutable paths        : ybranch array list;
+	mutable branchCounts : (int, int) H.t;
+	mutable pathCond     : ebranch list;
+}
+
+let pState : path_state = {
+	branchHT     = H.create 256;
+	paths        = [];
+	branchCounts = H.create 256;
+	pathCond     = [];
+}
+
+let brState_of_int (r : int) : brState =
+	match r with
+	| 0 -> FalseTaken
+	| 1 -> TrueTaken
+	| _ -> raise(Failure "brState_of_int")
+
+let merge_brState (bs1 : brState) (bs2 : brState) : brState =
+	match bs1, bs2 with
+	| BothTaken, _ | _, BothTaken
+	| TrueTaken, FalseTaken | FalseTaken, TrueTaken -> BothTaken
+	| NeitherTaken, bs | bs, NeitherTaken -> bs
+	| _ -> bs1
+
+
+let getBranchCount (cid : int) : int =
+	try
+		let oldcnt = H.find pState.branchCounts cid in
+		H.replace pState.branchCounts cid (oldcnt + 1);
+		oldcnt
+	with Not_found ->
+		H.replace pState.branchCounts cid 1;
+		0
+
+let mk_ebranch (e : E.exp) (cid : int) (cnt : int) (bs : brState) : ebranch =
+	{exp = e; bid = cid,cnt; bs = bs;}
+
+let addPathCond (cid : int) (r : int) (c : E.exp) : unit =
+	let cnt = getBranchCount cid in
+	let bs  = brState_of_int r in
+	match C.simplifyExp c with
+	| E.Op _ -> ()
+	| _    -> pState.pathCond <- (mk_ebranch c cid cnt bs) :: pState.pathCond
+
+
+let yicesb_of_expb (c : C.context) (eb : ebranch) : ybranch =
+	{yexp = C.yices_of_exp c eb.exp; ybid = eb.bid; ybs = eb.bs}
+let mk_yicesb_inv (c : C.context) (yel : Y.expr list) : ybranch =
+	{yexp = yel |> A.of_list |> Y.mk_and c.C.yctx;
+	 ybid = (-1,-1); ybs = NeitherTaken;}
+
+let ybranch_swap (c : C.context) (yb : ybranch) : ybranch =
+	{yb with yexp = Y.mk_not c.C.yctx yb.yexp}
+
+let updateBState (eb : ebranch) : unit =
+	try eb.bid |> H.find pState.branchHT
+		         |> merge_brState eb.bs
+		         |> H.replace pState.branchHT eb.bid
+	with Not_found -> H.add pState.branchHT eb.bid eb.bs
+
+
+let updatePathConds (c : C.context) : unit =
+	let ybl = L.map (yicesb_of_expb c) pState.pathCond in
+	let ybl = (mk_yicesb_inv c c.C.inv) :: ybl in
+	pState.paths <- (A.of_list ybl) :: pState.paths;
+	L.iter updateBState pState.pathCond
+
+let has_swappable_branch ?(excludes : branchID list = [])
+                          (yba : ybranch array) : bool =
+	yba |> A.to_list
+	    |> L.filter (fun yb -> yb.ybs <> NeitherTaken)
+	    |> L.filter (fun yb -> not(L.mem yb.ybid excludes))
+	    |> L.exists (fun yb -> H.find pState.branchHT yb.ybid <> BothTaken)
+
+let is_swappable_branch ?(excludes : branchID list = []) (yb : ybranch) : bool =
+	yb.ybs <> NeitherTaken &&
+	H.find pState.branchHT yb.ybid <> BothTaken &&
+	not(L.mem yb.ybid excludes)
+
+let genNextPath ?(excludes : branchID list = []) (c : C.context)
+                : (Y.expr array * branchID) option
+	=
+	try
+		let p = pState.paths |> L.find (has_swappable_branch ~excludes) |> A.copy in
+		let si = p |> array_find (is_swappable_branch ~excludes) |> L.hd in
+		p.(si) <- ybranch_swap c p.(si);
+		Some(p |> A.map (fun yb -> yb.yexp), p.(si).ybid)
+	with Not_found -> None
+
+let clearPathCond () : unit =
+	H.clear pState.branchCounts;
+	pState.pathCond <- []
+
+let writeOneVal (c : C.context) (m : Y.model)
+                (a : int64) ((n, vd) : string * Y.var_decl)
+                : unit =
+	try let ba = Y.get_bv_value m vd 64 in
+	ba |> int64_of_bool_array |> C.ctxtStoreVal c n
+	with _ -> C.ctxtStoreVal c n Int64.zero
+
+let writeModelVals (c : C.context) : unit =
+	let m = Y.get_model c.C.yctx in
+	H.iter (writeOneVal c m) c.C.input;
+	c.C.inv <- [];
+	H.clear c.C.memory
+
+let genNextInputs (c : C.context) (yea : Y.expr array) (bid : branchID) : bool =
+	let ye = Y.mk_and c.C.yctx yea in
+	let aid = Y.assert_retractable c.C.yctx ye in
+	match Y.check c.C.yctx with
+	| Y.True -> begin
+		writeModelVals c;
+		Y.retract c.C.yctx aid;
+		true
+	end
+	| Y.False
+	| Y.Undef ->
+		Y.retract c.C.yctx aid;
+		false
+
+let pathsFindNext () : int =
+	let c = !C.global_ctxt |> forceOption in
+	updatePathConds c;
+	clearPathCond ();
+	let rec helper excludes =
+		match genNextPath ~excludes c with
+		| None -> 0
+		| Some(yea, bid) ->
+			if genNextInputs c yea bid then 1 else
+			helper (bid :: excludes)
+	in
+	helper []
+
+let resetPaths () : unit =
+	H.clear pState.branchHT;
+	H.clear pState.branchCounts;
+	pState.paths <- [];
+	pState.pathCond <- []

ciltut-lib/src/concolic/concolic_util.ml

+module A = Array
+module L = List
+module S = String
+
+let (|>) (a : 'a) (f : 'a -> 'b) : 'b = f a
+
+let forceOption (a : 'a option) : 'a =
+	match a with
+	| Some a -> a
+	| None -> failwith "forceOption"
+
+let int32_of_int64 (i : int64) : int32 = i |> Int64.to_int |> Int32.of_int
+
+let string_of_bool_array (ba : bool array) : string =
+	let bs =
+		ba
+		|> A.to_list
+		|> L.rev
+		|> L.map (fun b -> if b then "1" else "0")
+		|> S.concat ""
+	in
+	"0b"^bs
+
+let int64_of_bool_array (ba : bool array) : int64 =
+	ba |> string_of_bool_array |> Int64.of_string
+
+let array_mem (a : 'a array) (x : 'a) : int list =
+	let res = ref [] in
+	A.iteri (fun i y -> if x = y then res := i :: (!res)) a;
+	!res
+
+let array_find (f : 'a -> bool) (a : 'a array) : int list =
+	let res = ref [] in
+	A.iteri (fun i x -> if f x then res := i :: (!res)) a;
+	!res
+

ciltut-lib/src/tut15.c

+#include <stdint.h>
+#include <stdio.h>
+#include <string.h>
+#include <caml/mlvalues.h>
+#include <caml/callback.h>
+#include <caml/alloc.h>
+
+static int ocaml_initialized = 0;
+
+static void init_ocaml()
+{
+	if (!ocaml_initialized) {
+		char *argv[2] = {"program",NULL};
+		caml_startup(argv);
+		ocaml_initialized = 1;	
+	}
+	return;
+}
+
+void assign(uint64_t lhs, uint64_t op, int opk, uint64_t opv)
+{
+	static value *assign_closure = NULL;
+	value args[4];
+	init_ocaml();
+	if (assign_closure == NULL) {
+		assign_closure = caml_named_value("assign");
+	}
+
+	args[0] = caml_copy_int64(lhs);
+	args[1] = caml_copy_int64(op);
+	args[2] = Val_int(opk);
+	args[3] = caml_copy_int64(opv);
+	caml_callbackN(*assign_closure, 4, args);
+	return;
+}
+
+void assgn_bop(uint64_t lhs, uint64_t lhsv, int bop,
+               uint64_t op1, int op1k, uint64_t op1v,
+               uint64_t op2, int op2k, uint64_t op2v)
+{
+	static value *assgn_bop_closure = NULL;
+	value args[9];
+	init_ocaml();
+	if (assgn_bop_closure == NULL)  {
+		assgn_bop_closure = caml_named_value("assgn_bop");
+	}
+
+	args[0] = caml_copy_int64(lhs);
+	args[1] = caml_copy_int64(lhsv);
+	args[2] = Val_int(bop);
+	args[3] = caml_copy_int64(op1);
+	args[4] = Val_int(op1k);
+	args[5] = caml_copy_int64(op1v);
+	args[6] = caml_copy_int64(op2);
+	args[7] = Val_int(op2k);
+	args[8] = caml_copy_int64(op2v);
+	caml_callbackN(*assgn_bop_closure, 9, args);
+	return;
+}
+
+void assgn_uop(uint64_t lhs, uint64_t lhsv, int uop,
+               uint64_t op, int opk, uint64_t opv)
+{
+	static value *assgn_uop_closure = NULL;
+	value args[6];
+	init_ocaml();
+	if (assgn_uop_closure == NULL)  {
+		assgn_uop_closure = caml_named_value("assgn_uop");
+	}
+
+	args[0] = caml_copy_int64(lhs);
+	args[1] = caml_copy_int64(lhsv);
+	args[2] = Val_int(uop);
+	args[3] = caml_copy_int64(op);
+	args[4] = Val_int(opk);
+	args[5] = caml_copy_int64(opv);
+	caml_callbackN(*assgn_uop_closure, 6, args);
+	return;
+}
+
+void cond(int cid, int r, uint64_t op, int opk, uint64_t opv)
+{
+	static value *cond_closure = NULL;
+	value args[5];
+	init_ocaml();
+	if (cond_closure == NULL)  {
+		cond_closure = caml_named_value("cond");
+	}
+
+	args[0] = Val_int(cid);
+	args[1] = Val_int(r);
+	args[2] = caml_copy_int64(op);
+	args[3] = Val_int(opk);
+	args[4] = caml_copy_int64(opv);
+	caml_callbackN(*cond_closure, 5, args);
+	return;
+}
+
+void cond_bop(int cid, int bop, int r,
+              uint64_t op1, int op1k, uint64_t op1v,
+              uint64_t op2, int op2k, uint64_t op2v)
+{
+	static value *cond_bop_closure = NULL;
+	value args[9];
+	init_ocaml();
+	if (cond_bop_closure == NULL)  {
+		cond_bop_closure = caml_named_value("cond_bop");
+	}
+
+	args[0] = Val_int(cid);
+	args[1] = Val_int(bop);
+	args[2] = Val_int(r);
+	args[3] = caml_copy_int64(op1);
+	args[4] = Val_int(op1k);
+	args[5] = caml_copy_int64(op1v);
+	args[6] = caml_copy_int64(op2);
+	args[7] = Val_int(op2k);
+	args[8] = caml_copy_int64(op2v);
+	caml_callbackN(*cond_bop_closure, 9, args);
+	return;
+}
+
+void cond_uop(int cid, int uop, int r,
+              uint64_t op, int opk, uint64_t opv)
+{
+	static value *cond_uop_closure = NULL;
+	value args[6];
+	init_ocaml();
+	if (cond_uop_closure == NULL)  {
+		cond_uop_closure = caml_named_value("cond_uop");
+	}
+
+	args[0] = Val_int(cid);
+	args[1] = Val_int(uop);
+	args[2] = Val_int(r);
+	args[3] = caml_copy_int64(op);
+	args[4] = Val_int(opk);
+	args[5] = caml_copy_int64(opv);
+	caml_callbackN(*cond_uop_closure, 6, args);
+	return;
+}
+
+void register_input(char *name, uint64_t addr, int bits)
+{
+	static value *register_input_closure = NULL;
+	init_ocaml();
+	if (register_input_closure == NULL) {
+		register_input_closure = caml_named_value("register_input");
+	}
+
+	caml_callback3(*register_input_closure, caml_copy_string(name),
+	                                        caml_copy_int64(addr),
+	                                        Val_long(bits));
+	return;
+}
+
+void register_arr_input(char *name, uint64_t start, int sz, int cnt)
+{
+	int namelen = strlen(name);
+	char buf[namelen + 10];
+	int i;
+
+	for (i = 0; i < cnt; i++) {
+		snprintf(buf, namelen + 10, "%s%d", name, i);
+		register_input(buf, start + i * sz, sz * 8);
+	}
+
+	return;
+}
+
+void register_nt_input(char *name, char *start)
+{
+	int namelen = strlen(name);
+	char buf[namelen + 10];
+	int i = 0;
+
+	char *ptr = start;
+	do {
+		snprintf(buf, namelen + 10, "%s%d", name, i);
+		register_input(buf, (uint64_t)ptr, 8);
+		i++;
+	} while (*ptr++);
+
+	return;
+}
+
+int autotest_finished = 0;
+
+void gen_new_input()
+{
+	static value *gen_new_input_closure = NULL;
+	init_ocaml();
+	if (gen_new_input_closure == NULL) {
+		gen_new_input_closure = caml_named_value("gen_new_input");
+	}
+	value v = caml_callback(*gen_new_input_closure, Val_unit);
+	if (Int_val(v) == 0) {
+		autotest_finished = 1;
+	}
+	return;
+}
+
+void push_val(uint64_t v)
+{
+	static value *push_val_closure = NULL;
+	init_ocaml();
+	if (push_val_closure == NULL) {
+		push_val_closure = caml_named_value("push_val");
+	}
+
+	caml_callback(*push_val_closure, caml_copy_int64(v));
+	return;
+}
+
+static uint64_t pop_val_opt_print(int print, char *name)
+{
+	static value *pop_val_closure = NULL;
+	init_ocaml();
+	if (pop_val_closure == NULL) {
+		pop_val_closure = caml_named_value("pop_val");
+	}
+
+	value r = caml_callback(*pop_val_closure, caml_copy_string(name));
+	if (print) {
+		printf("%s <- %llu\n", name, (unsigned long long)Int64_val(r));
+	}
+	return Int64_val(r);
+}
+
+uint64_t pop_val(char *name)
+{
+	return pop_val_opt_print(1, name);
+}
+
+void pop_array(char *name, char *base, int cnt, int sz)
+{
+	int namelen = strlen(name);
+	char buf[namelen + 10];
+	int i;
+
+	for (i = 0; i < cnt; i++) {
+		snprintf(buf, namelen + 10, "%s%d", name, i);
+		switch (sz) {
+			case 1:
+				*(base + i) = (uint8_t)pop_val(buf);
+				break;
+			case 2:
+				*(uint16_t *)(base + i*sz) = (uint16_t)pop_val(buf);
+			case 4:
+				*(uint32_t *)(base + i*sz) = (uint32_t)pop_val(buf);
+			default:
+				*(uint64_t *)(base + i*sz) = pop_val(buf);
+		}
+	}
+
+	return;
+}
+
+void pop_nt(char *name, char *base)
+{
+	int namelen = strlen(name);
+	char buf[namelen + 10];
+	int i = 0;
+
+	char *ptr = base;
+	char c;
+	do {
+		snprintf(buf, namelen + 10, "%s%d", name, i);
+		c = (char)pop_val_opt_print(0, buf);
+		*ptr = c; ptr++; i++;
+	} while(c);
+
+	printf ("%s <- %s\n", name, base);
+
+	return;
+}
+
+void return_push(uint64_t p, uint64_t v)
+{
+	static value *return_push_closure = NULL;
+	init_ocaml();
+	if (return_push_closure == NULL) {
+		return_push_closure = caml_named_value("return_push");
+	}
+
+	caml_callback2(*return_push_closure, caml_copy_int64(p), caml_copy_int64(v));
+	return;
+}
+
+void return_pop(uint64_t p, uint64_t v)
+{
+	static value *return_pop_closure = NULL;
+	init_ocaml();
+	if (return_pop_closure == NULL) {
+		return_pop_closure = caml_named_value("return_pop");
+	}
+
+	caml_callback2(*return_pop_closure, caml_copy_int64(p), caml_copy_int64(v));
+	return;
+}
+
+void autotest_reset()
+{
+	static value *autotest_reset_closure = NULL;
+	init_ocaml();
+	if (autotest_reset_closure == NULL) {
+		autotest_reset_closure = caml_named_value("autotest_reset");
+	}
+	caml_callback(*autotest_reset_closure , Val_unit);
+	autotest_finished = 0;
+	return;
+}
 ac_unique_file="src/main.ml"
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
+BUILD_TUT15
 BUILD_TUT11
 OCAMLINC
 CILTUT_VERSION
 DEFAULT_CIL_MODE
 CILTUTHOME
 ARCHOS
+OCAML_PKG_ocamlyices
 HAVE_WHY3
 OCAML_PKG_ocamlgraph
 OCAML_PKG_cil
 ac_user_opts='
 enable_option_checking
 enable_tut11
+enable_tut15
 '
       ac_precious_vars='build_alias
 host_alias
   --disable-FEATURE       do not include FEATURE (same as --enable-FEATURE=no)
   --enable-FEATURE[=ARG]  include FEATURE [ARG=yes]
   --disable-tut11         Do not build tut11
+  --disable-tut15         Do not build tut15
 
 Some influential environment variables:
   CC          C compiler command
 $as_echo "$as_me: WARNING: Why3 not found. Tut11 won't be built" >&2;}
 fi
 
+# Check for yices and ocamlyices to see if we should build tut15
+#
+#
+# Check whether --enable-tut15 was given.
+if test "${enable_tut15+set}" = set; then :
+  enableval=$enable_tut15; ac_build_tut15=$enableval
+else
+  ac_build_tut15=yes
+fi
+
+
+if test "x$ac_build_tut15" = "xno"; then
+  HAVE_YICES=false
+else
+
+  { $as_echo "$as_me:${as_lineno-$LINENO}: checking for OCaml findlib package ocamlyices" >&5
+$as_echo_n "checking for OCaml findlib package ocamlyices... " >&6; }
+
+  unset found
+  unset pkg
+  found=no
+  for pkg in ocamlyices  ; do
+    if $OCAMLFIND query $pkg >/dev/null 2>/dev/null; then
+      { $as_echo "$as_me:${as_lineno-$LINENO}: result: found" >&5
+$as_echo "found" >&6; }
+      OCAML_PKG_ocamlyices=$pkg
+      found=yes
+      break
+    fi
+  done
+  if test "$found" = "no" ; then
+    { $as_echo "$as_me:${as_lineno-$LINENO}: result: not found" >&5
+$as_echo "not found" >&6; }
+    OCAML_PKG_ocamlyices=no
+  fi
+
+
+
+  if test "x$OCAML_PKG_ocamlyices" = "xno"; then
+    as_fn_error $? "*** Couldn't find Ocamlyices installation. Use --disable-tut15, or install yices and ocamlyices" "$LINENO" 5
+  fi
+
+  BUILD_TUT15="true"
+fi
+if test $BUILD_TUT15 = "false"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ocamlyices not found. Tut15 won't be built" >&5
+$as_echo "$as_me: WARNING: Ocamlyices not found. Tut15 won't be built" >&2;}
+fi
+
+
 
 
 
   Ciltut home:                   $CILTUTHOME
   Ciltut version:                $CILTUT_VERSION
   Build Tutorial 11              $BUILD_TUT11
+  Build Tutorial 15              $BUILD_TUT15
 EOF
   AC_MSG_WARN([Why3 not found. Tut11 won't be built])
 fi
 
+# Check for yices and ocamlyices to see if we should build tut15
+#
+#
+AC_ARG_ENABLE([tut15],
+              AS_HELP_STRING([--disable-tut15], [Do not build tut15]),
+              [ac_build_tut15=$enableval], [ac_build_tut15=yes])
+
+if test "x$ac_build_tut15" = "xno"; then
+  HAVE_YICES=false
+else
+  AC_CHECK_OCAML_PKG([ocamlyices])
+  if test "x$OCAML_PKG_ocamlyices" = "xno"; then
+    AC_MSG_ERROR([*** Couldn't find Ocamlyices installation. Use --disable-tut15, or install yices and ocamlyices])
+  fi
+
+  BUILD_TUT15="true"
+fi
+if test $BUILD_TUT15 = "false"; then
+  AC_MSG_WARN([Ocamlyices not found. Tut15 won't be built])
+fi
+
 AC_SUBST(ARCHOS)
 AC_SUBST(CILTUTHOME)
 AC_SUBST(DEFAULT_CIL_MODE)
 AC_SUBST(CILTUT_VERSION)
 AC_SUBST(OCAMLINC)
 AC_SUBST(BUILD_TUT11)
+AC_SUBST(BUILD_TUT15)
 
 # finish the configure script and generate various files; ./configure
 # will apply variable substitutions to <filename>.in to generate <filename>;
   Ciltut home:                   $CILTUTHOME
   Ciltut version:                $CILTUT_VERSION
   Build Tutorial 11              $BUILD_TUT11
+  Build Tutorial 15              $BUILD_TUT15
 EOF
     # Override Cilly's default
     $self->{SEPARATE} = 1;
 
+    $self->{TUT15} = 0;
+
     bless $self, $class;
 }
 
         push @{$self->{CILARGS}}, "--out", $1;
     } elsif ($arg eq '--merge') {
         $self->{SEPARATE} = 0;
+    } elsif ($arg eq '--enable-tut15') {
+        $self->{TUT15} = 1;
+        push @{$self->{CILARGS}}, "--enable-tut15";
     } elsif ($arg =~ m|^--|) {
         # All other arguments starting with -- are passed to CIL
         # Split the ==
         print STDERR "ciltutcc: no input files\n";
         return 0;
     } else {
-	    unshift @libs, @{$self->{CILTUTLIBS}}, "-ldl", "-lrt";
+        unshift @libs, @{$self->{CILTUTLIBS}}, "-ldl", "-lrt";
+        if ($self->{TUT15} == 1) {
+            my $ocy = `ocamlfind query ocamlyices`;
+            chomp($ocy);
+            push @libs, "-L/usr/lib/ocaml", "-lunix", "-lnums", "-lcamlrun",
+                           "-lm", "-lcurses", "-L$ocy" , "-locamlyices",
+                           "-lstdc++", "/usr/local/lib/libyices.a";
+        }
         return $self->SUPER::link_after_cil(\@srcs, $dest, $ppargs,
                                             \@cargs, \@libs);
     }
         print STDERR "ciltutcc: no input files\n";
         return 0;
     } else {
-    	push @libs, @{$self->{CILTUTLIBS}};
+        push @libs, @{$self->{CILTUTLIBS}};
         return $self->SUPER::linktolib(\@srcs, $dest, $ppargs,
                                        $ccargs, $ldargs);
     }

src/ciltutoptions.ml

 let home : string ref = ref ""
 let merge : bool ref = ref false
 
-let num_tuts = 15
+let num_tuts = 16
 let enable_tut : bool ref array = Array.init num_tuts (fun i -> ref false)
 
 let prover : string ref = ref "alt-ergo"
   if !(O.enable_tut.(12)) then Tut12.tut12 cil;
   if !(O.enable_tut.(13)) then Tut13.tut13 cil;
   if !(O.enable_tut.(14)) then Tut14.tut14 cil;
+  if !(O.enable_tut.(15)) then Tut15.tut15 cil;
   outputFile cil
 ;;
 
   Wc.load_plugins main;
   let provers = Wc.get_provers config in
   let prover =
-    try W.Util.Mstr.find p provers
+    
+    try Wc.prover_by_id config p
     with Not_found -> Em.s (Em.error "Prover %s not found." p)
   in
   let env = E.create_env (W.Whyconf.loadpath main) in
-  let driver =
-    try W.Driver.load_driver env prover.Wc.driver
+  let driver : W.Driver.driver =
+    try W.Driver.load_driver env prover.Wc.driver []
     with e -> Em.s (Em.error "Failed to load driver for %s." p)
   in
   let int_theory = E.find_theory env ["int"] "Int" in
+
+
+
+
+IFDEF BUILD_TUT15 THEN
+
+
+
+
+open Cil
+open Pretty
+open Tututil
+
+module E = Errormsg
+module L = List
+module H = Hashtbl
+
+let autotest_str = "autotest"
+let isAutotestType   (t : typ) : bool = hasAttribute "autotest"   (typeAttrs t) 
+let isInstrumentType (t : typ) : bool = hasAttribute "instrument" (typeAttrs t)
+
+let input_str    = "input"
+let inputarr_str = "inputarr"
+let inputnt_str  = "inputnt"
+
+let isInputArrType (t : typ) : bool = hasAttribute "inputarr" (typeAttrs t)
+let isInputNTType  (t : typ) : bool = hasAttribute "inputnt"  (typeAttrs t)
+
+let isInputType (t : typ) : bool =
+  let a = typeAttrs t in
+  hasAttribute "input" a    ||
+  hasAttribute "inputarr" a ||
+  hasAttribute "inputnt" a
+
+let getInputArrLen (t : typ) : int =
+  match filterAttributes "inputarr" (typeAttrs t) with
+  | [Attr("inputarr", [AInt n])] -> n
+  | _ -> E.s(E.error "Malforemd inputarr attribute")
+
+let dummyVar = makeVarinfo false "_tut_foo" voidType
+
+let instCallHash : (string, varinfo) H.t = H.create 32
+let uint64_t : typ ref = ref voidType
+let finished : varinfo ref = ref dummyVar
+let initCalls (f : file) =
+  let focf : string -> typ -> varinfo = findOrCreateFunc f in
+  uint64_t := findType f.globals "uint64_t";
+  finished := findGlobalVar f.globals "autotest_finished";
+  let u64v n = (n, !uint64_t, []) in
+  let intv n = (n, intType,  []) in
+  let strv n = (n, charPtrType, []) in
+  let mkft r aa = TFun(r, Some aa, false, []) in
+  let void = voidType in
+  L.iter (fun (n,rt,atl) -> H.add instCallHash n (focf n (mkft rt atl))) [
+("assign",    void, [u64v "lhs"; u64v "op"; intv "opk"; u64v "opv";]);
+("assgn_bop", void, [u64v "lhs"; u64v "lhsv"; intv "bop";
+                     u64v "op1"; intv "op1k"; u64v "op1v";
+                     u64v "op2"; intv "op2k"; u64v "op2v";]);
+("assgn_uop", void, [u64v "lhs"; u64v "lhsv"; intv "uop";
+                     u64v "op"; intv "opk"; u64v "opv";]);
+("cond",      void, [intv "cid"; intv "r";
+                     u64v "op"; intv "opk"; u64v "opv";]);
+("cond_bop",  void, [intv "cid"; intv "bop"; intv "r";
+                     u64v "op1"; intv "op1k"; u64v "op1v";
+                     u64v "op2"; intv "op2k"; u64v "op2v";]);
+("cond_uop",  void, [intv "cid"; intv "uop"; intv "r";
+                     u64v "op"; intv "opk"; u64v "opv";]);
+("register_input",     void, [strv "name"; u64v "addr";intv "bits"]);
+("register_arr_input", void, [strv "name"; u64v "start"; intv "sz" ;intv "cnt"]);
+("register_nt_input",  void, [strv "name"; strv "start";]);
+("gen_new_input",      void, []);
+("push_val",           void, [u64v "v"]);
+("pop_val",            !uint64_t, [strv "name"]);
+("pop_array",          void, [strv "name"; strv "base"; intv "cnt"; intv "sz";]);
+("pop_nt",             void, [strv "name"; strv "base";]);
+("return_push",        void, [u64v "p";u64v "v"]);
+("return_pop",         void, [u64v "p";u64v "v"]);
+("autotest_reset",     void, []);]
+
+let getIcall (n : string) : exp = n |> H.find instCallHash |> v2e
+
+let int_of_bop (b : binop) : int =
+  match b with
+  | PlusA         | PlusPI        | IndexPI -> 0
+  | MinusA        | MinusPI       | MinusPP -> 1
+  | Mult    -> 2  | Div     -> 3  | Mod     -> 4
+  | Shiftlt -> 5  | Shiftrt -> 6  | Lt      -> 8
+  | Gt      -> 9  | Le      -> 10 | Ge      -> 11
+  | Eq      -> 12 | Ne      -> 13 | BAnd    -> 14
+  | BXor    -> 15 | BOr     -> 16 | LAnd    -> 17
+  | LOr     -> 18
+
+let int_of_uop (u : unop) : int =
+  match u with
+  | Neg  -> 0 | BNot -> 1 | LNot -> 2
+
+let rec op_of_exp (e : exp) : exp * exp =
+  let cast e = CastE(!uint64_t, e) in
+  match e with
+  | Const _ -> cast e, integer 0
+  | AddrOf(Var v, NoOffset) -> cast e, integer 0
+  | StartOf(Var v, NoOffset) -> cast e, integer 0
+  | Lval(Var v, off) -> cast(AddrOf(Var v, off)), integer 1
+  | Lval(Mem e, NoOffset) -> cast e, integer 1
+  | CastE(t, e) -> op_of_exp e
+  | _ -> E.s(E.bug "Unexpected expression in binop")
+
+let make_assign_call (lhs : lval) (e : exp) (loc : location) : instr list =
+  if isScalarType (typeOfLval lhs) then
+   let lhsaddr     = CastE(!uint64_t, AddrOf lhs) in
+    let eop, eopk = op_of_exp e in
+    let ecst = CastE(!uint64_t, e) in
+    [Set(lhs, e, loc);
+     Call(None, getIcall "assign", [lhsaddr; eop; eopk; ecst], loc);]
+  else [Set(lhs, e, loc)]
+
+let make_assgn_bop_call (lhs : lval) (b : binop) (rt : typ) (loc : location)
+                        (e1 : exp) (e2 : exp)
+                        : instr list
+  =
+  if isScalarType (typeOfLval lhs) then
+    let lhsaddr     = CastE(!uint64_t, AddrOf lhs) in
+    let bopint      = int_of_bop b in
+    let e1op, e1opk = op_of_exp e1 in
+    let e2op, e2opk = op_of_exp e2 in
+    let e1cst       = CastE(!uint64_t, e1) in
+    let e2cst       = CastE(!uint64_t, e2) in
+    [Set(lhs, BinOp(b, e1, e2, rt), loc);
+     Call(None, getIcall "assgn_bop", [lhsaddr;Lval lhs;integer bopint;
+                                       e1op; e1opk; e1cst; e2op; e2opk; e2cst],
+          loc)]
+  else [Set(lhs, BinOp(b, e1, e2, rt), loc)]
+
+let make_assgn_uop_call (lhs : lval) (u : unop) (rt : typ) (loc : location)
+                        (e : exp)
+                        : instr list
+  =
+  if isScalarType (typeOfLval lhs) then
+    let lhsaddr     = CastE(!uint64_t, AddrOf lhs) in
+    let uopint      = int_of_uop u in
+    let eop, eopk   = op_of_exp e in
+    let ecst        = CastE(!uint64_t, e) in
+    [Set(lhs, UnOp(u, e, rt), loc);
+     Call(None, getIcall "assgn_uop", [lhsaddr;Lval lhs;integer uopint;
+                                       eop; eopk; ecst;], loc)]
+  else [Set(lhs, UnOp(u, e, rt), loc)]
+
+
+let make_cond_call (cid : int) (r : int) (loc : location) (e : exp) : instr =
+  let eop, eopk = op_of_exp e in
+  let ecst      = CastE(!uint64_t, e) in
+  Call(None, getIcall "cond", [integer cid; integer r; eop; eopk; ecst;], loc)
+
+let make_cond_bop_call (cid : int) (bop : binop) (r : int) (loc : location)
+                       (e1 : exp) (e2 : exp)
+                       : instr
+  =
+  let bopint      = int_of_bop bop in
+  let e1op, e1opk = op_of_exp e1 in
+  let e2op, e2opk = op_of_exp e2 in
+  let e1cst       = CastE(!uint64_t, e1) in
+  let e2cst       = CastE(!uint64_t, e2) in
+  Call(None, getIcall "cond_bop",
+       [integer cid; integer bopint; integer r;
+        e1op; e1opk; e1cst; e2op; e2opk; e2cst], loc)
+
+let make_cond_uop_call (cid : int) (uop : unop) (r : int) (loc : location)
+                       (e : exp)
+                       : instr
+  =
+  let uopint    = int_of_uop uop in
+  let eop, eopk = op_of_exp e in
+  let ecst      = CastE(!uint64_t, e) in
+  Call(None, getIcall "cond_uop",
+       [integer cid; integer uopint; integer r; eop; eopk; ecst;], loc)
+
+let make_input_gen_call (loc : location) : instr =
+  Call(None, getIcall "gen_new_input", [], loc)
+
+let make_push_val_call (loc : location) (e : exp) : instr =
+  Call(None, getIcall "push_val", [e], loc)
+
+let make_pop_val_call (loc : location) ((rvi, n) : varinfo * string) : instr list =
+  match rvi.vtype with
+  | TPtr(rt, a) when isInputNTType  rvi.vtype ->
+    [Call(None, getIcall "pop_nt", [mkString n; v2e rvi], loc)]
+  | TPtr(rt, a) when isInputArrType rvi.vtype ->
+    let cnt = getInputArrLen rvi.vtype in
+    [Call(None, getIcall "pop_array",
+          [mkString n; v2e rvi; integer cnt; SizeOf rt;], loc)]
+  | TInt _ -> [Call(Some(var rvi),getIcall "pop_val", [mkString n], loc)]
+  | _ -> []
+
+let handle_instr (i : instr) : instr list =
+  match i with
+  | Set(lhs, UnOp(u, e, rt), loc) ->
+    make_assgn_uop_call lhs u rt loc e
+  | Set(lhs, BinOp(b, e1, e2, rt), loc) ->
+    make_assgn_bop_call lhs b rt loc e1 e2
+  | Set(lhs, e, loc) ->
+    make_assign_call lhs e loc
+  | _ -> [i]
+
+let make_return_pop_call (rlv : lval) (fe : exp) (args : exp list) (loc : location)
+                         : instr list
+  =
+  [Call(Some rlv, fe, args, loc);
+   Call(None, getIcall "return_pop", [AddrOf rlv; Lval rlv], loc)]
+
+let make_return_push_call (fd : fundec) (e : exp) (loc : location) : instr list =
+  let rvi = makeTempVar fd ~name:"ret" (typeOf e) in
+  (handle_instr (Set(var rvi, e, loc)))@
+  [Call(None, getIcall "return_push", [AddrOf(var rvi); Lval(var rvi)],loc)]
+
+let cond_id = ref 0
+class concolicCalleeVisitor (autotest : bool) (fd : fundec) = object(self)
+  inherit nopCilVisitor
+
+  method vinst (i : instr) =
+    match i with
+    | Set(lhs, UnOp(u, e, rt), loc) ->
+      ChangeTo(make_assgn_uop_call lhs u rt loc e)
+    | Set(lhs, BinOp(b, e1, e2, rt), loc) ->
+      ChangeTo(make_assgn_bop_call lhs b rt loc e1 e2)
+    | Set(lhs, e, loc) ->
+      ChangeTo(make_assign_call lhs e loc)
+    | Call(Some lv, fe, args, loc) ->
+      ChangeTo(make_return_pop_call lv fe args loc)
+    | _ -> DoChildren
+
+  method vstmt (s : stmt) =
+    let action s =
+      match s.skind with
+      | If(e,tb,fb,loc) -> begin
+        let cid = !cond_id in incr cond_id;
+        let tinstr, finstr =
+          match e with
+          | BinOp(b,e1,e2,rt) -> make_cond_bop_call cid b 1 loc e1 e2,
+                                 make_cond_bop_call cid b 0 loc e1 e2
+          | UnOp(u,e,rt)      -> make_cond_uop_call cid u 1 loc e,
+                                 make_cond_uop_call cid u 0 loc e
+          | _                 -> make_cond_call cid 1 loc e,
+                                 make_cond_call cid 0 loc e
+        in
+        tb.bstmts <- mkStmt(Instr[tinstr]) :: tb.bstmts;
+        fb.bstmts <- mkStmt(Instr[finstr]) :: fb.bstmts;
+        s
+      end
+      | Return(eo,loc) when autotest ->
+        mkStmt(Block(mkBlock[mkStmt(Instr[make_input_gen_call loc]);s]))
+      | Return(Some e, loc) when not autotest ->
+        mkStmt(Block(mkBlock[mkStmt(Instr(make_return_push_call fd e loc));s]))
+      | _ -> s
+    in
+    ChangeDoChildrenPost(s, action)
+
+end
+
+let mk_reset_call (loc : location) : instr =
+  Call(None, getIcall "autotest_reset", [], loc)
+
+let makeTestLoop (fd : fundec) (loc : location)
+                 (preloop : instr list) (body : instr list)
+                 : stmt list
+  =
+  Formatcil.cStmts "%I:preloop while(%l:finished == 0) { %I:body } %i:reset;"
+  (fun n t -> makeTempVar fd ~name:n t) loc
+  [("preloop",  FI preloop);
+   ("finished", Fl(var !finished));
+   ("body",     FI body);
+   ("reset",    Fi(mk_reset_call loc));]
+
+let procInstrList (fd : fundec) (il : instr list) : stmt =
+  mkStmt(Block(mkBlock
+  (L.map (fun i ->
+    match i with
+    | Call(rvo, fe, args, loc) when fe |> typeOf |> isAutotestType ->
+      
+      let rt, ats = function_elements fe in
+      let init_instrs, nvis =
+        ats  |> L.map snd3
+             |> L.map (makeTempVar fd ~name:"in")
+             |> L.combine args
+             |> L.map (fun (a, v) -> Set(var v, a, loc), v)
+             |> L.split
+      in
+      let nargs = L.map v2e nvis in
+      let pop_instrs  =
+        L.combine nvis (L.map fst3 ats)
+             |> L.map (make_pop_val_call loc)
+             |> L.concat
+      in
+      let orig = Call(rvo,fe,nargs,loc) in
+      let lbsl = makeTestLoop fd loc init_instrs (orig :: pop_instrs) in
+      mkStmt(Block(mkBlock lbsl))
+    | _ -> mkStmt(Instr[i])
+  ) il)))
+
+class concolicCallerVisitor (fd : fundec) = object(self)
+  inherit nopCilVisitor
+
+  method vstmt (s : stmt) =
+    match s.skind with
+    | Instr il -> ChangeTo(procInstrList fd il)
+    | _ -> DoChildren
+
+end
+
+let make_input_reg_call (loc : location) (vi : varinfo) : instr list =
+  if not(isInputType vi.vtype) then [] else
+  match vi.vtype with
+  | TPtr(rt, a) when isInputArrType vi.vtype ->
+    let cnt = getInputArrLen vi.vtype in
+    [Call(None, getIcall "register_arr_input",
+         [mkString vi.vname; v2e vi; SizeOf(rt); integer cnt], loc)]
+  | TPtr(rt, a) when isInputNTType  vi.vtype ->
+    [Call(None, getIcall "register_nt_input", [mkString vi.vname; v2e vi], loc)]
+  | TInt _ ->
+    [Call(None, getIcall "register_input",
+          [mkString vi.vname; AddrOf(Var vi, NoOffset);
+           vi.vtype |> bitsSizeOf |> integer], loc)]
+  | _ -> []
+
+let makeAutotestPreamble (fd : fundec) : unit =
+  let ircalls =
+    fd.sformals |> L.map (make_input_reg_call locUnknown)
+                |> L.concat
+  in
+  let irstmt = mkStmt(Instr ircalls) in
+  fd.sbody.bstmts <- irstmt :: fd.sbody.bstmts
+
+let processFunction (fd : fundec) (loc : location) : unit =
+  if isAutotestType fd.svar.vtype then
+    let vis = new concolicCalleeVisitor true fd in
+    ignore(visitCilFunction vis fd);
+    makeAutotestPreamble fd
+  else if isInstrumentType fd.svar.vtype then
+    let vis = new concolicCalleeVisitor false fd in
+    ignore(visitCilFunction vis fd)
+  else
+    let vis = new concolicCallerVisitor fd in
+    ignore(visitCilFunction vis fd)
+
+let tut15 (f : file) : unit =
+  initCalls f;
+  List.iter Simplify.doGlobal f.globals;
+  iterGlobals f (onlyFunctions processFunction)
+
+ELSE
+
+
+let tut15 (f : Cil.file) : unit = ()
+
+END
+
+
+
   | GEnumTagDecl(ei,_) :: _ when ei.ename = typname -> TEnum(ei,[])
   | _ :: rst -> findType rst typname
 
+let rec findFunction (gl : global list) (fname : string) : fundec =
+    match gl with
+    | [] -> raise(Failure "Function not found")
+    | GFun(fd,_) :: _ when fd.svar.vname = fname -> fd
+    | _ :: rst -> findFunction rst fname
+
+let rec findCompinfo (gl : global list) (ciname : string) : compinfo =
+	match gl with
+	| [] -> raise(Failure "Compinfo not found")
+	| GCompTag(ci, _) :: _ when ci.cname = ciname -> ci
+	| GCompTagDecl(ci, _) :: _ when ci.cname = ciname -> ci
+	| _ :: rst -> findCompinfo rst ciname
+
 let rec findGlobalVar (gl : global list) (varname : string) : varinfo =
   match gl with
   | [] -> E.s (E.error "Global not found: %s" varname)
+
+
+
+
+
+
+
+
+
+
+
+#include <ciltut.h>
+
+
+
+
+
+
+
+
+
+
+int (instrument string_compare)(char *a, char *b)
+{
+	int i = 0;
+
+	while (1) {
+		if (a[i] > b[i]) return 1;
+		if (a[i] < b[i]) return -1;
+		if (a[i] == 0 && b[i] == 0) break;
+		i++;
+	}
+
+	return 0;
+}
+
+
+
+
+
+
+
+
+
+
+
+uint64_t (autotest f)(int input a, int input b)
+{
+	if ((a * b) - (a + b) == 14862436) {
+		return 1;
+	}
+	else return 0;
+}
+
+
+
+
+
+
+
+
+
+uint64_t (autotest g)(char *inputnt s)
+{
+	return string_compare(s, "autotest");
+}
+
+int main ()
+{
+	uint64_t res;
+	char cheese[1024] = "cheese";
+
+	res = f(0,0);
+	res = g(cheese);
+
+	return res;
+}
+