SV: Add parser for types when binding to external primitives

lib/concurrency_interface/emulator_memory.sail

@@ -100,6 +100,7 @@ val read_mem# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
  ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
+$[sv_module { reads_memory = true }]
 val __read_mem# = impure "emulator_read_mem" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
  (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
@@ -116,6 +117,7 @@ val read_mem_ifetch# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {3
  ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
+$[sv_module { reads_memory = true }]
 val __read_mem_ifetch# = impure "emulator_read_mem_ifetch" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
  (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
@@ -132,6 +134,7 @@ val read_mem_exclusive# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in
  ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
+$[sv_module { reads_memory = true }]
 val __read_mem_exclusive# = impure "emulator_read_mem_exclusive" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
  (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
@@ -148,6 +151,7 @@ val write_mem# : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
  ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
+$[sv_module { writes_memory = true }]
 val __write_mem# = impure "emulator_write_mem" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
  (int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
@@ -164,15 +168,18 @@ val write_mem_exclusive# : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in
  ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
+$[sv_module { writes_memory = true }]
 val __write_mem_exclusive# = impure "emulator_write_mem_exclusive" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
  (int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 function write_mem_exclusive#(_, addrsize, addr, n, value) = __write_mem_exclusive#(addrsize, addr, n, value)
 $endif
 $endif
 
+$[sv_module { reads_memory = true }]
 val read_tag# = impure "emulator_read_tag" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> bool
 
+$[sv_module { writes_memory = true }]
 val write_tag# = impure "emulator_write_tag" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize), bool) -> unit
 
 $endif

lib/hex_bits.sail

@@ -73,6 +73,8 @@ $include <vector.sail>
 $include <string.sail>
 
 val "parse_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bits('n)
+
+$[sv_function { types = "int #0" }]
 val "valid_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bool
 
 val hex_bits : forall 'n, 'n > 0. bits('n) <-> (int('n), string)

lib/mapping.sail

@@ -71,13 +71,12 @@ $define _MAPPING
 $include <arith.sail>
 $include <option.sail>
 
-$[sv_function { arguments = ["string", "int"], return_type = "string" }]
+$[sv_function { types = "int #1" }]
 val string_take = pure "string_take" : (string, nat) -> string
 
-$[sv_function { arguments = ["string", "int"], return_type = "string" }]
+$[sv_function { types = "int #1" }]
 val string_drop = pure "string_drop" : (string, nat) -> string
 
-$[sv_function { arguments = "string", return_type = "int" }]
 val string_length = pure "string_length" : string -> nat
 
 val string_append = pure {coq: "String.append", c: "concat_str", _: "string_append"} : (string, string) -> string

lib/sv/sail_modules.sv

@@ -33,7 +33,7 @@ module print_endline
  end
 endmodule // print_endline
 
-function automatic bit sail_valid_hex_bits(int n, string hex);
+function automatic bit valid_hex_bits(int n, string hex);
  int len = hex.len();
  int non_zero = 2;
  int fnz_width;
@@ -66,10 +66,10 @@ function automatic bit sail_valid_hex_bits(int n, string hex);
  end;
 
  return 1'h1;
-endfunction // sail_valid_hex_bits
+endfunction // valid_hex_bits
 
-function automatic string sail_string_take(string str, int n);
+function automatic string string_take(string str, int n);
  return str.substr(0, n - 1);
-endfunction // sail_string_take
+endfunction // string_take
 
 `endif

src/lib/ast_util.ml

@@ -110,6 +110,8 @@ let attribute_data_string = function AD_aux (AD_string s, _) -> Some s | _ -> No
 
 let attribute_data_string_with_loc = function AD_aux (AD_string s, l) -> Some (s, l) | _ -> None
 
+let attribute_data_list = function AD_aux (AD_list xs, _) -> Some xs | _ -> None
+
 let json_of_attribute attr = function
  | None -> `String attr
  | Some data -> `List [`String attr; json_of_attribute_data data]

src/lib/ast_util.mli

@@ -104,6 +104,8 @@ val attribute_data_string : attribute_data -> string option
 
 val attribute_data_string_with_loc : attribute_data -> (string * Parse_ast.l) option
 
+val attribute_data_list : attribute_data -> attribute_data list option
+
 (** Add an attribute to an annotation. Attributes are attached to expressions in Sail via:
  {@sail[
  $[attribute argument] expression

src/lib/initial_check.mli

@@ -148,6 +148,8 @@ val typ_of_string : ?inline:Lexing.position -> string -> typ
 
 val constraint_of_string : ?inline:Lexing.position -> string -> n_constraint
 
+val parse_from_string : (Lexing.lexbuf -> 'a) -> ?inline:Lexing.position -> string -> 'a
+
 (** {2 Parsing files } *)
 
 (** Parse a file into a sequence of comments and a parse AST

src/lib/smt_exp.ml

@@ -324,7 +324,12 @@ let or_order x y =
  | None, Some _ -> 1
  | None, None -> 0
 
-let identical x y = match (x, y) with Var x, Var y -> Name.compare x y = 0 | _ -> false
+let rec identical x y =
+ match (x, y) with
+ | Var x, Var y -> Name.compare x y = 0
+ | Fn (f1, args1), Fn (f2, args2) ->
+ String.compare f1 f2 = 0 && List.compare_lengths args1 args2 = 0 && List.for_all2 identical args1 args2
+ | _ -> false
 
 let simp_eq x y =
  match (x, y) with
@@ -434,6 +439,18 @@ module Simplifier = struct
  let rule_ite_literal =
  mk_simple_rule __LOC__ @@ function Ite (Bool_lit b, x, y) -> change (if b then x else y) | _ -> NoChange
 
+ let rec remove_duplicates = function
+ | x :: xs ->
+ let xs' = List.filter (fun x' -> not (identical x x')) xs in
+ x :: remove_duplicates xs'
+ | [] -> []
+
+ let rule_and_duplicates =
+ mk_simple_rule __LOC__ @@ function Fn ("and", xs) -> Change (0, Fn ("and", remove_duplicates xs)) | _ -> NoChange
+
+ let rule_or_duplicates =
+ mk_simple_rule __LOC__ @@ function Fn ("or", xs) -> Change (0, Fn ("or", remove_duplicates xs)) | _ -> NoChange
+
  let rule_and_inequalities =
  mk_simple_rule __LOC__ @@ function
  | Fn ("and", xs) ->
@@ -749,6 +766,10 @@ module Simplifier = struct
  | Fn ("not", [Fn ("and", xs)]) -> change (Fn ("or", List.map (fun x -> Fn ("not", [x])) xs))
  | Fn ("not", [Ite (i, t, e)]) -> change (Ite (i, Fn ("not", [t]), Fn ("not", [e])))
  | Fn ("not", [Bool_lit b]) -> change (Bool_lit (not b))
+ | Fn ("not", [Fn ("bvslt", [x; y])]) -> change (Fn ("bvsge", [x; y]))
+ | Fn ("not", [Fn ("bvsle", [x; y])]) -> change (Fn ("bvsgt", [x; y]))
+ | Fn ("not", [Fn ("bvsgt", [x; y])]) -> change (Fn ("bvsle", [x; y]))
+ | Fn ("not", [Fn ("bvsge", [x; y])]) -> change (Fn ("bvslt", [x; y]))
  | _ -> NoChange
 
  let is_bvfunction = function
@@ -877,6 +898,7 @@ let simp simpset exp =
  rule_flatten_and;
  rule_false_and;
  rule_true_and;
+ rule_and_duplicates;
  rule_and_inequalities;
  rule_order_and;
  Repeat rule_and_assume;
@@ -885,7 +907,17 @@ let simp simpset exp =
  )
  | Fn ("or", _) ->
  run_strategy simpset exp
- (Then [rule_flatten_or; rule_true_or; rule_false_or; rule_or_equalities; rule_order_or; Repeat rule_or_assume])
+ (Then
+ [
+ rule_flatten_or;
+ rule_true_or;
+ rule_false_or;
+ rule_or_duplicates;
+ rule_or_equalities;
+ rule_order_or;
+ Repeat rule_or_assume;
+ ]
+ )
  | Var _ -> run_strategy simpset exp rule_var
  | Fn ("=", _) -> run_strategy simpset exp (Then [rule_inequality; rule_simp_eq; rule_concat_literal_eq])
  | Fn ("not", _) -> run_strategy simpset exp (Then [Repeat rule_not_not; Repeat rule_not_push; rule_inequality])

src/lib/smt_gen.ml

@@ -1083,15 +1083,11 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
  (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1)) - 1) ~from:(int_size i_ctyp))
  in
  return (Store (Fixed (len, ctyp), store_fn, vec, i, 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 _ ->
- Fn
- ( "store",
- [smt_cval ctx vec; force_size ctx !vector_index (int_size ctx index_ctyp) (smt_cval ctx i); smt_cval ctx x]
- )
- *)
+ | CT_vector _, i_ctyp, _, CT_vector _ ->
+ let* vec = smt_cval vec in
+ let* i = bind (smt_cval i) (unsigned_size ~checked:false ~into:32 ~from:(int_size i_ctyp)) in
+ let* x = smt_cval x in
+ return (Fn ("vupdate", [vec; i; x]))
  | _ -> builtin_type_error "vector_update" [vec; i; x] (Some ret_ctyp)
 
  let builtin_vector_update_inc vec i x ret_ctyp =

src/sail_sv_backend/dune

@@ -12,6 +12,11 @@
  (native plugin))
  (libraries libsail))
 
+(menhir
+ (modules sv_type_parser))
+
+(ocamllex sv_type_lexer)
+
 (install
  (section
  (site