Fix issues with missing well-formedness checks

Make sure numeric type synonyms with arguments are expanded correctly

src/lib/type_check.ml

@@ -2824,6 +2824,7 @@ and bind_assignment assign_l env (LE_aux (lexp_aux, (lexp_l, uannot)) as lexp) e
   match lexp_aux with
   | LE_app (f, xs) -> (check_exp env (E_aux (E_app (f, xs @ [exp]), (lexp_l, uannot))) unit_typ, env)
   | LE_typ (typ_annot, _) ->
+      Env.wf_typ ~at:lexp_l env typ_annot;
       let checked_exp = crule check_exp env exp typ_annot in
       let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
       (annot_assign tlexp checked_exp, env')
@@ -3453,7 +3454,8 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
   let typ_args =
     match expected_ret_typ with
     | None -> typ_args
-    | Some expect when is_exist (Env.expand_synonyms env expect) || is_exist !typ_ret -> typ_args
+    | Some expect when is_exist (Env.expand_synonyms env expect) -> typ_args
+    | Some expect when is_exist !typ_ret -> typ_args
     | Some expect -> (
         let goals = quant_kopts (mk_typquant !quants) |> List.map kopt_kid |> KidSet.of_list in
         try
@@ -4626,6 +4628,7 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t =
   | DEF_default default -> check_default env def_annot default
   | DEF_overload (id, ids) -> ([DEF_aux (DEF_overload (id, ids), def_annot)], Env.add_overloads def_annot.loc id ids env)
   | DEF_register (DEC_aux (DEC_reg (typ, id, None), (l, uannot))) -> begin
+      Env.wf_typ ~at:l env typ;
       match typ with
       | Typ_aux (Typ_app (Id_aux (Id "option", _), [_]), _) ->
           Reporting.warn "No default value" l "Registers of type option should explicitly be given a default value";
@@ -4643,6 +4646,8 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t =
           )
     end
   | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), (l, _))) ->
+      typ_print (lazy "WF reg");
+      Env.wf_typ ~at:l env typ;
       let checked_exp = crule check_exp env exp typ in
       let env = Env.add_register id typ env in
       ( [

src/lib/type_env.ml

@@ -556,7 +556,12 @@ let mk_synonym typq typ_arg =
         let typ_arg, ncs = subst_args env l kopts args in
         (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs)
     | [], [] -> (typ_arg, ncs)
-    | _, _ -> typ_error l "Synonym applied to bad arguments"
+    | kopts, args ->
+        typ_error l
+          ("Synonym applied to bad arguments "
+          ^ Util.string_of_list ", " string_of_kinded_id kopts
+          ^ Util.string_of_list ", " string_of_typ_arg args
+          )
   in
   fun l env args ->
     let typ_arg, ncs = subst_args env l kopts args in
@@ -648,7 +653,12 @@ and wf_nexp ?(exs = KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
             )
     end
   | Nexp_constant _ -> ()
-  | Nexp_app (_, nexps) -> List.iter (fun n -> wf_nexp ~exs env n) nexps
+  | Nexp_app (id, nexps) ->
+      let name = string_of_id id in
+      (* We allow the abs, mod, and div functions that are included in the SMTLIB2 integer theory *)
+      if name = "abs" || name = "mod" || name = "div" || Bindings.mem id env.global.synonyms then
+        List.iter (fun n -> wf_nexp ~exs env n) nexps
+      else typ_error l ("Unknown type level operator or function " ^ name)
   | Nexp_times (nexp1, nexp2) ->
       wf_nexp ~exs env nexp1;
       wf_nexp ~exs env nexp2
@@ -734,7 +744,7 @@ and expand_nexp_synonyms env (Nexp_aux (aux, l) as nexp) =
   | Nexp_app (id, args) -> (
       try
         begin
-          match get_typ_synonym id env l env [] with
+          match get_typ_synonym id env l env (List.map arg_nexp args) with
           | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp
           | _ -> typ_error l ("Expected Int when expanding synonym " ^ string_of_id id)
         end

test/lem/run_tests.py

@@ -43,6 +43,7 @@
     # The Lem backend needs sail_mem_read to be instantiated at a minimum
     'concurrency_interface_dec',
     'concurrency_interface_inc',
+    'wf_register_type',
 }
 
 print('Sail is {}'.format(sail))

test/typecheck/fail/wf_assign_type.expect

@@ -0,0 +1,10 @@
+Type error:
+fail/wf_assign_type.sail:9.10-17:
+9 |  var Y : bits(X) = 0b00;
+  |          ^-----^
+  | Well-formedness check failed for type
+  | 
+  | Caused by fail/wf_assign_type.sail:9.15-16:
+  | 9 |  var Y : bits(X) = 0b00;
+  |   |               ^
+  |   | Undefined type synonym X

test/typecheck/fail/wf_assign_type.sail

@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+type bar : Int = 10
+
+function foo() -> bits(bar) = {
+  let X = sizeof(bar);
+  var Y : bits(X) = 0b00;
+  Y
+}

test/typecheck/pass/existential_ast/v3.expect

@@ -9,4 +9,4 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * 'ex340# in {32, 64}
+   | * 'ex343# in {32, 64}

test/typecheck/pass/wf_register_type.sail

@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+type x : Int = 8
+
+type operator /('n : Int, 'm : Int) -> Int = div('n, 'm)
+
+register r : bits(x / 2) = 0x0

test/typecheck/pass/wf_register_type/v1.expect

@@ -0,0 +1,10 @@
+Type error:
+pass/wf_register_type/v1.sail:7.13-24:
+7 |register r : bits(x / 2) = 0x0
+  |             ^---------^
+  | Well-formedness check failed for type
+  | 
+  | Caused by pass/wf_register_type/v1.sail:7.18-23:
+  | 7 |register r : bits(x / 2) = 0x0
+  |   |                  ^---^
+  |   | Unknown type level operator or function (operator /)

test/typecheck/pass/wf_register_type/v1.sail

@@ -0,0 +1,7 @@
+default Order dec
+
+$include <prelude.sail>
+
+type x : Int = 8
+
+register r : bits(x / 2) = 0x0