summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/process_file.ml4
-rw-r--r--src/process_file.mli1
-rw-r--r--src/sail.ml3
-rw-r--r--src/type_check_new.ml72
-rw-r--r--src/type_check_new.mli5
-rw-r--r--test/typecheck/fail/modify_assignment1.sail8
-rw-r--r--test/typecheck/fail/modify_assignment2.sail8
-rw-r--r--test/typecheck/fail/modify_let_bound.sail16
-rw-r--r--test/typecheck/fail/modify_type_chain1.sail8
-rw-r--r--test/typecheck/fail/modify_type_chain2.sail8
-rw-r--r--test/typecheck/fail/modify_type_chain3.sail8
-rw-r--r--test/typecheck/fail/modify_type_chain4.sail8
-rw-r--r--test/typecheck/fail/modify_type_chain5.sail8
-rw-r--r--test/typecheck/fail/reg_mod.sail11
-rw-r--r--test/typecheck/pass/modify_assignment1.sail8
-rw-r--r--test/typecheck/pass/modify_type_chain.sail8
-rw-r--r--test/typecheck/pass/reg_mod.sail11
17 files changed, 187 insertions, 8 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index 12a067e1..63e42219 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -89,6 +89,7 @@ let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tann
Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
let opt_new_typecheck = ref false
+let opt_just_check = ref false
let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs =
let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
@@ -102,6 +103,9 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
if !opt_new_typecheck
then let _ = Type_check_new.check Type_check_new.initial_env defs in ()
else ();
+ if !opt_just_check
+ then exit 0
+ else ();
Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs
let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs
diff --git a/src/process_file.mli b/src/process_file.mli
index bfc719cc..4c703dd2 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -49,6 +49,7 @@ val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.
val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
val opt_new_typecheck : bool ref
+val opt_just_check : bool ref
type out_type =
| Lem_ast_out
diff --git a/src/sail.ml b/src/sail.ml
index 343a677c..0bdcf4ab 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -89,6 +89,9 @@ let options = Arg.align ([
( "-new_typecheck",
Arg.Set opt_new_typecheck,
" use new typechecker with Z3 constraint solving (experimental)");
+ ( "-just_check",
+ Arg.Tuple [Arg.Set opt_new_typecheck; Arg.Set opt_just_check],
+ " terminate immediately after typechecking, implies -new_typecheck");
( "-v",
Arg.Set opt_print_version,
" print version");
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 01527f73..495d52b7 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -45,7 +45,7 @@ open Ast
open Util
open Big_int
-let debug = ref 1
+let debug = ref 2
let depth = ref 0
let rec indent n = match n with
@@ -333,13 +333,17 @@ module KBindings = Map.Make(Kid)
module KidSet = Set.Make(Kid)
type mut = Immutable | Mutable
-
+
+type lvar = Register of typ | Local of mut * typ | Unbound
+
module Env : sig
type t
val get_val_spec : id -> t -> typquant * typ
val add_val_spec : id -> typquant * typ -> t -> t
val get_local : id -> t -> mut * typ
val add_local : id -> mut * typ -> t -> t
+ val get_register : id -> t -> typ
+ val add_register : id -> typ -> t -> t
val is_mutable : id -> t -> bool
val get_constraints : t -> n_constraint list
val add_constraint : n_constraint -> t -> t
@@ -352,6 +356,7 @@ module Env : sig
val get_default_order : t -> order
val set_default_order_inc : t -> t
val set_default_order_dec : t -> t
+ val lookup_id : id -> t -> lvar
val fresh_kid : t -> kid
val expand_synonyms : t -> typ -> typ
val empty : t
@@ -359,6 +364,7 @@ end = struct
type t =
{ top_val_specs : (typquant * typ) Bindings.t;
locals : (mut * typ) Bindings.t;
+ registers : typ Bindings.t;
typ_vars : base_kind_aux KBindings.t;
typ_synonyms : (typ_arg list -> typ) Bindings.t;
constraints : n_constraint list;
@@ -369,6 +375,7 @@ end = struct
let empty =
{ top_val_specs = Bindings.empty;
locals = Bindings.empty;
+ registers = Bindings.empty;
typ_vars = KBindings.empty;
typ_synonyms = Bindings.empty;
constraints = [];
@@ -428,6 +435,30 @@ end = struct
{ env with locals = Bindings.add id mtyp env.locals }
end
+ let get_register id env =
+ try Bindings.find id env.registers with
+ | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id)
+
+ let add_register id typ env =
+ if Bindings.mem id env.registers
+ then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
+ else
+ begin
+ typ_print ("Adding register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ);
+ { env with registers = Bindings.add id typ env.registers }
+ end
+
+ let lookup_id id env =
+ try
+ let (mut, typ) = Bindings.find id env.locals in
+ Local (mut, typ)
+ with
+ | Not_found ->
+ begin
+ try Register (Bindings.find id env.registers) with
+ | Not_found -> Unbound
+ end
+
let get_typ_var kid env =
try KBindings.find kid env.typ_vars with
| Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
@@ -919,11 +950,35 @@ let rec bind_pat env (P_aux (pat_aux, (l, _)) as pat) (Typ_aux (typ_aux, _) as t
and bind_lexp env (LEXP_aux (lexp_aux, (l, _))) typ =
let annot_lexp lexp typ = LEXP_aux (lexp, (l, Some (env, typ))) in
match lexp_aux with
- | LEXP_id v -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
+ | LEXP_id v ->
+ begin
+ match Env.lookup_id v env with
+ | Local (Immutable, _) -> typ_error l ("Cannot modify or shadow let-bound constant " ^ string_of_id v)
+ | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
+ | Register vtyp -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
+ | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
+ end
| LEXP_cast (typ_annot, v) ->
begin
- subtyp l env typ typ_annot;
- annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
+ match Env.lookup_id v env with
+ | Local (Immutable, _) -> typ_error l ("Cannot modify or shadow let-bound constant " ^ string_of_id v)
+ | Local (Mutable, vtyp) ->
+ begin
+ subtyp l env typ typ_annot;
+ subtyp l env typ_annot vtyp;
+ annot_lexp (LEXP_cast (typ_annot, v)) typ, env
+ end
+ | Register vtyp ->
+ begin
+ subtyp l env typ typ_annot;
+ subtyp l env typ_annot vtyp;
+ annot_lexp (LEXP_cast (typ_annot, v)) typ, env
+ end
+ | Unbound ->
+ begin
+ subtyp l env typ typ_annot;
+ annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
+ end
end
| LEXP_tup lexps ->
begin
@@ -1223,9 +1278,10 @@ let rec check_def env def =
| DEF_val letdef -> cd_err ()
| DEF_spec vs -> check_val_spec env vs
| DEF_default default -> check_default env default
- | DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) -> cd_err ()
- | DEF_reg_dec(DEC_aux(DEC_alias(id,aspec), (l,annot))) -> cd_err ()
- | DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))) -> cd_err ()
+ | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, _))) ->
+ DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, None))), Env.add_register id typ env
+ | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err ()
+ | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
| DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
| DEF_comm (DC_comm str) -> DEF_comm (DC_comm str), env
| DEF_comm (DC_comm_struct def) ->
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index 54140267..bcf95b34 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -45,12 +45,16 @@ open Ast
type mut = Immutable | Mutable
+type lvar = Register of typ | Local of mut * typ | Unbound
+
module Env : sig
type t
val get_val_spec : id -> t -> typquant * typ
val add_val_spec : id -> typquant * typ -> t -> t
val get_local : id -> t -> mut * typ
val add_local : id -> mut * typ -> t -> t
+ val get_register : id -> t -> typ
+ val add_register : id -> typ -> t -> t
val is_mutable : id -> t -> bool
val get_constraints : t -> n_constraint list
val add_constraint : n_constraint -> t -> t
@@ -60,6 +64,7 @@ module Env : sig
val add_ret_typ : typ -> t -> t
val add_typ_synonym : id -> (typ_arg list -> typ) -> t -> t
val get_typ_synonym : id -> t -> typ_arg list -> typ
+ val lookup_id : id -> t -> lvar
val fresh_kid : t -> kid
val expand_synonyms : t -> typ -> typ
val empty : t
diff --git a/test/typecheck/fail/modify_assignment1.sail b/test/typecheck/fail/modify_assignment1.sail
new file mode 100644
index 00000000..99adc95c
--- /dev/null
+++ b/test/typecheck/fail/modify_assignment1.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ z := 9;
+ z := 10
+} \ No newline at end of file
diff --git a/test/typecheck/fail/modify_assignment2.sail b/test/typecheck/fail/modify_assignment2.sail
new file mode 100644
index 00000000..6551afff
--- /dev/null
+++ b/test/typecheck/fail/modify_assignment2.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ ([|0:9|]) z := 9;
+ z := ([|0:10|]) 10
+} \ No newline at end of file
diff --git a/test/typecheck/fail/modify_let_bound.sail b/test/typecheck/fail/modify_let_bound.sail
new file mode 100644
index 00000000..a2ad1b98
--- /dev/null
+++ b/test/typecheck/fail/modify_let_bound.sail
@@ -0,0 +1,16 @@
+
+default Order dec
+
+register bit[3] test
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ let i = 10 in {
+ i := 20
+ };
+ z := 9;
+ z := 10;
+ test := 3
+} \ No newline at end of file
diff --git a/test/typecheck/fail/modify_type_chain1.sail b/test/typecheck/fail/modify_type_chain1.sail
new file mode 100644
index 00000000..3fff3b59
--- /dev/null
+++ b/test/typecheck/fail/modify_type_chain1.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ ([|0:10|]) z := 9;
+ ([|0:9|]) z := ([|0:10|]) 8
+} \ No newline at end of file
diff --git a/test/typecheck/fail/modify_type_chain2.sail b/test/typecheck/fail/modify_type_chain2.sail
new file mode 100644
index 00000000..085e7db5
--- /dev/null
+++ b/test/typecheck/fail/modify_type_chain2.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ ([|0:10|]) z := 9;
+ ([|0:7|]) z := ([|0:8|]) 8
+} \ No newline at end of file
diff --git a/test/typecheck/fail/modify_type_chain3.sail b/test/typecheck/fail/modify_type_chain3.sail
new file mode 100644
index 00000000..cfe532aa
--- /dev/null
+++ b/test/typecheck/fail/modify_type_chain3.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ ([|0:6|]) z := 9;
+ ([|0:7|]) z := ([|0:8|]) 8
+} \ No newline at end of file
diff --git a/test/typecheck/fail/modify_type_chain4.sail b/test/typecheck/fail/modify_type_chain4.sail
new file mode 100644
index 00000000..c36a9086
--- /dev/null
+++ b/test/typecheck/fail/modify_type_chain4.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ ([|0:10|]) z := 9;
+ ([|0:11|]) z := ([|0:13|]) 8
+} \ No newline at end of file
diff --git a/test/typecheck/fail/modify_type_chain5.sail b/test/typecheck/fail/modify_type_chain5.sail
new file mode 100644
index 00000000..3c3076a4
--- /dev/null
+++ b/test/typecheck/fail/modify_type_chain5.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ ([|0:10|]) z := 9;
+ ([|0:9|]) z := ([|0:13|]) 8
+} \ No newline at end of file
diff --git a/test/typecheck/fail/reg_mod.sail b/test/typecheck/fail/reg_mod.sail
new file mode 100644
index 00000000..24b318b4
--- /dev/null
+++ b/test/typecheck/fail/reg_mod.sail
@@ -0,0 +1,11 @@
+
+register [|0:10|] reg
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ reg := 9;
+ reg := 10;
+ reg := 8
+} \ No newline at end of file
diff --git a/test/typecheck/pass/modify_assignment1.sail b/test/typecheck/pass/modify_assignment1.sail
new file mode 100644
index 00000000..1c7ab614
--- /dev/null
+++ b/test/typecheck/pass/modify_assignment1.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ ([|0:10|]) z := 9;
+ z := ([|0:9|]) 8
+} \ No newline at end of file
diff --git a/test/typecheck/pass/modify_type_chain.sail b/test/typecheck/pass/modify_type_chain.sail
new file mode 100644
index 00000000..14651787
--- /dev/null
+++ b/test/typecheck/pass/modify_type_chain.sail
@@ -0,0 +1,8 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+ ([|0:10|]) z := 9;
+ ([|0:9|]) z := ([|0:8|]) 8
+} \ No newline at end of file
diff --git a/test/typecheck/pass/reg_mod.sail b/test/typecheck/pass/reg_mod.sail
new file mode 100644
index 00000000..37c8d890
--- /dev/null
+++ b/test/typecheck/pass/reg_mod.sail
@@ -0,0 +1,11 @@
+
+register [|0:10|] reg
+
+val unit -> unit effect {wreg} test
+
+function unit test () =
+{
+ reg := 9;
+ reg := 10;
+ reg := 8
+} \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 18:23:24 +0000