Add a string_literal type, as a subtype of string

The main motivation for this is for the Sail->SystemVerilog backend,
where we can easily represent string literals as elements of an
enumeration-like type, but cannot deal at all with run-time created
strings. There is an option -sv_nostrings that removes all strings, but
with this option we can at least keep literal strings.

Eventually the plan would be to use the effect system to track runtime
created strings in such a way we can guarantee that they never affect
the behaviour of the model, so can be safely removed.

This commit adds a -string_literal_type option that causes string
literals to be inferred as the `string_literal` type which is a subtype
of the `string` type. We already have subtyping for refinement types so
mostly this just works with a few minor adjustments for mappings and
string literal patterns.

editors/sail-mode.el

@@ -40,7 +40,7 @@
     "exmem" "undef" "unspec" "nondet" "escape" "configuration"))
 
 (defconst sail-types
-  '("vector" "bitvector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits" "option" "result"))
+  '("vector" "bitvector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "string_literal" "bits" "option" "result"))
 
 (defconst sail-special
   '("_prove" "_not_prove" "create" "kill" "convert" "undefined"

src/bin/sail.ml

@@ -168,6 +168,7 @@ let rec options =
         "<symbol> check if a feature symbol is set by default"
       );
       ("-no_color", Arg.Clear Util.opt_colors, " do not use terminal color codes in output");
+      ("-string_literal_type", Arg.Set Type_env.opt_string_literal_type, " use a separate string_literal type for string literals");
       ( "-undefined_gen",
         Arg.Set Initial_check.opt_undefined_gen,
         " generate undefined_type functions for types in the specification"

src/lib/ast_util.ml

@@ -481,6 +481,7 @@ let range_typ nexp1 nexp2 =
 let bool_typ = mk_id_typ (mk_id "bool")
 let atom_bool_typ nc = mk_typ (Typ_app (mk_id "atom_bool", [mk_typ_arg (A_bool nc)]))
 let string_typ = mk_id_typ (mk_id "string")
+let string_literal_typ = mk_id_typ (mk_id "string_literal")
 let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (A_typ typ)]))
 let tuple_typ typs = mk_typ (Typ_tuple typs)
 let function_typ arg_typs ret_typ = mk_typ (Typ_fn (arg_typs, ret_typ))

src/lib/ast_util.mli

@@ -220,6 +220,7 @@ val app_typ : id -> typ_arg list -> typ
 val register_typ : typ -> typ
 val unit_typ : typ
 val string_typ : typ
+val string_literal_typ : typ
 val real_typ : typ
 val vector_typ : nexp -> typ -> typ
 val bitvector_typ : nexp -> typ

src/lib/initial_check.ml

@@ -1381,6 +1381,7 @@ let initial_ctx =
           ("unit", []);
           ("bit", []);
           ("string", []);
+          ("string_literal", []);
           ("real", []);
           ("list", [Some K_type]);
           ("register", [Some K_type]);

src/lib/type_check.ml

@@ -601,6 +601,7 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as
   | Typ_app (id1, []), Typ_id id2 when Id.compare id1 id2 = 0 -> KBindings.empty
   | Typ_id id1, Typ_app (id2, []) when Id.compare id1 id2 = 0 -> KBindings.empty
   | Typ_id id1, Typ_id id2 when Id.compare id1 id2 = 0 -> KBindings.empty
+  | Typ_id id1, Typ_id id2 when Id.compare id1 (mk_id "string") = 0 && Id.compare id2 (mk_id "string_literal") = 0 -> KBindings.empty
   | Typ_tuple typs1, Typ_tuple typs2 when List.length typs1 = List.length typs2 ->
       List.fold_left (merge_uvars env l) KBindings.empty (List.map2 (unify_typ l env goals) typs1 typs2)
   | Typ_fn (arg_typs1, ret_typ1), Typ_fn (arg_typs2, ret_typ2) when List.length arg_typs1 = List.length arg_typs2 ->
@@ -1088,6 +1089,7 @@ let rec subtyp l env typ1 typ2 =
       match (typ_aux1, typ_aux2) with
       | _, Typ_internal_unknown when Env.allow_unknowns env -> ()
       | Typ_app (id1, _), Typ_id id2 when string_of_id id1 = "atom_bool" && string_of_id id2 = "bool" -> ()
+      | Typ_id id1, Typ_id id2 when string_of_id id1 = "string_literal" && string_of_id id2 = "string" -> ()
       | Typ_tuple typs1, Typ_tuple typs2 when List.length typs1 = List.length typs2 ->
           List.iter2 (subtyp l env) typs1 typs2
       | Typ_app (id1, args1), Typ_app (id2, args2) when Id.compare id1 id2 = 0 && List.length args1 = List.length args2
@@ -1343,6 +1345,7 @@ let infer_lit env (L_aux (lit_aux, l)) =
   | L_num n -> atom_typ (nconstant n)
   | L_true -> atom_bool_typ nc_true
   | L_false -> atom_bool_typ nc_false
+  | L_string _ when !Type_env.opt_string_literal_type -> string_literal_typ
   | L_string _ -> string_typ
   | L_real _ -> real_typ
   | L_bin str -> bits_typ env (nint (String.length str))
@@ -2316,7 +2319,7 @@ and bind_pat env (P_aux (pat_aux, (l, uannot)) as pat) typ =
     end
   | P_string_append pats -> begin
       match Env.expand_synonyms env typ with
-      | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 ->
+      | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 || Id.compare id (mk_id "string_literal") = 0 ->
           let rec process_pats env = function
             | [] -> ([], env, [])
             | pat :: pats ->
@@ -2531,6 +2534,9 @@ and infer_pat env (P_aux (pat_aux, (l, uannot)) as pat) =
       Env.wf_typ env typ_annot;
       let typed_pat, env, guards = bind_pat env pat typ_annot in
       (annot_pat (P_typ (typ_annot, typed_pat)) typ_annot, env, guards)
+  | P_lit (L_aux (L_string _, _) as lit) ->
+    (* String literal patterns match strings, not just string_literals *)
+    (annot_pat (P_lit lit) string_typ, env, [])
   | P_lit lit -> (annot_pat (P_lit lit) (infer_lit env lit), env, [])
   | P_vector (pat :: pats) ->
       let fold_pats (pats, env, guards) pat =
@@ -2550,7 +2556,7 @@ and infer_pat env (P_aux (pat_aux, (l, uannot)) as pat) =
   | P_string_append pats ->
       let fold_pats (pats, env, guards) pat =
         let inferred_pat, env, guards' = infer_pat env pat in
-        typ_equality l env (typ_of_pat inferred_pat) string_typ;
+        subtyp l env (typ_of_pat inferred_pat) string_typ;
         (pats @ [inferred_pat], env, guards' @ guards)
       in
       let typed_pats, env, guards = List.fold_left fold_pats ([], env, []) pats in
@@ -3553,7 +3559,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, uannot)) as mpa
     end
   | MP_string_append mpats -> begin
       match Env.expand_synonyms env typ with
-      | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 ->
+      | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 || Id.compare id (mk_id "string_literal") = 0 ->
           let rec process_mpats env = function
             | [] -> ([], env, [])
             | pat :: pats ->
@@ -3808,6 +3814,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, uannot)) as mp
         end
       | _ -> typ_error l ("Malformed mapping type " ^ string_of_id f)
     end
+  | MP_lit (L_aux (L_string _, _) as lit) -> (annot_mpat (MP_lit lit) string_typ, env, [])
   | MP_lit lit -> (annot_mpat (MP_lit lit) (infer_lit env lit), env, [])
   | MP_typ (mpat, typ_annot) ->
       Env.wf_typ env typ_annot;
@@ -3827,7 +3834,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, uannot)) as mp
   | MP_string_append mpats ->
       let fold_pats (pats, env, guards) pat =
         let inferred_pat, env, guards' = infer_mpat allow_unknown other_env env pat in
-        typ_equality l env (typ_of_mpat inferred_pat) string_typ;
+        subtyp l env (typ_of_mpat inferred_pat) string_typ;
         (pats @ [inferred_pat], env, guards' @ guards)
       in
       let typed_mpats, env, guards = List.fold_left fold_pats ([], env, []) mpats in

src/lib/type_env.ml

@@ -77,6 +77,8 @@ open Type_internal
    the SMT solver to use non-linear arithmetic. *)
 let opt_smt_linearize = ref false
 
+let opt_string_literal_type = ref false
+
 module IdPair = struct
   type t = id * id
   let compare (a, b) (c, d) =
@@ -278,6 +280,7 @@ let builtin_typs =
       ("real", []);
       ("list", [K_type]);
       ("string", []);
+      ("string_literal", []);
       ("itself", [K_int]);
       ("atom_bool", [K_bool]);
       ("float16", []);

src/lib/type_env.mli

@@ -72,6 +72,9 @@ open Ast_util
    the SMT solver to use non-linear arithmetic. *)
 val opt_smt_linearize : bool ref
 
+(** Val use a separate string literal type *)
+val opt_string_literal_type : bool ref
+
 type global_env
 
 type env

src/sail_c_backend/c_backend.ml

@@ -201,6 +201,7 @@ end) : CONFIG = struct
     | Typ_id id when string_of_id id = "nat" -> CT_lint
     | Typ_id id when string_of_id id = "unit" -> CT_unit
     | Typ_id id when string_of_id id = "string" -> CT_string
+    | Typ_id id when string_of_id id = "string_literal" -> CT_string
     | Typ_id id when string_of_id id = "real" -> CT_real
     | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
     | Typ_app (id, args) when string_of_id id = "itself" -> convert_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))

src/sail_coq_backend/pretty_print_coq.ml

@@ -603,6 +603,7 @@ let rec doc_typ_fns ctx env =
     | _ -> atomic_typ atyp_needed ty
   and atomic_typ atyp_needed (Typ_aux (t, l) as ty) =
     match t with
+    | Typ_id (Id_aux (Id "string_literal", _)) -> string "string"
     | Typ_id (Id_aux (Id "bool", _)) -> string "bool"
     | Typ_id (Id_aux (Id "bit", _)) -> string "bitU"
     | Typ_id id ->

src/sail_lem_backend/pretty_print_lem.ml

@@ -398,6 +398,7 @@ let doc_typ_lem, doc_typ_lem_brackets, doc_atomic_typ_lem =
     | _ -> atomic_typ params_to_print atyp_needed ty
   and atomic_typ params_to_print atyp_needed (Typ_aux (t, l) as ty) =
     match t with
+    | Typ_id (Id_aux (Id "string_literal", _)) -> string "string"
     | Typ_id (Id_aux (Id "bool", _)) -> string "bool"
     | Typ_id (Id_aux (Id "bit", _)) -> string "bitU"
     | Typ_id id ->

src/sail_ocaml_backend/ocaml_backend.ml

@@ -145,6 +145,7 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, l)) arg =
 
 let ocaml_typ_id ctx = function
   | id when Id.compare id (mk_id "string") = 0 -> string "string"
+  | id when Id.compare id (mk_id "string_literal") = 0 -> string "string"
   | id when Id.compare id (mk_id "list") = 0 -> string "list"
   | id when Id.compare id (mk_id "bit") = 0 -> string "bit"
   | id when Id.compare id (mk_id "int") = 0 -> string "Big_int.num"

test/c/string_literal_type.expect

@@ -0,0 +1,7 @@
+foo
+foo
+baz
+baz
+ok
+ok
+ok

test/c/string_literal_type.sail

@@ -0,0 +1,33 @@
+$include <prelude.sail>
+
+$option -string_literal_type
+
+val test : string_literal -> unit
+
+function test(s) = print_endline(s)
+
+val main : unit -> unit
+
+function main() = {
+  let x : string_literal = "foo";
+  var y : string_literal = "bar";
+  let z = "baz";
+  y = x;
+  print_endline(y);
+  test(y);
+  y = z;
+  print_endline(y);
+  test(y);
+  match x {
+    "foo" => print_endline("ok"),
+    _ => print_endline("fail"),
+  };
+  match y {
+    "baz" => print_endline("ok"),
+    _ => print_endline("fail"),
+  };
+  match concat_str(x, z) {
+    "foobaz" => print_endline("ok"),
+    _ => print_endline("fail"),
+  }
+}

test/typecheck/pass/string_literal_type.sail

@@ -0,0 +1,34 @@
+$include <prelude.sail>
+
+$option -string_literal_type
+
+val test : string_literal -> unit
+
+function test(s) = print_endline(s)
+
+val main : unit -> unit
+
+function main() = {
+  let x : string_literal = "foo";
+  var y : string_literal = "bar";
+  let z = "baz";
+  test(z);
+  y = x;
+  print_endline(y);
+  test(y);
+  y = z;
+  print_endline(y);
+  test(y);
+  match x {
+    "foo" => print_endline("ok"),
+    _ => print_endline("fail"),
+  };
+  match y {
+    "baz" => print_endline("ok"),
+    _ => print_endline("fail"),
+  };
+  match concat_str(x, z) {
+    "foobaz" => print_endline("ok"),
+    _ => print_endline("fail"),
+  }
+}

test/typecheck/pass/string_literal_type/v1.expect

@@ -0,0 +1,5 @@
+Type error:
+pass/string_literal_type/v1.sail:14.7-23:
+14 |  test(concat_str(x, z))
+   |       ^--------------^
+   | string is not a subtype of string_literal

test/typecheck/pass/string_literal_type/v1.sail

@@ -0,0 +1,15 @@
+$include <prelude.sail>
+
+$option -string_literal_type
+
+val test : string_literal -> unit
+
+function test(s) = print_endline(s)
+
+val main : unit -> unit
+
+function main() = {
+  let x : string_literal = "foo";
+  let z = "baz";
+  test(concat_str(x, z))
+}