SV: Various improvements

Subsets of primitives can be linked with DPI-C, e.g.
just the memory functions in the library

Fix for pow2 with fixed-width integers

Allowing passing CFLAGS and LDFLAGS options to verilator

Option for linking Sail runtime with generated verilator emulator

editors/sail-mode.el

@@ -34,7 +34,7 @@
   '("val" "outcome" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" "by"
     "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect"
     "overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from"
-    "pure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" "private"
+    "pure" "impure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" "private"
     "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
     "mapping" "where" "with" "implicit" "instantiation" "impl" "forwards" "backwards"))
 

lib/sv/sail_modules.sv

@@ -37,7 +37,7 @@ module print_endline
       out_sail_stdout = {in_sail_stdout, in_str, "\n"};
       out_return = SAIL_UNIT;
    end
-endmodule // print_endline
+endmodule
 
 function automatic bit valid_hex_bits(int n, string hex);
    int  len = hex.len();
@@ -72,23 +72,29 @@ function automatic bit valid_hex_bits(int n, string hex);
    end;
 
    return 1'h1;
-endfunction // valid_hex_bits
+endfunction
 
 function automatic string string_take(string str, int n);
    return str.substr(0, n - 1);
-endfunction // string_take
+endfunction
 
 function automatic string string_drop(string str, int n);
    return str.substr(n, str.len() - 1);
-endfunction // string_drop
+endfunction
 
 function automatic int string_length(string str);
    return str.len();
-endfunction // string_length
+endfunction
+
+`ifdef SAIL_DPI_MEMORY
+import "DPI-C" function bit[7:0] sail_read_byte(logic [63:0] addr);
 
+import "DPI-C" function bit sail_read_tag(logic [63:0] addr);
+`else
 logic [7:0] sail_memory [logic [63:0]];
 
 bit sail_tag_memory [logic [63:0]];
+`endif
 
 typedef struct {
    logic [63:0] paddr;
@@ -99,15 +105,17 @@ 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;
+   logic [SAIL_INDEX_WIDTH-2:0] i;
 
    paddr = addr.bits[63:0];
 
-   for (i = n; i > 0; i = i - 1) begin
-      buffer = buffer << 8;
-      buffer[7:0] = sail_memory[paddr + (i[63:0] - 1)];
+   for (i = n[SAIL_INDEX_WIDTH-2:0]; i > 0; i = i - 1) begin
+`ifdef SAIL_DPI_MEMORY
+      buffer[7 + (i * 8) -: 8] = sail_read_byte(paddr + (64'(i) - 1));
+`else
+      buffer[7 + (i * 8) -: 8] = sail_memory[paddr + (64'(i) - 1)];
+`endif
    end
 
    return '{n[SAIL_INDEX_WIDTH-1:0] * 8, buffer};
@@ -124,10 +132,14 @@ endfunction
 function automatic bit emulator_read_tag(logic [63:0] addrsize, sail_bits addr);
    logic [63:0] paddr;
    paddr = addr.bits[63:0];
+`ifdef SAIL_DPI_MEMORY
+   return sail_read_tag(paddr);
+`else
    if (sail_tag_memory.exists(paddr) == 1)
      return sail_tag_memory[paddr];
    else
      return 1'b0;
+`endif
 endfunction
 
 module emulator_write_mem
@@ -160,10 +172,10 @@ module emulator_write_tag
    output sail_unit          ret,
    output sail_memory_writes out_writes
    );
-endmodule // emulator_write_tag
+endmodule
 
 function automatic string sail_string_of_bits(sail_bits bv);
    return "";
-endfunction // sail_string_of_bits
+endfunction
 
 `endif

src/lib/mappings.ml

@@ -75,9 +75,40 @@
     }
     ]}
 
-   which is quite complicated. The [$[mapping_match]] attribute
-   ensures the type checker can re-check the mapping despite
-   the added option type. *)
+    which is quite complicated. The [$[mapping_match]] attribute
+    ensures the type checker can re-check the mapping despite
+    the added option type.
+
+    There are a few constraints that make this rewrite as tricky looking as it is:
+
+    - We don't want to duplicate any expression (`<expr1>` and `<expr2>`).
+    - We can't change the evaluation order, as this might change the
+      observable side effects of the expression. This includes the order
+      in which we evaluate `mapping_forwards` relative to all the other
+      expressions.
+    - The scope of all pattern bindings should be preserved.
+    - The match can be embedded in any context (so we can't use `return`).
+    - Mappings can be nested e.g. `m1(m2(m3(<pattern>)))`.
+
+    If the mapping match is in a return position we can instead rewrite to
+
+    {@sail[
+    let y = x in {
+      $[complete] match y {
+        <pat> => return <expr1>,
+        z if mapping_forwards_matches(z) => $[complete] match mapping_forwards(z) {
+          A => return <expr2>,
+          _ => (),
+        },
+        _ => (),
+      };
+      $[<completeness>] match y {
+        <rest>
+      }
+    }
+    ]}
+
+    which avoids the nested match statements and option type. *)
 
 open Ast
 open Ast_util
@@ -175,23 +206,29 @@ let name_gen prefix =
   in
   fresh
 
-(* Take a arm like "<pat> => <exp>" and turn it into "<pat> => Some(<exp>)" *)
-let some_arm = function
-  | Pat_aux (Pat_exp (pat, exp), annot) -> Pat_aux (Pat_exp (pat, mk_exp (E_app (mk_id "Some", [exp]))), annot)
-  | Pat_aux (Pat_when (pat, guard, exp), annot) ->
-      Pat_aux (Pat_when (pat, guard, mk_exp (E_app (mk_id "Some", [exp]))), annot)
+let wrap_some ~return_position exp =
+  if return_position then mk_exp (E_return exp) else mk_exp (E_app (mk_id "Some", [exp]))
 
-let wildcard_none = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit]))))
+(* Take a arm like "<pat> => <exp>" and turn it into "<pat> => Some(<exp>)", or
+   "<pat> => return <exp>" when in return position. *)
+let some_arm ~return_position = function
+  | Pat_aux (Pat_exp (pat, exp), annot) -> Pat_aux (Pat_exp (pat, wrap_some ~return_position exp), annot)
+  | Pat_aux (Pat_when (pat, guard, exp), annot) -> Pat_aux (Pat_when (pat, guard, wrap_some ~return_position exp), annot)
+
+(* Create an arm like "_ => None()" or "_ => ()" (when in return position) *)
+let wildcard_arm ~return_position () =
+  if return_position then mk_pexp (Pat_exp (mk_pat P_wild, mk_lit_exp L_unit))
+  else mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit]))))
 
 let unwrap_some =
   mk_pexp (Pat_exp (mk_pat (P_app (mk_id "Some", [mk_pat (P_id (mk_id "result"))])), mk_exp (E_id (mk_id "result"))))
 
 let none_pexp exp = mk_pexp (Pat_exp (mk_pat (P_app (mk_id "None", [mk_pat (P_lit (mk_lit L_unit))])), exp))
 
+let remove_completeness_attribute uannot = uannot |> remove_attribute "incomplete" |> remove_attribute "complete"
+
 let match_completeness c (E_aux (aux, (l, uannot))) =
-  let uannot =
-    uannot |> remove_attribute "incomplete" |> remove_attribute "complete" |> add_attribute (gen_loc l) c None
-  in
+  let uannot = uannot |> remove_completeness_attribute |> add_attribute (gen_loc l) c None in
   match aux with
   | E_match _ -> E_aux (aux, (l, uannot))
   | _ -> Reporting.unreachable l __POS__ "Non-match in match_completeness"
@@ -237,7 +274,7 @@ let tuple_exp = function [exp] -> exp | exps -> mk_exp (E_tuple exps)
 
 let tuple_pat = function [pat] -> pat | pats -> mk_pat (P_tuple pats)
 
-let rec mappings_match is_mapping subst mappings pexp =
+let rec mappings_match ~terminal ~return_position is_mapping subst mappings pexp =
   let handle_mapping (subst_id, P_aux (aux, (l, uannot))) =
     match aux with
     | P_app (mapping, [subpat]) ->
@@ -257,50 +294,78 @@ let rec mappings_match is_mapping subst mappings pexp =
   let subpat = tuple_pat (List.map (fun (_, _, subpat) -> subpat) mappings) in
   let match_exp =
     let arms =
-      [
-        construct_pexp (subpat, guard_opt, mk_exp (E_app (mk_id "Some", [exp])), (gen_loc l, empty_uannot));
-        wildcard_none;
-      ]
+      if terminal then [construct_pexp (subpat, guard_opt, exp, (gen_loc l, empty_uannot))]
+      else
+        [
+          construct_pexp (subpat, guard_opt, wrap_some ~return_position exp, (gen_loc l, empty_uannot));
+          wildcard_arm ~return_position ();
+        ]
     in
-    rewrite_match_untyped is_mapping subst head_exp arms (gen_loc l, empty_uannot)
+    rewrite_match_untyped ~return_position is_mapping subst head_exp arms (gen_loc l, empty_uannot)
   in
   construct_pexp (pat, Some guard_exp, match_exp, (gen_loc l, empty_uannot))
 
-and rewrite_arms is_mapping subst msa (l, uannot) =
+and rewrite_arms ~return_position is_mapping subst msa (l, uannot) =
   let head_exp_tmp = mk_id "head_exp#" in
-  let mmatch = mappings_match is_mapping subst msa.mappings msa.subst_arm in
+  let mmatch terminal = mappings_match ~terminal ~return_position is_mapping subst msa.mappings msa.subst_arm in
   let new_head_exp =
-    mk_exp (E_match (mk_exp (E_id head_exp_tmp), List.map some_arm msa.before_arms @ [mmatch; wildcard_none]))
+    mk_exp
+      (E_match
+         ( mk_exp (E_id head_exp_tmp),
+           List.map (some_arm ~return_position) msa.before_arms @ [mmatch false; wildcard_arm ~return_position ()]
+         )
+      )
     |> match_complete
   in
   let outer_match =
-    match msa.after_arms with
-    | [] ->
-        E_aux (E_match (new_head_exp, [unwrap_some]), (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot))
-        |> match_incomplete
-    | _ ->
-        let after_match =
-          rewrite_match_untyped is_mapping subst (mk_exp (E_id head_exp_tmp)) msa.after_arms (l, uannot)
-        in
-        E_aux
-          ( E_match (new_head_exp, [unwrap_some; none_pexp after_match]),
-            (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot)
-          )
-        |> match_complete
+    if return_position then (
+      match msa.after_arms with
+      | [] ->
+          mk_exp
+            (E_match (mk_exp (E_id head_exp_tmp), List.map (some_arm ~return_position) msa.before_arms @ [mmatch true]))
+          |> match_incomplete
+      | _ ->
+          let after_match =
+            rewrite_match_untyped ~return_position is_mapping subst (mk_exp (E_id head_exp_tmp)) msa.after_arms
+              (l, uannot)
+          in
+          E_aux (E_block [new_head_exp; after_match], (l, remove_completeness_attribute uannot))
+    )
+    else (
+      match msa.after_arms with
+      | [] ->
+          E_aux (E_match (new_head_exp, [unwrap_some]), (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot))
+          |> match_incomplete
+      | _ ->
+          let after_match =
+            rewrite_match_untyped ~return_position is_mapping subst (mk_exp (E_id head_exp_tmp)) msa.after_arms
+              (l, uannot)
+          in
+          E_aux
+            ( E_match (new_head_exp, [unwrap_some; none_pexp after_match]),
+              (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot)
+            )
+          |> match_complete
+    )
   in
-  mk_exp (E_let (mk_letbind (mk_pat (P_id head_exp_tmp)) msa.head_exp, outer_match))
+  (* Make sure we don't generate a pointless `let head_exp# = head_exp# in ...` *)
+  match msa.head_exp with
+  | E_aux (E_id id, _) when string_of_id id = "head_exp#" -> outer_match
+  | _ -> mk_exp (E_let (mk_letbind (mk_pat (P_id head_exp_tmp)) msa.head_exp, outer_match))
 
-and rewrite_match_untyped is_mapping subst head_exp arms (l, (uannot : uannot)) =
+and rewrite_match_untyped ~return_position is_mapping subst head_exp arms (l, (uannot : uannot)) =
   match split_arms (fun x -> x) is_mapping subst [] arms with
   | before_arms, Some (subst_arm, mappings, after_arms) ->
-      rewrite_arms is_mapping subst { head_exp; before_arms; subst_arm; mappings; after_arms } (l, uannot)
+      rewrite_arms ~return_position is_mapping subst
+        { head_exp; before_arms; subst_arm; mappings; after_arms }
+        (l, uannot)
   | _, None -> E_aux (E_match (head_exp, arms), (l, uannot))
 
-and rewrite_match_typed is_mapping subst head_exp arms (l, (tannot : tannot)) =
+and rewrite_match_typed ~return_position is_mapping subst head_exp arms (l, (tannot : tannot)) =
   match split_arms map_uannot is_mapping subst [] arms with
   | before_arms, Some (subst_arm, mappings, after_arms) ->
       let rewritten_match =
-        rewrite_arms is_mapping subst
+        rewrite_arms ~return_position is_mapping subst
           (strip_mapping_split_arms { head_exp; before_arms; subst_arm; mappings; after_arms })
           (l, untyped_annot tannot)
       in
@@ -311,7 +376,9 @@ let rewrite_exp (aux, annot) =
   match aux with
   | E_match (head_exp, arms) ->
       let fresh = name_gen "mapping" in
-      rewrite_match_typed (fun m -> Env.is_mapping m (env_of_annot annot)) fresh head_exp arms annot
+      rewrite_match_typed ~return_position:false
+        (fun m -> Env.is_mapping m (env_of_annot annot))
+        fresh head_exp arms annot
   | _ -> E_aux (aux, annot)
 
 let rewrite_ast ast =

src/lib/smt_gen.ml

@@ -353,6 +353,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
     | CT_fint n, CT_lbits ->
         let* x = signed_size ~into:lbits_size ~from:n x in
         return (Fn ("Bits", [bvint lbits_index (Big_int.of_int n); x]))
+    | CT_fint n, CT_fint m -> signed_size ~into:m ~from:n x
     | CT_lbits, CT_fbits n -> unsigned_size ~into:n ~from:lbits_size (Fn ("contents", [x]))
     | CT_fbits n, CT_fbits m -> unsigned_size ~into:m ~from:n x
     | CT_fbits n, CT_lbits ->
@@ -1242,11 +1243,12 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
     match (cval_ctyp v, ret_ctyp) with
     | CT_constant n, _ when Big_int.greater_equal n Big_int.zero ->
         return (bvint (int_size ret_ctyp) (Big_int.pow_int_positive 2 (Big_int.to_int n)))
-    | CT_lint, CT_lint ->
-        let* v = smt_cval v in
+    | ctyp, _ ->
         (* TODO: Check we haven't shifted too far *)
-        return (bvshl (bvone lint_size) v)
-    | _ -> builtin_type_error "pow2" [v] (Some ret_ctyp)
+        let sz = int_size ctyp in
+        let ret_sz = int_size ret_ctyp in
+        let* shift = bind (smt_cval v) (signed_size ~into:ret_sz ~from:sz) in
+        return (bvshl (bvone ret_sz) shift)
 
   let builtin_count_leading_zeros v ret_ctyp =
     let rec lzcnt ret_sz sz smt =
@@ -1367,6 +1369,10 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
         in
         return (Fn ("or", constructors))
     | (CT_fbits _ | CT_lbits), (CT_fbits _ | CT_lbits) -> builtin_eq_bits x y
+    | CT_bit, CT_bit ->
+        let* x = smt_cval x in
+        let* y = smt_cval y in
+        return (Fn ("=", [x; y]))
     | (CT_constant _ | CT_fint _ | CT_lint), (CT_constant _ | CT_fint _ | CT_lint) -> builtin_eq_int x y
     | CT_unit, CT_unit -> return (Bool_lit true)
     | CT_enum _, CT_enum _ ->

src/lib/util.ml

@@ -347,6 +347,7 @@ let string_to_list s =
 module IntSet = Set.Make (Int)
 module IntMap = Map.Make (Int)
 
+module StringSet = Set.Make (String)
 module StringMap = Map.Make (String)
 
 module IntIntSet = Set.Make (struct

src/lib/util.mli

@@ -268,11 +268,13 @@ val string_to_list : string -> char list
 
 (** {2 Useful sets} *)
 
-(** Sets of Integers *)
+(** Sets of integers and strings *)
 module IntSet : Set.S with type elt = int and type t = Set.Make(Int).t
 
 module IntMap : Map.S with type key = int and type 'a t = 'a Map.Make(Int).t
 
+module StringSet : Set.S with type elt = string and type t = Set.Make(String).t
+
 module StringMap : Map.S with type key = string and type 'a t = 'a Map.Make(String).t
 
 module IntIntSet : Set.S with type elt = int * int

src/lib/value.ml

@@ -457,6 +457,8 @@ let value_undefined_vector = function
   | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2))
   | _ -> failwith "value undefined_vector"
 
+let value_undefined_range = function [v1; v2] -> v1 | _ -> failwith "value undefined_range"
+
 let value_undefined_list = function [_] -> V_list [] | _ -> failwith "value undefined_list"
 
 let value_undefined_bitvector = function
@@ -795,6 +797,7 @@ let primops =
          ("undefined_unit", fun _ -> V_unit);
          ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
          ("undefined_int", fun _ -> V_int Big_int.zero);
+         ("undefined_range", value_undefined_range);
          ("undefined_nat", fun _ -> V_int Big_int.zero);
          ("undefined_bool", fun _ -> V_bool false);
          ("undefined_bitvector", value_undefined_bitvector);