diff options
| author | Thomas Bauereiss | 2020-03-13 13:54:37 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-03-13 14:00:18 +0000 |
| commit | a8987e69a2d3a86f2912e5c23bb0a2a91ca1981a (patch) | |
| tree | bfbe52ca31d5fb3781cc81475bd5f5a83da37471 /src | |
| parent | 8359701a67e2e2fd1026ef958d1395807a93489c (diff) | |
SMT fixes for some corner cases of vector updates
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_compile.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 18 |
2 files changed, 17 insertions, 3 deletions
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] -> |