Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

2 files changed, 65 insertions, 3 deletions

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 2b144d35..2b2234b5 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -1481,6 +1481,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
        | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)"
        | "undefined_bit", _ -> "UNDEFINED(fbits)"
        | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
+       | "undefined_list", _ -> Printf.sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp)
        | fname, _ -> fname
      in
      if fname = "reg_deref" then
@@ -1844,6 +1845,9 @@ let codegen_list_clear id ctyp =
   ^^ string "  sail_free(*rop);"
   ^^ string "}"
 
+let codegen_list_recreate id =
+  string (Printf.sprintf "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id))
+
 let codegen_list_set id ctyp =
   string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
   ^^ string "  if (op == NULL) { *rop = NULL; return; };\n"
@@ -1879,6 +1883,20 @@ let codegen_pick id ctyp =
   else
     string (Printf.sprintf "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp))
 
+let codegen_list_equal id ctyp =
+  let open Printf in
+  ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id)
+  ^^ ksprintf string "  if (op1 == NULL && op2 == NULL) { return true; };\n"
+  ^^ ksprintf string "  if (op1 == NULL || op2 == NULL) { return false; };\n"
+  ^^ ksprintf string "  return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id)
+  ^^ string "}"
+
+let codegen_list_undefined id ctyp =
+  let open Printf in
+  ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)
+  ^^ ksprintf string "  *rop = NULL;\n"
+  ^^ string "}"
+
 let codegen_list ctx ctyp =
   let id = mk_id (string_of_ctyp (CT_list ctyp)) in
   if IdSet.mem id !generated then
@@ -1889,9 +1907,12 @@ let codegen_list ctx ctyp =
       codegen_node id ctyp ^^ twice hardline
       ^^ codegen_list_init id ^^ twice hardline
       ^^ codegen_list_clear id ctyp ^^ twice hardline
+      ^^ codegen_list_recreate id ^^ twice hardline
       ^^ codegen_list_set id ctyp ^^ twice hardline
       ^^ codegen_cons id ctyp ^^ twice hardline
       ^^ codegen_pick id ctyp ^^ twice hardline
+      ^^ codegen_list_equal id ctyp ^^ twice hardline
+      ^^ codegen_list_undefined id ctyp ^^ twice hardline
     end
 
 (* Generate functions for working with non-bit vectors of some specific type. *)
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 81b876a4..c4e8576c 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -283,8 +283,14 @@ let smt_conversion ctx from_ctyp to_ctyp x =
      force_size ctx ctx.lint_size sz x
   | CT_lint, CT_fint sz ->
      force_size ctx sz ctx.lint_size x
+  | CT_lint, CT_fbits (n, _) ->
+     force_size ctx n ctx.lint_size x
+  | CT_lint, CT_lbits _ ->
+     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int ctx.lint_size); force_size ctx (lbits_size ctx) ctx.lint_size x])
   | CT_lbits _, CT_fbits (n, _) ->
      unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x]))
+  | CT_fbits (n, _), CT_fbits (m, _) ->
+     unsigned_size ctx m n x
   | CT_fbits (n, _), CT_lbits _ ->
      Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); unsigned_size ctx (lbits_size ctx) n x])
 
@@ -580,6 +586,8 @@ let bvmask ctx len =
   let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in
   bvnot (bvshl all_ones shift)
 
+let fbits_mask ctx n len = bvnot (bvshl (bvones n) len)
+
 let builtin_eq_bits ctx v1 v2 =
   match cval_ctyp v1, cval_ctyp v2 with
   | CT_fbits (n, _), CT_fbits (m, _) ->
@@ -796,9 +804,17 @@ let builtin_vector_subrange ctx vec i j ret_ctyp =
      Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [smt_cval ctx vec]))
 
   | CT_fbits (n, _), i_ctyp, CT_constant j, CT_lbits _ when Big_int.equal j Big_int.zero ->
-     let len = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in
+     let i' = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in
+     let len = bvadd i' (bvint ctx.lbits_index (Big_int.of_int 1)) in
      Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; unsigned_size ctx (lbits_size ctx) n (smt_cval ctx vec)])])
 
+  | CT_fbits (n, b), i_ctyp, j_ctyp, ret_ctyp ->
+     let i' = force_size ctx n (int_size ctx i_ctyp) (smt_cval ctx i) in
+     let j' = force_size ctx n (int_size ctx j_ctyp) (smt_cval ctx j) in
+     let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in
+     let vec' = bvand (bvlshr (smt_cval ctx vec) j') (fbits_mask ctx n len) in
+     smt_conversion ctx (CT_fbits (n, b)) ret_ctyp vec'
+
   | _ -> builtin_type_error ctx "vector_subrange" [vec; i; j] (Some ret_ctyp)
 
 let builtin_vector_access ctx vec i ret_ctyp =
@@ -844,17 +860,31 @@ let builtin_vector_update ctx vec i x ret_ctyp =
 
 let builtin_vector_update_subrange ctx vec i j x ret_ctyp =
   match cval_ctyp vec, cval_ctyp i, cval_ctyp j, cval_ctyp x, ret_ctyp with
-  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j >= 0 ->
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j > 0 ->
      assert (n = m);
      let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in
      let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in
      Fn ("concat", [top; Fn ("concat", [smt_cval ctx x; bot])])
 
-  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j >= 0 ->
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j > 0 ->
      assert (n = m);
      let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in
      Fn ("concat", [smt_cval ctx x; bot])
 
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j = 0 ->
+     assert (n = m);
+     let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in
+     Fn ("concat", [top; smt_cval ctx x])
+
+  | CT_fbits (n, b), ctyp_i, ctyp_j, ctyp_x, CT_fbits (m, _) ->
+     assert (n = m);
+     let i' = force_size ctx n (int_size ctx ctyp_i) (smt_cval ctx i) in
+     let j' = force_size ctx n (int_size ctx ctyp_j) (smt_cval ctx j) in
+     let x' = smt_conversion ctx ctyp_x (CT_fbits (n, b)) (smt_cval ctx x) in
+     let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in
+     let mask = bvshl (fbits_mask ctx n len) j' in
+     bvor (bvand (smt_cval ctx vec) (bvnot mask)) (bvand (bvshl x' j') mask)
+
   | _ -> builtin_type_error ctx "vector_update_subrange" [vec; i; j; x] (Some ret_ctyp)
 
 let builtin_unsigned ctx v ret_ctyp =
@@ -873,6 +903,10 @@ let builtin_unsigned ctx v ret_ctyp =
   | CT_lbits _, CT_lint ->
      Extract (ctx.lint_size - 1, 0, Fn ("contents", [smt_cval ctx v]))
 
+  | CT_lbits _, CT_fint m ->
+     let smt = Fn ("contents", [smt_cval ctx v]) in
+     force_size ctx m (lbits_size ctx) smt
+
   | ctyp, _ -> builtin_type_error ctx "unsigned" [v] (Some ret_ctyp)
 
 let builtin_signed ctx v ret_ctyp =
@@ -1021,6 +1055,13 @@ let builtin_get_slice_int ctx v1 v2 v3 ret_ctyp =
      let contents = unsigned_size ~checked:false ctx (lbits_size ctx) ctx.lint_size (smt_cval ctx v2) in
      Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; contents])])
 
+  | CT_lint, ctyp2, ctyp3, ret_ctyp ->
+     let len = Extract (ctx.lbits_index - 1, 0, smt_cval ctx v1) in
+     let smt2 = force_size ctx (lbits_size ctx) (int_size ctx ctyp2) (smt_cval ctx v2) in
+     let smt3 = force_size ctx (lbits_size ctx) (int_size ctx ctyp3) (smt_cval ctx v3) in
+     let result = bvand (bvmask ctx len) (bvlshr smt2 smt3) in
+     smt_conversion ctx CT_lint ret_ctyp result
+
   | _ -> builtin_type_error ctx "get_slice_int" [v1; v2; v3] (Some ret_ctyp)
 
 let builtin_count_leading_zeros ctx v ret_ctyp =