More updates to C backend

Add support for short-ciruiting and/or. I forgot about this in the
original ANF specification and not having it causes problems for the
ARM spec.

7 files changed, 337 insertions, 36 deletions

diff --git a/lib/exception_basic.sail b/lib/exception_basic.sail
new file mode 100644
index 00000000..cab394b0
--- /dev/null
+++ b/lib/exception_basic.sail
@@ -0,0 +1,6 @@
+$ifndef _EXN_BASIC
+$define _EXN_BASIC
+
+newtype exception = Exception : unit
+
+$endif
diff --git a/lib/flow.sail b/lib/flow.sail
index 1a0e0f2f..b904c0bc 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -37,6 +37,11 @@ overload operator == = {eq_atom, eq_range, eq_int}
 overload operator | = {or_bool}
 overload operator & = {and_bool}
 
+overload operator <= = {lteq_atom, lteq_range_atom, lteq_atom_range}
+overload operator < = {lt_atom, lt_range_atom, lt_atom_range}
+overload operator >= = {gteq_atom, gteq_range_atom, gteq_atom_range}
+overload operator > = {gt_atom, gt_range_atom, gt_atom_range}
+
 $ifdef TEST
 
 val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 8a55ed61..130f4d63 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -1,15 +1,47 @@
 $ifndef _VECTOR_DEC
 $define _VECTOR_DEC
 
+$include <flow.sail>
+
 type bits ('n : Int) = vector('n, dec, bit)
 
+val "eq_bit" : (bit, bit) -> bool
+
+val "eq_bits" : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
+
+overload operator == = {eq_bit, eq_bits}
+
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+
+val vector_length = {
+  ocaml: "length",
+  lem: "length_list",
+  c: "length"
+} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+
+overload length = {bitvector_length, vector_length}
+
 val "zeros" : forall 'n. atom('n) -> bits('n)
 
 val "print_bits" : forall 'n. (string, bits('n)) -> unit
 
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
 val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
+val "truncate" : forall 'm 'n, 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
+
+val mask : forall 'len 'v, 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
+
+function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_extend(v, len)
+
+overload operator ^ = {mask}
+
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+
+overload append = {bitvector_concat}
+
 /* Used for creating long bitvector literals in the C backend. */
 val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
 
@@ -35,4 +67,30 @@ val add_bits_int = {
   c: "add_bits_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
+overload operator + = {add_bits, add_bits_int}
+
+val vector_subrange = {
+  ocaml: "subrange",
+  lem: "subrange_vec_dec",
+  c: "vector_subrange"
+} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+
+val vector_update_subrange = {
+  ocaml: "update_subrange",
+  lem: "update_subrange_vec_dec",
+  c: "vector_update_subrange"
+} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+// Some ARM specific builtins
+
+val get_slice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
+
+val set_slice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
+
+val set_slice_bits = "set_slice" : forall 'n 'm.
+  (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
+
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+
 $endif
diff --git a/src/c_backend.ml b/src/c_backend.ml
index fa1f2b5e..adc44820 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -138,6 +138,9 @@ type aexp =
   | AE_record_update of aval * aval Bindings.t * typ
   | AE_for of id * aexp * aexp * aexp * order * aexp
   | AE_loop of loop * aexp * aexp
+  | AE_short_circuit of sc_op * aval * aexp
+
+and sc_op = SC_and | SC_or
 
 and apat =
   | AP_tup of apat list
@@ -212,6 +215,7 @@ let rec aexp_rename from_id to_id aexp =
   | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when Id.compare from_id to_id = 0 -> AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
   | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> AE_for (id, recur aexp1, recur aexp2, recur aexp3, order, recur aexp4)
   | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, recur aexp1, recur aexp2)
+  | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval_rename from_id to_id aval, recur aexp)
 
 and apexp_rename from_id to_id (apat, aexp1, aexp2) =
   if IdSet.mem from_id (apat_bindings apat) then
@@ -251,6 +255,7 @@ let rec no_shadow ids aexp =
      let ids = IdSet.add id ids in
      AE_for (id, no_shadow ids aexp1, no_shadow ids aexp2, no_shadow ids aexp3, order, no_shadow ids aexp4)
   | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, no_shadow ids aexp1, no_shadow ids aexp2)
+  | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, no_shadow ids aexp)
 
 and no_shadow_apexp ids (apat, aexp1, aexp2) =
   let shadows = IdSet.inter (apat_bindings apat) ids in
@@ -283,12 +288,14 @@ let rec map_aval f = function
      AE_case (f aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ)
   | AE_try (aexp, cases, typ) ->
      AE_try (map_aval f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ)
+  | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f aval, map_aval f aexp)
 
 (* Map over all the functions in an aexp. *)
 let rec map_functions f = function
   | AE_app (id, vs, typ) -> f id vs typ
   | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ)
   | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp)
+  | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp)
   | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2)
   | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ)
   | AE_if (aval, aexp1, aexp2, typ) ->
@@ -337,6 +344,10 @@ let rec pp_aexp = function
      pp_annot typ (pp_id id) ^^ string " := " ^^ pp_aexp aexp
   | AE_app (id, args, typ) ->
      pp_annot typ (pp_id id ^^ parens (separate_map (comma ^^ space) pp_aval args))
+  | AE_short_circuit (SC_or, aval, aexp) ->
+     pp_aval aval ^^ string " || " ^^ pp_aexp aexp
+  | AE_short_circuit (SC_and, aval, aexp) ->
+     pp_aval aval ^^ string " && " ^^ pp_aexp aexp
   | AE_let (id, id_typ, binding, body, typ) -> group
      begin
        match binding with
@@ -455,6 +466,9 @@ let rec apat_globals = function
 let rec anf (E_aux (e_aux, exp_annot) as exp) =
   let to_aval = function
     | AE_val v -> (v, fun x -> x)
+    | AE_short_circuit (_, _, _) as aexp ->
+       let id = gensym () in
+       (AV_id (id, Local (Immutable, bool_typ)), fun x -> AE_let (id, bool_typ, aexp, x, typ_of exp))
     | AE_app (_, _, typ)
       | AE_let (_, _, _, _, typ)
       | AE_return (_, typ)
@@ -536,6 +550,18 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
     let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in
     exp_wrap (wrap (AE_record_update (aval, record, typ_of exp)))
 
+  | E_app (id, [exp1; exp2]) when string_of_id id = "and_bool" ->
+     let aexp1 = anf exp1 in
+     let aexp2 = anf exp2 in
+     let aval1, wrap = to_aval aexp1 in
+     wrap (AE_short_circuit (SC_and, aval1, aexp2))
+
+  | E_app (id, [exp1; exp2]) when string_of_id id = "or_bool" ->
+     let aexp1 = anf exp1 in
+     let aexp2 = anf exp2 in
+     let aval1, wrap = to_aval aexp1 in
+     wrap (AE_short_circuit (SC_or, aval1, aexp2))
+
   | E_app (id, exps) ->
      let aexps = List.map anf exps in
      let avals = List.map to_aval aexps in
@@ -1606,6 +1632,29 @@ let rec compile_aexp ctx = function
      (fun clexp -> icopy clexp (F_id gs, ctyp)),
      gs_cleanup
 
+  | AE_short_circuit (SC_and, aval, aexp) ->
+     let left_setup, cval, left_cleanup = compile_aval ctx aval in
+     let right_setup, _, call, right_cleanup = compile_aexp ctx aexp in
+     let gs = gensym () in
+     left_setup
+     @ [ idecl CT_bool gs;
+         iif cval (right_setup @ [call (CL_id gs)] @ right_cleanup) [icopy (CL_id gs) (F_lit "false", CT_bool)] CT_bool ]
+     @ left_cleanup,
+     CT_bool,
+     (fun clexp -> icopy clexp (F_id gs, CT_bool)),
+     []
+  | AE_short_circuit (SC_or, aval, aexp) ->
+     let left_setup, cval, left_cleanup = compile_aval ctx aval in
+     let right_setup, _, call, right_cleanup = compile_aexp ctx aexp in
+     let gs = gensym () in
+     left_setup
+     @ [ idecl CT_bool gs;
+         iif cval [icopy (CL_id gs) (F_lit "true", CT_bool)] (right_setup @ [call (CL_id gs)] @ right_cleanup) CT_bool ]
+     @ left_cleanup,
+     CT_bool,
+     (fun clexp -> icopy clexp (F_id gs, CT_bool)),
+     []
+
   | AE_assign (id, assign_typ, aexp) ->
      (* assign_ctyp is the type of the C variable we are assigning to,
         ctyp is the type of the C expression being assigned. These may
@@ -2786,9 +2835,6 @@ let codegen_def' ctx = function
        | _ -> assert false
      in
      let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in
-     prerr_endline (string_of_id id);
-     prerr_endline (Util.string_of_list ", " (fun arg -> sgen_id arg) args);
-     prerr_endline (Util.string_of_list ", " (fun ctyp -> sgen_ctyp ctyp) arg_ctyps);
      let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in
      let function_header =
        match ret_arg with
@@ -2888,7 +2934,7 @@ let compile_ast ctx (Defs defs) =
     let postamble = separate hardline (List.map string
        ( [ "int main(void)";
            "{";
-           "  setup_real();" ]
+           "  setup_library();" ]
        @ fst exn_boilerplate
        @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
        @ (if regs = [] then [] else [ "  zinitializze_registers(UNIT);" ])
@@ -2897,8 +2943,9 @@ let compile_ast ctx (Defs defs) =
        @ letbind_finalizers
        @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs)
        @ snd exn_boilerplate
-       @ [ "  return 0;" ]
-       @ [ "}" ] ))
+       @ [ "  cleanup_library();";
+           "  return 0;";
+           "}" ] ))
     in
 
     let hlhl = hardline ^^ hardline in
diff --git a/test/c/sail.h b/test/c/sail.h
index 880f5a57..92127a1b 100644
--- a/test/c/sail.h
+++ b/test/c/sail.h
@@ -38,7 +38,7 @@ unit sail_exit(const unit u) {
 }
 
 void elf_entry(mpz_t *rop, const unit u) {
-  mpz_set_ui(*rop, 0x8000ul);
+  mpz_set_ui(*rop, 0x400130ul);
 }
 
 // Sail bits are mapped to ints where bitzero = 0 and bitone = 1
@@ -240,6 +240,11 @@ void pow2(mpz_t *rop, mpz_t exp) {
 
 // ***** Sail bitvectors *****
 
+unit print_bits(const sail_string str, const bv_t op) {
+  fputs(str, stdout);
+  gmp_printf("%d'0x%ZX\n", op.len, op.bits);
+}
+
 void length_bv_t(mpz_t *rop, const bv_t op) {
   mpz_set_ui(*rop, op.len);
 }
@@ -278,13 +283,22 @@ void replicate_bits(bv_t *rop, const bv_t op1, const mpz_t op2) {
   rop->len = op1.len * op2_ui;
   mpz_set(*rop->bits, *op1.bits);
   for (int i = 1; i < op2_ui; i++) {
-    mpz_mul_2exp(*rop->bits, *rop->bits, op2_ui);
-    mpz_add(*rop->bits, *rop->bits, *op1.bits);
+    mpz_mul_2exp(*rop->bits, *rop->bits, op1.len);
+    mpz_ior(*rop->bits, *rop->bits, *op1.bits);
   }
 }
 
-void slice(bv_t *rop, const bv_t op, const mpz_t i, const mpz_t len) {
-  // TODO
+void slice(bv_t *rop, const bv_t op, const mpz_t start_mpz, const mpz_t len_mpz)
+{
+  uint64_t start = mpz_get_ui(start_mpz);
+  uint64_t len = mpz_get_ui(len_mpz);
+
+  mpz_set_ui(*rop->bits, 0ul);
+  rop->len = len;
+
+  for (uint64_t i = 0; i < len; i++) {
+    if (mpz_tstbit(*op.bits, i + start)) mpz_setbit(*rop->bits, i);
+  }
 }
 
 uint64_t convert_uint64_t_of_bv_t(const bv_t op) {
@@ -321,6 +335,12 @@ void mask(bv_t *rop) {
   }
 }
 
+void truncate(bv_t *rop, const bv_t op, const mpz_t len) {
+  rop->len = mpz_get_ui(len);
+  mpz_set(*rop->bits, *op.bits);
+  mask(rop);
+}
+
 void and_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
   rop->len = op1.len;
   mpz_and(*rop->bits, *op1.bits, *op2.bits);
@@ -341,8 +361,11 @@ void xor_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
   mpz_xor(*rop->bits, *op1.bits, *op2.bits);
 }
 
+mpz_t eq_bits_test;
+
 bool eq_bits(const bv_t op1, const bv_t op2) {
-  return mpz_cmp(*op1.bits, *op2.bits) == 0;
+  mpz_xor(eq_bits_test, *op1.bits, *op2.bits);
+  return mpz_popcount(eq_bits_test) == 0;
 }
 
 void sail_uint(mpz_t *rop, const bv_t op) {
@@ -382,37 +405,122 @@ void sub_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) {
   mask(rop);
 }
 
-void get_slice_int(bv_t *rop, const mpz_t n, const mpz_t m, const mpz_t o) {
-  // TODO
+// Takes a slice of the (two's complement) binary representation of
+// integer n, starting at bit start, and of length len. With the
+// argument in the following order:
+//
+// get_slice_int(len, n, start)
+//
+// For example:
+//
+// get_slice_int(8, 1680, 4) =
+//
+//                    11           0
+//                    V            V
+// get_slice_int(8, 0b0110_1001_0000, 4) = 0b0110_1001
+//                    <-------^
+//                    (8 bit) 4
+//
+void get_slice_int(bv_t *rop, const mpz_t len_mpz, const mpz_t n, const mpz_t start_mpz)
+{
+  uint64_t start = mpz_get_ui(start_mpz);
+  uint64_t len = mpz_get_ui(len_mpz);
+
+  mpz_set_ui(*rop->bits, 0ul);
+  rop->len = len;
+
+  for (uint64_t i = 0; i < len; i++) {
+    if (mpz_tstbit(n, i + start)) mpz_setbit(*rop->bits, i);
+  }
 }
 
-void set_slice_int(mpz_t *rop, const mpz_t n, const mpz_t m, const mpz_t o, const bv_t op) {
-  // TODO
+// Set slice uses the same indexing scheme as get_slice_int, but it
+// puts a bitvector slice into an integer rather than returning it.
+void set_slice_int(mpz_t *rop,
+		   const mpz_t len_mpz,
+		   const mpz_t n,
+		   const mpz_t start_mpz,
+		   const bv_t slice)
+{
+  uint64_t start = mpz_get_ui(start_mpz);
+
+  mpz_set(*rop, n);
+
+  for (uint64_t i = 0; i < slice.len; i++) {
+    if (mpz_tstbit(*slice.bits, i)) {
+      mpz_setbit(*rop, i + start);
+    } else {
+      mpz_clrbit(*rop, i + start);
+    }
+  }
 }
 
-void vector_update_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n, const mpz_t m, const bv_t slice) {
-  // TODO
+void vector_update_subrange_bv_t(bv_t *rop,
+				 const bv_t op,
+				 const mpz_t n_mpz,
+				 const mpz_t m_mpz,
+				 const bv_t slice)
+{
+  uint64_t n = mpz_get_ui(n_mpz);
+  uint64_t m = mpz_get_ui(m_mpz);
+
+  mpz_set(*rop->bits, *op.bits);
+
+  for (uint64_t i = 0; i < n - (m - 1ul); i++) {
+    if (mpz_tstbit(*slice.bits, i)) {
+      mpz_setbit(*rop->bits, i + m);
+    } else {
+      mpz_clrbit(*rop->bits, i + m);
+    }
+  }
 }
 
-void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n, const mpz_t m) {
-  // TODO
+void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n_mpz, const mpz_t m_mpz)
+{
+  uint64_t n = mpz_get_ui(n_mpz);
+  uint64_t m = mpz_get_ui(m_mpz);
+
+  mpz_set_ui(*rop->bits, 0ul);
+  rop->len = n - (m - 1ul);
+
+  for (uint64_t i = 0; i < rop->len; i++) {
+    if (mpz_tstbit(*op.bits, i + m)) {
+      mpz_setbit(*rop->bits, i);
+    } else {
+      mpz_clrbit(*rop->bits, i);
+    }
+  }
 }
 
-int bitvector_access(const bv_t op, const mpz_t n) {
-  return 0; // TODO
+int bitvector_access(const bv_t op, const mpz_t n_mpz) {
+  uint64_t n = mpz_get_ui(n_mpz);
+  return mpz_tstbit(*op.bits, n);
 }
 
 void hex_slice (bv_t *rop, const sail_string hex, const mpz_t n, const mpz_t m) {
-  // TODO
+  fprintf(stderr, "hex_slice unimplemented");
+  exit(1);
 }
 
-void set_slice (bv_t *rop, const mpz_t len, const mpz_t slen, const bv_t op, const mpz_t i, const bv_t slice) {
-  // TODO
-}
+void set_slice (bv_t *rop,
+		const mpz_t len_mpz,
+		const mpz_t slen_mpz,
+		const bv_t op,
+		const mpz_t start_mpz,
+		const bv_t slice)
+{
+  uint64_t start = mpz_get_ui(start_mpz);
 
-unit print_bits(const sail_string str, const bv_t op) {
-  fputs(str, stdout);
-  gmp_printf("%d'0x%ZX\n", op.len, op.bits);
+  mpz_set(*rop->bits, *op.bits);
+  rop->len = op.len;
+
+  for (uint64_t i = 0; i < slice.len; i++) {
+    if (mpz_tstbit(*slice.bits, i)) {
+      mpz_setbit(*rop->bits, i + start);
+    } else {
+      mpz_clrbit(*rop->bits, i + start);
+    }
+  }
 }
 
 // ***** Real number implementation *****
@@ -425,10 +533,6 @@ typedef mpf_t real;
 
 #define FLOAT_PRECISION 255
 
-void setup_real(void) {
-  mpf_set_default_prec(FLOAT_PRECISION);
-}
-
 void init_real(real *rop) {
   mpf_init(*rop);
 }
@@ -528,9 +632,67 @@ void init_real_of_sail_string(real *rop, const sail_string op) {
 // ***** Memory *****
 
 unit write_ram(const mpz_t m, const mpz_t n, const bv_t x, const bv_t y, const bv_t data) {
-  return UNIT;
+  fprintf(stderr, "write_ram unimplemented");
+  exit(1);
+}
+
+void read_ram(bv_t *data, const mpz_t m, const mpz_t n, const bv_t x, const bv_t addr_bv) {
+  uint64_t addr = mpz_get_ui(*addr_bv.bits);
+  uint32_t instr;
+  switch (addr) {
+    // print_char
+  case 0x400110: instr = 0xd10043ffu; break;
+  case 0x400114: instr = 0x39003fe0u; break;
+  case 0x400118: instr = 0x39403fe0u; break;
+  case 0x40011c: instr = 0x580003e1u; break;
+  case 0x400120: instr = 0x39000020u; break;
+  case 0x400124: instr = 0xd503201fu; break;
+  case 0x400128: instr = 0x910043ffu; break;
+  case 0x40012c: instr = 0xd65f03c0u; break;
+    // _start
+  case 0x400130: instr = 0xa9be7bfdu; break;
+  case 0x400134: instr = 0x910003fdu; break;
+  case 0x400138: instr = 0x94000007u; break;
+  case 0x40013c: instr = 0xb9001fa0u; break;
+  case 0x400140: instr = 0x52800080u; break;
+  case 0x400144: instr = 0x97fffff3u; break;
+  case 0x400148: instr = 0xd503201fu; break;
+  case 0x40014c: instr = 0xa8c27bfdu; break;
+  case 0x400150: instr = 0xd65f03c0u; break;
+    // main
+  case 0x400154: instr = 0xd10043ffu; break;
+  case 0x400158: instr = 0xb9000fffu; break;
+  case 0x40015c: instr = 0xb9000bffu; break;
+  case 0x400160: instr = 0x14000007u; break;
+  case 0x400164: instr = 0xb9400fe0u; break;
+  case 0x400168: instr = 0x11000400u; break;
+  case 0x40016c: instr = 0xb9000fe0u; break;
+  case 0x400170: instr = 0xb9400be0u; break;
+  case 0x400174: instr = 0x11000400u; break;
+  case 0x400178: instr = 0xb9000be0u; break;
+  case 0x40017c: instr = 0xb9400be0u; break;
+  case 0x400180: instr = 0x710fa01fu; break;
+  case 0x400184: instr = 0x54ffff0du; break;
+  case 0x400188: instr = 0xb9400fe0u; break;
+  case 0x40018c: instr = 0x910043ffu; break;
+  case 0x400190: instr = 0xd65f03c0u; break;
+  case 0x400194: instr = 0x00000000u; break;
+  case 0x400198: instr = 0x13000000u; break;
+  case 0x40019c: instr = 0x00000000u; break;
+  }
+
+  mpz_set_ui(*data->bits, instr);
+  data->len = 32;
+  print_bits("instruction = ", *data);
+}
+
+// ***** Setup and cleanup functions for library code *****
+
+void setup_library(void) {
+  mpf_set_default_prec(FLOAT_PRECISION);
+  mpz_init(eq_bits_test);
 }
 
-void read_ram(bv_t *data, const mpz_t m, const mpz_t n, const bv_t x, const bv_t y) {
-  // TODO
+void cleanup_library(void) {
+  mpz_clear(eq_bits_test);
 }
diff --git a/test/c/short_circuit.expect b/test/c/short_circuit.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/short_circuit.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/short_circuit.sail b/test/c/short_circuit.sail
new file mode 100644
index 00000000..8289efa6
--- /dev/null
+++ b/test/c/short_circuit.sail
@@ -0,0 +1,22 @@
+
+$include <exception_basic.sail>
+$include <flow.sail>
+
+val print = "print_endline" : string -> unit
+
+val test : unit -> bool effect {escape}
+
+function test () = {
+  assert(false);
+  false
+}
+
+val main : unit -> unit effect {escape}
+
+function main () = {
+  if false & test() then {
+    print("unreachable");
+  } else {
+    print("ok");
+  }
+}
\ No newline at end of file