SV: Implement some more primitives so RV model builds

lib/arith.sail

@@ -140,22 +140,16 @@ overload shr_int = {_shr32, _shr_int, _shr_int_general}
 
 /*! Truncating division (rounds towards zero) */
 val tdiv_int = pure {
-  ocaml: "tdiv_int",
-  interpreter: "tdiv_int",
-  lem: "tdiv_int",
-  c: "tdiv_int",
   coq: "Z.quot",
-  lean: "Int.tdiv"
+  lean: "Int.tdiv",
+  _: "tdiv_int"
 } : (int, int) -> int
 
 /*! Remainder for truncating division (has sign of dividend) */
 val _tmod_int = pure {
-  ocaml: "tmod_int",
-  interpreter: "tmod_int",
-  lem: "tmod_int",
   coq: "Z.rem",
   lean: "Int.tmod",
-  c: "tmod_int"
+  _: "tmod_int"
 } : (int, int) -> int
 
 /*! If we know the second argument is positive, we know the result is positive */

lib/smt.sail

@@ -54,24 +54,24 @@ val ediv_int = pure {
   ocaml: "quotient",
   interpreter: "quotient",
   lem: "integerDiv",
-  c: "ediv_int",
-  coq: "ZEuclid.div"
+  coq: "ZEuclid.div",
+  _: "ediv_int"
 } : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
 
 val emod_int = pure {
   ocaml: "modulus",
   interpreter: "modulus",
   lem: "integerMod",
-  c: "emod_int",
-  coq: "ZEuclid.modulo"
+  coq: "ZEuclid.modulo",
+  _: "emod_int"
 } : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
 
 val abs_int_atom = pure {
   ocaml: "abs_int",
   interpreter: "abs_int",
   lem: "integerAbs",
-  c: "abs_int",
-  coq: "Z.abs"
+  coq: "Z.abs",
+  _: "abs_int"
 } : forall 'n. int('n) -> int(abs('n))
 
 overload abs_int = {abs_int_atom}

lib/sv/sail_modules.sv

@@ -99,6 +99,7 @@ typedef sail_write sail_memory_writes [$];
 
 function automatic sail_bits emulator_read_mem(logic [63:0] addrsize, sail_bits addr, sail_int n);
    logic [63:0] paddr;
+   /* verilator lint_off UNOPTFLAT */
    logic [SAIL_BITS_WIDTH-1:0] buffer;
    sail_int i;
 
@@ -159,7 +160,10 @@ module emulator_write_tag
    output sail_unit          ret,
    output sail_memory_writes out_writes
    );
-endmodule
+endmodule // emulator_write_tag
 
+function automatic string sail_string_of_bits(sail_bits bv);
+   return "";
+endfunction // sail_string_of_bits
 
 `endif

src/lib/smt_exp.ml

@@ -187,9 +187,12 @@ let bvsub x y = Fn ("bvsub", [x; y])
 let bvmul x y = Fn ("bvmul", [x; y])
 let bvudiv x y = Fn ("bvudiv", [x; y])
 let bvurem x y = Fn ("bvurem", [x; y])
+let bvsdiv x y = Fn ("bvsdiv", [x; y])
+let bvsrem x y = Fn ("bvsrem", [x; y])
 let bvshl x y = Fn ("bvshl", [x; y])
 let bvlshr x y = Fn ("bvlshr", [x; y])
 let bvult x y = Fn ("bvult", [x; y])
+let bvslt x y = Fn ("bvslt", [x; y])
 
 let bvzero n = Bitvec_lit (Sail2_operators_bitlists.zeros (Big_int.of_int n))
 

src/lib/smt_gen.ml

@@ -447,10 +447,10 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
             else Extract (esz - 1, 0, smt)
           )
 
-  let builtin_arith fn big_int_fn padding v1 v2 ret_ctyp =
+  let builtin_arith ?(fold = true) fn big_int_fn padding v1 v2 ret_ctyp =
     match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with
     | _, _, CT_constant c -> return (bvint (required_width c) c)
-    | CT_constant c1, CT_constant c2, _ -> return (bvint (int_size ret_ctyp) (big_int_fn c1 c2))
+    | CT_constant c1, CT_constant c2, _ when fold -> return (bvint (int_size ret_ctyp) (big_int_fn c1 c2))
     | ctyp1, ctyp2, _ ->
         (* To detect arithmetic overflow we can expand the input
            bitvectors to some size determined by a padding function,
@@ -463,6 +463,40 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
         let* padded_smt2 = signed_size ~into:(padding ret_sz) ~from:(int_size ctyp2) smt2 in
         signed_size ~into:ret_sz ~from:(padding ret_sz) (Fn (fn, [padded_smt1; padded_smt2]))
 
+  let builtin_ediv_int v1 v2 ret_ctyp =
+    match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with
+    | _, _, CT_constant c -> return (bvint (required_width c) c)
+    | ctyp1, ctyp2, _ ->
+        let ret_sz = int_size ret_ctyp in
+        let* smt1 = bind (smt_cval v1) (signed_size ~into:ret_sz ~from:(int_size ctyp1)) in
+        let* smt2 = bind (smt_cval v2) (signed_size ~into:ret_sz ~from:(int_size ctyp2)) in
+        let negative_dividend = bvslt smt1 (bvzero ret_sz) in
+        let negative_divisor = bvslt smt2 (bvzero ret_sz) in
+        return
+          (Ite
+             ( smt_conj [negative_dividend; negative_divisor],
+               bvadd (bvsdiv (bvsub (bvneg smt1) (bvone ret_sz)) (bvneg smt2)) (bvone ret_sz),
+               Ite (negative_dividend, bvsub (bvsdiv (bvadd smt1 (bvone ret_sz)) smt2) (bvone ret_sz), bvsdiv smt1 smt2)
+             )
+          )
+
+  let builtin_emod_int v1 v2 ret_ctyp =
+    match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with
+    | _, _, CT_constant c -> return (bvint (required_width c) c)
+    | ctyp1, ctyp2, _ ->
+        let ret_sz = int_size ret_ctyp in
+        let* smt1 = bind (smt_cval v1) (signed_size ~into:ret_sz ~from:(int_size ctyp1)) in
+        let* smt2 = bind (smt_cval v2) (signed_size ~into:ret_sz ~from:(int_size ctyp2)) in
+        let negative_dividend = bvslt smt1 (bvzero ret_sz) in
+        let negative_divisor = bvslt smt2 (bvzero ret_sz) in
+        return
+          (Ite
+             ( smt_conj [negative_dividend; negative_divisor],
+               bvadd (bvsrem (bvsub (bvneg smt1) (bvone ret_sz)) (bvneg smt2)) (bvone ret_sz),
+               Ite (negative_dividend, bvsub (bvsrem (bvadd smt1 (bvone ret_sz)) smt2) (bvone ret_sz), bvsrem smt1 smt2)
+             )
+          )
+
   let builtin_add_int = builtin_arith "bvadd" Big_int.add (fun x -> x + 1)
   let builtin_sub_int = builtin_arith "bvsub" Big_int.sub (fun x -> x + 1)
   let builtin_mult_int = builtin_arith "bvmul" Big_int.mul (fun x -> x * 2)
@@ -500,8 +534,8 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
   let builtin_max_int = builtin_choose_int "bvsgt" max
   let builtin_min_int = builtin_choose_int "bvslt" min
 
-  let builtin_tdiv_int = builtin_arith "bvsdiv" Big_int.div (fun x -> x)
-  let builtin_tmod_int = builtin_arith "bvsrem" Big_int.div (fun x -> x)
+  let builtin_tdiv_int = builtin_arith ~fold:false "bvsdiv" Sail2_values.tdiv_int (fun x -> x)
+  let builtin_tmod_int = builtin_arith ~fold:false "bvsrem" Sail2_values.tmod_int (fun x -> x)
 
   let int_comparison fn big_int_fn v1 v2 =
     let* sv1 = smt_cval v1 in
@@ -603,6 +637,19 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
         return (Fn ("Bits", [Fn ("len", [bv]); shifted]))
     | _ -> builtin_type_error shiftop [vbits; vshift] (Some ret_ctyp)
 
+  let builtin_shift_by_bits shiftop vbits vshift ret_ctyp =
+    match cval_ctyp vbits with
+    | CT_fbits n ->
+        let* bv = smt_cval vbits in
+        let* shift = bind (smt_cval vshift) (smt_conversion ~into:(CT_fbits n) ~from:(cval_ctyp vshift)) in
+        return (Fn (shiftop, [bv; shift]))
+    | CT_lbits ->
+        let* bv = smt_cval vbits in
+        let* shift = bind (smt_cval vshift) (smt_conversion ~into:(CT_fbits lbits_size) ~from:(cval_ctyp vshift)) in
+        let shifted = Fn (shiftop, [Fn ("contents", [bv]); shift]) in
+        return (Fn ("Bits", [Fn ("len", [bv]); shifted]))
+    | _ -> builtin_type_error shiftop [vbits; vshift] (Some ret_ctyp)
+
   let builtin_slice v1 v2 v3 ret_ctyp =
     match (cval_ctyp v1, cval_ctyp v2, cval_ctyp v3, ret_ctyp) with
     | CT_lbits, CT_constant start, CT_constant len, CT_fbits _ ->
@@ -1399,6 +1446,8 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
     | "min_int" -> binary_primop builtin_min_int
     | "tdiv_int" -> binary_primop builtin_tdiv_int
     | "tmod_int" -> binary_primop builtin_tmod_int
+    | "ediv_int" -> binary_primop builtin_ediv_int
+    | "emod_int" -> binary_primop builtin_emod_int
     | "pow2" -> unary_primop builtin_pow2
     | "zeros" -> unary_primop builtin_zeros
     | "ones" -> unary_primop builtin_ones
@@ -1422,6 +1471,8 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
     | "shiftl" -> binary_primop (builtin_shift "bvshl")
     | "shiftr" -> binary_primop (builtin_shift "bvlshr")
     | "arith_shiftr" -> binary_primop (builtin_shift "bvashr")
+    | "shift_bits_left" -> binary_primop (builtin_shift_by_bits "bvshl")
+    | "shift_bits_right" -> binary_primop (builtin_shift_by_bits "bvlshr")
     | "and_bits" -> binary_primop (builtin_bitwise "bvand")
     | "or_bits" -> binary_primop (builtin_bitwise "bvor")
     | "xor_bits" -> binary_primop (builtin_bitwise "bvxor")

src/sail_sv_backend/jib_sv.ml

@@ -927,8 +927,12 @@ module Make (Config : CONFIG) = struct
     | Fn ("bvshl", [x; y]) -> opt_parens (separate space [pp_smt_parens x; string "<<"; sv_signed (pp_smt y)])
     | Fn ("bvlshr", [x; y]) -> opt_parens (separate space [pp_smt_parens x; string ">>"; sv_signed (pp_smt y)])
     | Fn ("bvashr", [x; y]) -> opt_parens (separate space [pp_smt_parens x; string ">>>"; sv_signed (pp_smt y)])
-    | Fn ("bvsdiv", [x; y]) -> opt_parens (separate space [pp_smt_parens x; string "/"; pp_smt_parens y])
-    | Fn ("bvsmod", [x; y]) -> opt_parens (separate space [pp_smt_parens x; string "%"; pp_smt_parens y])
+    (* SV LRM: The integer division shall truncate any fractional part toward zero
+       SMTLIB bvsdiv: Truncation is towards zero (could not find official reference, but z3 and cvc5 are consistent). *)
+    | Fn ("bvsdiv", [x; y]) -> opt_parens (separate space [sv_signed (pp_smt x); string "/"; sv_signed (pp_smt y)])
+    (* SV LRM: The result of a modulus operation shall take the sign of the first operand (dividend).
+       SMTLIB bvsrem: Sign follows dividend *)
+    | Fn ("bvsrem", [x; y]) -> opt_parens (separate space [sv_signed (pp_smt x); string "%"; sv_signed (pp_smt y)])
     | Fn ("select", [x; i]) -> pp_smt_parens x ^^ lbracket ^^ pp_smt i ^^ rbracket
     | Fn ("contents", [Var v]) -> pp_name v ^^ dot ^^ string "bits"
     | Fn ("contents", [x]) -> string "sail_bits_value" ^^ parens (pp_smt x)

test/c/ediv.expect

@@ -0,0 +1 @@
+ediv ok

test/c/ediv.sail

@@ -0,0 +1,27 @@
+default Order dec
+
+$include <arith.sail>
+$include <smt.sail>
+$include <string.sail>
+
+function main (() : unit) -> unit = {
+  assert(ediv_int(7, 5) == 1);
+  assert(ediv_int(7, -5) == -1);
+  assert(ediv_int(-7, 5) == -2);
+  assert(ediv_int(-7, -5) == 2);
+  assert(ediv_int(12, 3) == 4);
+  assert(ediv_int(12, -3) == -4);
+  assert(ediv_int(-12, 3) == -4);
+  assert(ediv_int(-12, -3) == 4);
+
+  assert(emod_int(7, 5) == 2);
+  assert(emod_int(7, -5) == 2);
+  assert(emod_int(-7, 5) == 3);
+  assert(emod_int(-7, -5) == 3);
+  assert(emod_int(12, 3) == 0);
+  assert(emod_int(12, -3) == 0);
+  assert(emod_int(-12, 3) == 0);
+  assert(emod_int(-12, -3) == 0);
+
+  print_endline("ediv ok")
+}

test/c/ediv_from_tdiv.expect

@@ -0,0 +1 @@
+ediv from tdiv ok

test/c/ediv_from_tdiv.sail

@@ -0,0 +1,43 @@
+default Order dec
+
+$include <arith.sail>
+$include <smt.sail>
+$include <string.sail>
+
+val my_ediv_int : (int, int) -> int
+
+function my_ediv_int(n, m) = {
+  if n < 0 & m < 0 then {
+    tdiv_int(abs_int_plain(n) - 1, abs_int_plain(m)) + 1
+  } else if n < 0 then {
+    tdiv_int(n + 1, m) - 1
+  } else {
+    tdiv_int(n, m)
+  }
+}
+
+val my_emod_int : (int, int) -> int
+
+function my_emod_int(n, m) = {
+  n - (m * my_ediv_int(n, m))
+}
+
+function main (() : unit) -> unit = {
+  foreach (n from -100 to 100) {
+    foreach (m from -100 to 100) {
+      if m != 0 then {
+        let d = ediv_int(n, m);
+        let r = emod_int(n, m);
+
+        let my_d = my_ediv_int(n, m);
+        let my_r = my_emod_int(n, m);
+
+        assert(d == my_d);
+        assert(r == my_r);
+        assert(n == m * d + r);
+      }
+    }
+  };
+
+  print_endline("ediv from tdiv ok")
+}

test/c/fdiv.expect

@@ -0,0 +1 @@
+fdiv ok

test/c/fdiv.sail

@@ -0,0 +1,26 @@
+default Order dec
+
+$include <arith.sail>
+$include <string.sail>
+
+function main (() : unit) -> unit = {
+  assert(fdiv_int(7, 5) == 1);
+  assert(fdiv_int(7, -5) == -2);
+  assert(fdiv_int(-7, 5) == -2);
+  assert(fdiv_int(-7, -5) == 1);
+  assert(fdiv_int(12, 3) == 4);
+  assert(fdiv_int(12, -3) == -4);
+  assert(fdiv_int(-12, 3) == -4);
+  assert(fdiv_int(-12, -3) == 4);
+
+  assert(fmod_int(7, 5) == 2);
+  assert(fmod_int(7, -5) == -3);
+  assert(fmod_int(-7, 5) == 3);
+  assert(fmod_int(-7, -5) == -2);
+  assert(fmod_int(12, 3) == 0);
+  assert(fmod_int(12, -3) == 0);
+  assert(fmod_int(-12, 3) == 0);
+  assert(fmod_int(-12, -3) == 0);
+
+  print_endline("fdiv ok")
+}

test/c/tdiv.expect

@@ -0,0 +1 @@
+tdiv ok

test/c/tdiv.sail

@@ -0,0 +1,26 @@
+default Order dec
+
+$include <arith.sail>
+$include <string.sail>
+
+function main (() : unit) -> unit = {
+  assert(tdiv_int(7, 5) == 1);
+  assert(tdiv_int(7, -5) == -1);
+  assert(tdiv_int(-7, 5) == -1);
+  assert(tdiv_int(-7, -5) == 1);
+  assert(tdiv_int(12, 3) == 4);
+  assert(tdiv_int(12, -3) == -4);
+  assert(tdiv_int(-12, 3) == -4);
+  assert(tdiv_int(-12, -3) == 4);
+
+  assert(tmod_int(7, 5) == 2);
+  assert(tmod_int(7, -5) == 2);
+  assert(tmod_int(-7, 5) == -2);
+  assert(tmod_int(-7, -5) == -2);
+  assert(tmod_int(12, 3) == 0);
+  assert(tmod_int(12, -3) == 0);
+  assert(tmod_int(-12, 3) == 0);
+  assert(tmod_int(-12, -3) == 0);
+
+  print_endline("tdiv ok")
+}

test/sv/run_tests.py

@@ -30,6 +30,7 @@
     'lib_hex_bits_signed', # bitvector parsing
     'nexp_simp_euclidian', # division
     'concurrency_interface', # memory
+    'ediv_from_tdiv', # loops
 }
 
 print("Sail is {}".format(sail))