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/Replicate/v2.expect

@@ -8,4 +8,4 @@ Explicit effect annotations are deprecated. They are no longer used and can be r
 pass/Replicate/v2.sail:13.4-30:
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Failed to prove constraint: ('M * 'ex249#) == 'N
+   | Failed to prove constraint: ('M * 'ex248#) == 'N

test/typecheck/pass/bool_constraint/v1.expect

@@ -9,13 +9,13 @@ All external bindings should be marked as either monadic or pure
 12 |  if b then n else 4
    |                   ^
    | int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
-   | as (('b & 'ex240 == 'n) | (not('b) & 'ex240 == 3)) could not be proven
+   | as (('b & 'ex239 == 'n) | (not('b) & 'ex239 == 3)) could not be proven
    | 
-   | type variable 'ex240:
+   | type variable 'ex239:
    | pass/bool_constraint/v1.sail:9.25-73:
    | 9 |  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
    |   |                         ^----------------------------------------------^ derived from here
    | pass/bool_constraint/v1.sail:12.19-20:
    | 12 |  if b then n else 4
    |    |                   ^ bound here
-   |    | has constraint: 4 == 'ex240
+   |    | has constraint: 4 == 'ex239

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}
+   | * 'ex342# in {32, 64}

test/typecheck/pass/existential_ast3/v1.expect

@@ -2,26 +2,26 @@
 pass/existential_ast3/v1.sail:17.48-65:
 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |                                                ^---------------^
-   | (int(33), int('ex291)) is not a subtype of (int('ex286), int('ex287))
-   | as ((33 == 32 | 33 == 64) & (0 <= 'ex291 & 'ex291 < 33)) could not be proven
+   | (int(33), int('ex290)) is not a subtype of (int('ex285), int('ex286))
+   | as ((33 == 32 | 33 == 64) & (0 <= 'ex290 & 'ex290 < 33)) could not be proven
    | 
-   | type variable 'ex286:
+   | type variable 'ex285:
    | pass/existential_ast3/v1.sail:16.23-25:
    | 16 |  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
    |    |                       ^^ derived from here
    | pass/existential_ast3/v1.sail:17.48-65:
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^ bound here
    | 
-   | type variable 'ex287:
+   | type variable 'ex286:
    | pass/existential_ast3/v1.sail:16.26-28:
    | 16 |  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
    |    |                          ^^ derived from here
    | pass/existential_ast3/v1.sail:17.48-65:
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^ bound here
    | 
-   | type variable 'ex291:
+   | type variable 'ex290:
    | pass/existential_ast3/v1.sail:17.48-65:
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^ bound here

test/typecheck/pass/existential_ast3/v2.expect

@@ -2,26 +2,26 @@
 pass/existential_ast3/v2.sail:17.48-65:
 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |                                                ^---------------^
-   | (int(31), int('ex291)) is not a subtype of (int('ex286), int('ex287))
-   | as ((31 == 32 | 31 == 64) & (0 <= 'ex291 & 'ex291 < 31)) could not be proven
+   | (int(31), int('ex290)) is not a subtype of (int('ex285), int('ex286))
+   | as ((31 == 32 | 31 == 64) & (0 <= 'ex290 & 'ex290 < 31)) could not be proven
    | 
-   | type variable 'ex286:
+   | type variable 'ex285:
    | pass/existential_ast3/v2.sail:16.23-25:
    | 16 |  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
    |    |                       ^^ derived from here
    | pass/existential_ast3/v2.sail:17.48-65:
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^ bound here
    | 
-   | type variable 'ex287:
+   | type variable 'ex286:
    | pass/existential_ast3/v2.sail:16.26-28:
    | 16 |  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
    |    |                          ^^ derived from here
    | pass/existential_ast3/v2.sail:17.48-65:
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^ bound here
    | 
-   | type variable 'ex291:
+   | type variable 'ex290:
    | pass/existential_ast3/v2.sail:17.48-65:
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^ bound here

test/typecheck/pass/existential_ast3/v3.expect

@@ -3,4 +3,4 @@
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * ((64 == 32 | 64 == 64) & (0 <= 'ex330# & 'ex330# < 64))
+   | * ((64 == 32 | 64 == 64) & (0 <= 'ex329# & 'ex329# < 64))

test/typecheck/pass/existential_ast3/v4.expect

@@ -3,13 +3,13 @@
 36 |    if is_64 then 64 else 32;
    |                  ^^
    | int(64) is not a subtype of {('d : Int), (('is_64 & 'd == 63) | (not('is_64) & 'd == 32)). int('d)}
-   | as (('is_64 & 'ex350 == 63) | (not('is_64) & 'ex350 == 32)) could not be proven
+   | as (('is_64 & 'ex349 == 63) | (not('is_64) & 'ex349 == 32)) could not be proven
    | 
-   | type variable 'ex350:
+   | type variable 'ex349:
    | pass/existential_ast3/v4.sail:35.18-79:
    | 35 |  let 'datasize : {'d, ('is_64 & 'd == 63) | (not('is_64) & 'd == 32). int('d)} =
    |    |                  ^-----------------------------------------------------------^ derived from here
    | pass/existential_ast3/v4.sail:36.18-20:
    | 36 |    if is_64 then 64 else 32;
    |    |                  ^^ bound here
-   |    | has constraint: 64 == 'ex350
+   |    | has constraint: 64 == 'ex349

test/typecheck/pass/existential_ast3/v5.expect

@@ -3,13 +3,13 @@
 37 |  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
    |                                                  ^-------------^
    | range(0, 63) is not a subtype of range(0, ('datasize - 2))
-   | as (0 <= 'ex356 & 'ex356 <= ('datasize - 2)) could not be proven
+   | as (0 <= 'ex355 & 'ex355 <= ('datasize - 2)) could not be proven
    | 
-   | type variable 'ex356:
+   | type variable 'ex355:
    | pass/existential_ast3/v5.sail:37.10-33:
    | 37 |  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
    |    |          ^---------------------^ derived from here
    | pass/existential_ast3/v5.sail:37.50-65:
    | 37 |  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
    |    |                                                  ^-------------^ bound here
-   |    | has constraint: (0 <= 'ex356 & 'ex356 <= 63)
+   |    | has constraint: (0 <= 'ex355 & 'ex355 <= 63)

test/typecheck/pass/existential_ast3/v6.expect

@@ -3,13 +3,13 @@
 37 |  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
    |                                                                       ^-------------^
    | range(0, 63) is not a subtype of range(0, ('datasize - 1))
-   | as (0 <= 'ex360 & 'ex360 <= ('datasize - 1)) could not be proven
+   | as (0 <= 'ex359 & 'ex359 <= ('datasize - 1)) could not be proven
    | 
-   | type variable 'ex360:
+   | type variable 'ex359:
    | pass/existential_ast3/v6.sail:37.10-33:
    | 37 |  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
    |    |          ^---------------------^ derived from here
    | pass/existential_ast3/v6.sail:37.71-86:
    | 37 |  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
    |    |                                                                       ^-------------^ bound here
-   |    | has constraint: (0 <= 'ex360 & 'ex360 <= 63)
+   |    | has constraint: (0 <= 'ex359 & 'ex359 <= 63)

test/typecheck/pass/if_infer/v1.expect

@@ -5,7 +5,7 @@
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex241# & 'ex241# < 3)
+   |    * (0 <= 'ex240# & 'ex240# < 3)
    | * plain_vector_access
    |    Could not unify vector('n, 'a) and bitvector(3)
    | 

test/typecheck/pass/if_infer/v2.expect

@@ -5,7 +5,7 @@
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex241# & 'ex241# < 4)
+   |    * (0 <= 'ex240# & 'ex240# < 4)
    | * plain_vector_access
    |    Could not unify vector('n, 'a) and bitvector(4)
    | 

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