From a8987e69a2d3a86f2912e5c23bb0a2a91ca1981a Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 13 Mar 2020 13:54:37 +0000
Subject: SMT fixes for some corner cases of vector updates

---
 src/jib/jib_compile.ml |  2 +-
 src/jib/jib_smt.ml     | 18 ++++++++++++++++--
 2 files changed, 17 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 4282ae30..34477967 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -366,7 +366,7 @@ let rec compile_aval l ctx = function
           setup
           @ [iextern (CL_id (gs, ctyp))
                      (mk_id "update_fbits", [])
-                     [V_id (gs, ctyp); V_lit (VL_int (Big_int.of_int i), CT_fint 64); cval]]
+                     [V_id (gs, ctyp); V_lit (VL_int (Big_int.of_int i), CT_constant (Big_int.of_int i)); cval]]
           @ cleanup
      in
      [idecl ctyp gs;
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 569005a5..47f6ee49 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -843,14 +843,17 @@ let builtin_vector_update ctx vec i x ret_ctyp =
      let bot = Extract (Big_int.to_int i - 1, 0, smt_cval ctx vec) in
      Fn ("concat", [top; Fn ("concat", [smt_cval ctx x; bot])])
 
-  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when n - 1 = Big_int.to_int i ->
+  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int i > 0 ->
      let bot = Extract (Big_int.to_int i - 1, 0, smt_cval ctx vec) in
      Fn ("concat", [smt_cval ctx x; bot])
 
-  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when Big_int.to_int i = 0 ->
+  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int i = 0 ->
      let top = Extract (n - 1, 1, smt_cval ctx vec) in
      Fn ("concat", [top; smt_cval ctx x])
 
+  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when n - 1 = 0 && Big_int.to_int i = 0 ->
+     smt_cval ctx x
+
   | CT_vector _, CT_constant i, ctyp, CT_vector _ ->
      Fn ("store", [smt_cval ctx vec; bvint !vector_index i; smt_cval ctx x])
   | CT_vector _, index_ctyp, _, CT_vector _ ->
@@ -876,6 +879,9 @@ let builtin_vector_update_subrange ctx vec i j x ret_ctyp =
      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, _), 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 ->
+     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
@@ -1842,6 +1848,14 @@ let smt_instr ctx =
        | _ ->
           Reporting.unreachable l __POS__ "Bad arguments for internal_vector_update"
        end
+     else if (string_of_id (fst function_id) = "update_fbits"
+              || string_of_id (fst function_id) = "update_lbits") && extern then
+       begin match args with
+       | [vec; i; x] ->
+          [define_const ctx id ret_ctyp (builtin_vector_update ctx vec i x ret_ctyp)]
+       | _ ->
+          Reporting.unreachable l __POS__ "Bad arguments for update_{f,l}bits"
+       end
      else if string_of_id (fst function_id) = "sail_assume" then
        begin match args with
        | [assumption] ->
-- 
cgit v1.2.3