From 1edd0e73a7d19904639341fd360fff5fa3ff4fec Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 5 Nov 2019 18:04:51 +0000
Subject: Make sure we correctly forbid recursive datatypes that we don't want
 to support

Ensure we give a nice error message that explains that recursive types are forbidden

```
Type error:
[struct_rec.sail]:3:10-11
3 |  field : S
  |          ^
  | Undefined type S
  | This error was caused by:
  | [struct_rec.sail]:2:0-4:1
  | 2 |struct S = {
  |   |^-----------
  | 4 |}
  |   |^
  |   | Recursive types are not allowed
```

The theorem prover backends create a special register_value union that
can be recursive, so we make sure to special case that.
---
 src/gdbmi.ml                                     |  7 +++++
 src/type_check.ml                                | 33 ++++++++++++++++++------
 src/type_error.ml                                |  2 +-
 test/typecheck/fail/struct_rec.expect            | 13 ++++++++++
 test/typecheck/fail/struct_rec.sail              |  4 +++
 test/typecheck/fail/synonym_rec.expect           | 11 ++++++++
 test/typecheck/fail/synonym_rec.sail             |  2 ++
 test/typecheck/fail/union_rec.expect             | 13 ++++++++++
 test/typecheck/fail/union_rec.sail               |  4 +++
 test/typecheck/fail/union_recf.expect            | 13 ++++++++++
 test/typecheck/fail/union_recf.sail              |  4 +++
 test/typecheck/pass/constrained_struct/v1.expect |  5 ++++
 test/typecheck/pass/existential_ast/v3.expect    |  2 +-
 test/typecheck/pass/reg_32_64/v2.expect          |  2 +-
 test/typecheck/pass/union_recf_ok.sail           |  4 +++
 test/typecheck/run_tests.sh                      | 18 +++++++++++++
 test/typecheck/update_errors.sh                  | 13 +++++++---
 17 files changed, 136 insertions(+), 14 deletions(-)
 create mode 100644 test/typecheck/fail/struct_rec.expect
 create mode 100644 test/typecheck/fail/struct_rec.sail
 create mode 100644 test/typecheck/fail/synonym_rec.expect
 create mode 100644 test/typecheck/fail/synonym_rec.sail
 create mode 100644 test/typecheck/fail/union_rec.expect
 create mode 100644 test/typecheck/fail/union_rec.sail
 create mode 100644 test/typecheck/fail/union_recf.expect
 create mode 100644 test/typecheck/fail/union_recf.sail
 create mode 100644 test/typecheck/pass/union_recf_ok.sail

diff --git a/src/gdbmi.ml b/src/gdbmi.ml
index bcefb002..faf3ac11 100644
--- a/src/gdbmi.ml
+++ b/src/gdbmi.ml
@@ -179,6 +179,13 @@ let gdb_effect_interp session state eff =
      | None ->
         cont (Bindings.find (mk_id name) gstate.registers) state
      end
+  | Write_reg (name, v, cont) ->
+     let id = mk_id name in
+     if Bindings.mem id gstate.registers then
+       let state' = (lstate, { gstate with registers = Bindings.add id v gstate.registers }) in
+       cont () state'
+     else
+       failwith ("Write of nonexistent register: " ^ name)
   | _ ->
      failwith "Unsupported in GDB state"
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 93b6da36..1f27a0ab 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1059,7 +1059,7 @@ end = struct
     | Not_found -> typ_error env (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist")
 
   let is_enum id env = Bindings.mem id env.enums
-                 
+
   let is_record id env = Bindings.mem id env.records
 
   let get_record id env = Bindings.find id env.records
@@ -5074,37 +5074,54 @@ let fold_union_quant quants (QI_aux (qi, l)) =
   | QI_id kind_id -> quants @ [kinded_id_arg kind_id]
   | _ -> quants
 
-let check_type_union env variant typq (Tu_aux (tu, l)) =
+(* We wrap this around wf_binding checks that aim to forbid recursive
+   types to explain any error messages raised if the well-formedness
+   check fails. *)
+let forbid_recursive_types type_l f =
+  try f () with
+  | Type_error (env, l, err) ->
+     raise (Type_error (env, l, Err_because (err, type_l, Err_other "Recursive types are not allowed")))
+
+let check_type_union u_l non_rec_env env variant typq (Tu_aux (tu, l)) =
   let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in
   match tu with
   | Tu_ty_id (Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) as typ, v) ->
      let typq = mk_typquant (List.map (mk_qi_id K_type) (KidSet.elements (tyvars_of_typ typ))) in
+     forbid_recursive_types u_l (fun () -> wf_binding l non_rec_env (typq, tuple_typ arg_typ));
      wf_binding l env (typq, typ);
      env
      |> Env.add_union_id v (typq, typ)
      |> Env.add_val_spec v (typq, typ)
   | Tu_ty_id (arg_typ, v) ->
      let typ' = mk_typ (Typ_fn ([arg_typ], ret_typ, no_effect)) in
+     forbid_recursive_types u_l (fun () -> wf_binding l non_rec_env (typq, arg_typ));
      wf_binding l env (typq, typ');
      env
      |> Env.add_union_id v (typq, typ')
      |> Env.add_val_spec v (typq, typ')
 
-(* FIXME: This code is duplicated with general kind-checking code in environment, can they be merged? *)
-
 let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
   fun env (TD_aux (tdef, (l, _))) ->
   let td_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
   match tdef with
   | TD_abbrev (id, typq, typ_arg) ->
+     begin match typ_arg with
+     | A_aux (A_typ typ, a_l) ->
+        forbid_recursive_types l (fun () -> wf_binding a_l env (typq, typ));
+     | _ -> ()
+     end;
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id typq typ_arg env
   | TD_record (id, typq, fields, _) ->
+     forbid_recursive_types l (fun () -> List.iter (fun (Typ_aux (_, l) as field, _) -> wf_binding l env (typq, field)) fields);
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env
   | TD_variant (id, typq, arms, _) ->
+     let rec_env = Env.add_variant id (typq, arms) env in
+     (* register_value is a special type used by theorem prover
+        backends that we allow to be recursive. *)
+     let non_rec_env = if string_of_id id = "register_value" then rec_env else env in
      let env =
-       env
-       |> Env.add_variant id (typq, arms)
-       |> (fun env -> List.fold_left (fun env tu -> check_type_union env id typq tu) env arms)
+       rec_env
+       |> (fun env -> List.fold_left (fun env tu -> check_type_union l non_rec_env env id typq tu) env arms)
      in
      [DEF_type (TD_aux (tdef, (l, None)))], env
   | TD_enum (id, ids, _) ->
@@ -5137,7 +5154,7 @@ and check_scattered : 'a. Env.t -> 'a scattered_def -> (tannot def) list * Env.t
      [DEF_scattered (SD_aux (SD_unioncl (id, tu), (l, None)))],
      let env = Env.add_variant_clause id tu env in
      let typq, _ = Env.get_variant id env in
-     check_type_union env id typq tu
+     check_type_union l env env id typq tu
   | SD_funcl (FCL_aux (FCL_Funcl (id, _), (l, _)) as funcl) ->
      let typq, typ = Env.get_val_spec id env in
      let funcl_env = add_typquant l typq env in
diff --git a/src/type_error.ml b/src/type_error.ml
index eed1379a..6205302e 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -107,7 +107,7 @@ let message_of_type_error =
   let rec msg = function
     | Err_because (err, l', err') ->
        Seq [msg err;
-            Line "This error occured because of a previous error:";
+            Line "This error was caused by:";
             Location (l', msg err')]
 
     | Err_other str -> Line str
diff --git a/test/typecheck/fail/struct_rec.expect b/test/typecheck/fail/struct_rec.expect
new file mode 100644
index 00000000..6daa067d
--- /dev/null
+++ b/test/typecheck/fail/struct_rec.expect
@@ -0,0 +1,13 @@
+Type error:
+[struct_rec.sail]:3:10-11
+3 |  field : S
+  |          ^
+  | Undefined type S
+  | This error was caused by:
+  | [struct_rec.sail]:2:0-4:1
+  | 2 |struct S = {
+  |   |^-----------
+  | 4 |}
+  |   |^
+  |   | Recursive types are not allowed
+  | 
diff --git a/test/typecheck/fail/struct_rec.sail b/test/typecheck/fail/struct_rec.sail
new file mode 100644
index 00000000..01c29d6d
--- /dev/null
+++ b/test/typecheck/fail/struct_rec.sail
@@ -0,0 +1,4 @@
+
+struct S = {
+  field : S
+}
diff --git a/test/typecheck/fail/synonym_rec.expect b/test/typecheck/fail/synonym_rec.expect
new file mode 100644
index 00000000..5d205606
--- /dev/null
+++ b/test/typecheck/fail/synonym_rec.expect
@@ -0,0 +1,11 @@
+Type error:
+[synonym_rec.sail]:2:9-10
+2 |type T = T
+  |         ^
+  | Undefined type T
+  | This error was caused by:
+  | [synonym_rec.sail]:2:0-10
+  | 2 |type T = T
+  |   |^--------^
+  |   | Recursive types are not allowed
+  | 
diff --git a/test/typecheck/fail/synonym_rec.sail b/test/typecheck/fail/synonym_rec.sail
new file mode 100644
index 00000000..54906418
--- /dev/null
+++ b/test/typecheck/fail/synonym_rec.sail
@@ -0,0 +1,2 @@
+
+type T = T
diff --git a/test/typecheck/fail/union_rec.expect b/test/typecheck/fail/union_rec.expect
new file mode 100644
index 00000000..2d50cea6
--- /dev/null
+++ b/test/typecheck/fail/union_rec.expect
@@ -0,0 +1,13 @@
+Type error:
+[union_rec.sail]:3:9-10
+3 |  Ctor : U
+  |         ^
+  | Undefined type U
+  | This error was caused by:
+  | [union_rec.sail]:2:0-4:1
+  | 2 |union U = {
+  |   |^----------
+  | 4 |}
+  |   |^
+  |   | Recursive types are not allowed
+  | 
diff --git a/test/typecheck/fail/union_rec.sail b/test/typecheck/fail/union_rec.sail
new file mode 100644
index 00000000..7ca7b8e9
--- /dev/null
+++ b/test/typecheck/fail/union_rec.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : U
+}
diff --git a/test/typecheck/fail/union_recf.expect b/test/typecheck/fail/union_recf.expect
new file mode 100644
index 00000000..b07910ba
--- /dev/null
+++ b/test/typecheck/fail/union_recf.expect
@@ -0,0 +1,13 @@
+Type error:
+[union_recf.sail]:3:9-10
+3 |  Ctor : U -> U
+  |         ^
+  | Undefined type U
+  | This error was caused by:
+  | [union_recf.sail]:2:0-4:1
+  | 2 |union U = {
+  |   |^----------
+  | 4 |}
+  |   |^
+  |   | Recursive types are not allowed
+  | 
diff --git a/test/typecheck/fail/union_recf.sail b/test/typecheck/fail/union_recf.sail
new file mode 100644
index 00000000..f64ca675
--- /dev/null
+++ b/test/typecheck/fail/union_recf.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : U -> U
+}
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index 8c95193d..bf498a36 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -3,4 +3,9 @@ Type error:
 10 |type MyStruct64 = MyStruct(65)
    |                  ^------^
    | Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
+   | This error was caused by:
+   | [constrained_struct/v1.sail]:10:0-30
+   | 10 |type MyStruct64 = MyStruct(65)
+   |    |^----------------------------^
+   |    | Recursive types are not allowed
    | 
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index ca83adb9..8d061933 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex273#)
+   | * datasize('ex276#)
    | 
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
index 24439bed..90166904 100644
--- a/test/typecheck/pass/reg_32_64/v2.expect
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -5,7 +5,7 @@ Type error:
    | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data
    | Coercion failed because:
    | Mismatched argument types in subtype check
-   | This error occured because of a previous error:
+   | This error was caused by:
    | [reg_32_64/v2.sail]:21:2-15
    | 21 |  (*R)['d .. 0] = data
    |    |  ^-----------^
diff --git a/test/typecheck/pass/union_recf_ok.sail b/test/typecheck/pass/union_recf_ok.sail
new file mode 100644
index 00000000..0f415601
--- /dev/null
+++ b/test/typecheck/pass/union_recf_ok.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : int -> U
+}
\ No newline at end of file
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index e5650646..adc30c42 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -87,6 +87,24 @@ do
     done
 done
 
+for file in $DIR/fail/*.sail;
+do
+    pushd $DIR/fail > /dev/null;
+    if $SAILDIR/sail -no_memo_z3 $(basename $file) 2> result
+    then
+        red "Expected failure, but $i $(basename $file) passed" "fail"
+    else
+        if diff ${file%.sail}.expect result;
+        then
+            green "failing $i $(basename $file)" "pass"
+        else
+            yellow "failing $i $(basename $file)" "unexpected error"
+        fi
+    fi;
+    rm -f result;
+    popd > /dev/null
+done
+
 finish_suite "Typechecking tests"
 
 printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/typecheck/update_errors.sh b/test/typecheck/update_errors.sh
index ba436daf..1d174797 100755
--- a/test/typecheck/update_errors.sh
+++ b/test/typecheck/update_errors.sh
@@ -10,8 +10,15 @@ do
     shopt -s nullglob;
     for file in $DIR/pass/${i%.sail}/*.sail;
     do
-	pushd $DIR/pass > /dev/null;
-	$SAILDIR/sail ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
-	popd > /dev/null
+        pushd $DIR/pass > /dev/null;
+        $SAILDIR/sail -no_memo_z3 ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
+        popd > /dev/null
     done
 done
+
+for file in $DIR/fail/*.sail;
+do
+    pushd $DIR/fail > /dev/null;
+    $SAILDIR/sail -no_memo_z3 $(basename $file) 2> ${file%.sail}.expect || true;
+    popd > /dev/null
+done
-- 
cgit v1.2.3