diff options
| author | Thomas Bauereiss | 2020-03-02 18:20:02 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-03-02 18:20:02 +0000 |
| commit | c81f2fbdeef670e8cbd6771ecd22ce1e64f2306b (patch) | |
| tree | dd64e4df97bc1a0e8edd9686c192d60549e7b189 /src | |
| parent | 306d4e2b195b6d28c136e33135dca2da5d0f122d (diff) | |
Add arith_shiftr to SMT and interpreter
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 1 | ||||
| -rw-r--r-- | src/value.ml | 5 |
2 files changed, 6 insertions, 0 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index c4e8576c..569005a5 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1208,6 +1208,7 @@ let smt_builtin ctx name args ret_ctyp = | "sail_truncateLSB", [v1; v2], _ -> builtin_sail_truncateLSB ctx v1 v2 ret_ctyp | "shiftl", [v1; v2], _ -> builtin_shift "bvshl" ctx v1 v2 ret_ctyp | "shiftr", [v1; v2], _ -> builtin_shift "bvlshr" ctx v1 v2 ret_ctyp + | "arith_shiftr", [v1; v2], _ -> builtin_shift "bvashr" ctx v1 v2 ret_ctyp | "and_bits", [v1; v2], _ -> builtin_and_bits ctx v1 v2 ret_ctyp | "or_bits", [v1; v2], _ -> builtin_or_bits ctx v1 v2 ret_ctyp | "xor_bits", [v1; v2], _ -> builtin_xor_bits ctx v1 v2 ret_ctyp diff --git a/src/value.ml b/src/value.ml index f94ae176..11cda94b 100644 --- a/src/value.ml +++ b/src/value.ml @@ -457,6 +457,10 @@ let value_shiftr = function | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2)) | _ -> failwith "value shiftr" +let value_arith_shiftr = function + | [v1; v2] -> mk_vector (Sail_lib.arith_shiftr (coerce_bv v1, coerce_int v2)) + | _ -> failwith "value arith_shiftr" + let value_shift_bits_left = function | [v1; v2] -> mk_vector (Sail_lib.shift_bits_left (coerce_bv v1, coerce_bv v2)) | _ -> failwith "value shift_bits_left" @@ -697,6 +701,7 @@ let primops = ref ("ones", value_ones); ("shiftr", value_shiftr); ("shiftl", value_shiftl); + ("arith_shiftr", value_shiftr); ("shift_bits_left", value_shift_bits_left); ("shift_bits_right", value_shift_bits_right); ("add_int", value_add_int); |