From 029ade91124c138be42a98dc05919661f013b154 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 6 Dec 2024 14:37:12 +0000 Subject: [PATCH 01/54] First batch of features --- lib/vector.sail | 2 + src/sail_lean_backend/Sail/Sail.lean | 6 ++ src/sail_lean_backend/pretty_print_lean.ml | 18 +++++- test/lean/bitfield.lean.expected | 69 ++++++++++++++++++++++ test/lean/bitfield.sail | 11 ++++ 5 files changed, 104 insertions(+), 2 deletions(-) create mode 100644 test/lean/bitfield.lean.expected create mode 100644 test/lean/bitfield.sail diff --git a/lib/vector.sail b/lib/vector.sail index 59c29d43d..ef14f7fa2 100644 --- a/lib/vector.sail +++ b/lib/vector.sail @@ -299,6 +299,7 @@ val subrange_bits = pure { interpreter: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec", + lean: "Sail.BitVec.extractLsb", _: "vector_subrange" } : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o)) -> bits('m - 'o + 1) @@ -321,6 +322,7 @@ val update_subrange_bits = pure { interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec", + lean: "Sail.BitVec.update_subrange", _: "vector_update_subrange" } : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o), bits('m - ('o - 1))) -> bits('n) $else diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 8cf943fdb..b7af3a9dc 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -19,5 +19,11 @@ def truncate {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' := def truncateLsb {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' := x.extractLsb' (w - w') w' +def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := + x.extractLsb hi lo + +def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := + sorry + end BitVec end Sail diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 868714246..978645819 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -137,12 +137,19 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = parens (string "BitVec " ^^ doc_nexp ctxt m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) + | Typ_app (Id_aux (Id "register", _), t_app) -> string "Register " ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts) | Typ_id (Id_aux (Id id, _)) -> string id | _ -> failwith ("Type " ^ string_of_typ_con typ ^ " " ^ string_of_typ typ ^ " not translatable yet.") +and doc_typ_app ctxt (A_aux (t, _) as typ) = + match t with + | A_typ t' -> doc_typ ctxt t' + | A_bool nc -> failwith ("Constraint " ^ string_of_n_constraint nc ^ "not translatable yet.") + | A_nexp m -> doc_nexp ctxt m + let rec captured_typ_var ((i, Typ_aux (t, _)) as typ) = match t with | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) @@ -254,8 +261,8 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *) | E_lit l -> doc_lit l | E_app (Id_aux (Id "internal_pick", _), _) -> - string "sorry" (* TODO replace by actual implementation of internal_pick *) - | E_internal_plet _ -> string "sorry" (* TODO replace by actual implementation of internal_plet *) + string "sorry /- internal_pick -/" (* TODO replace by actual implementation of internal_pick *) + | E_internal_plet _ -> string "sorry /- internal_plet -/" (* TODO replace by actual implementation of internal_plet *) | E_app (f, args) -> let d_id = if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") @@ -274,8 +281,15 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | _ -> failwith "Let pattern not translatable yet." in nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e + | E_struct fexps -> let args = List.map (doc_fexp ctxt) fexps in + braces (separate comma args) + | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id + | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in + braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") +and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp + let doc_binder ctxt i t = let paranthesizer = match t with diff --git a/test/lean/bitfield.lean.expected b/test/lean/bitfield.lean.expected new file mode 100644 index 000000000..a92fe23f3 --- /dev/null +++ b/test/lean/bitfield.lean.expected @@ -0,0 +1,69 @@ +import Sail.sail + +structure cr_type where + bits : BitVec 8 + + +def undefined_cr_type (lit : Unit) : cr_type := + sorry + +def Mk_cr_type (v : BitVec 8) : cr_type := + {bits := v} + +def _get_cr_type_bits (v : cr_type) : BitVec 8 := + (Sail.BitVec.extractLsb v.bits (HSub.hSub 8 1) 0) + +def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)} + +def _set_cr_type_bits (r_ref : Register cr_type) (v : BitVec 8) : Unit := + sorry + +def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := + (Sail.BitVec.extractLsb v.bits 7 4) + +def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)} + +def _set_cr_type_CR0 (r_ref : Register cr_type) (v : BitVec 4) : Unit := + sorry + +def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := + (Sail.BitVec.extractLsb v.bits 3 2) + +def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)} + +def _set_cr_type_CR1 (r_ref : Register cr_type) (v : BitVec 2) : Unit := + sorry + +def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := + (Sail.BitVec.extractLsb v.bits 1 0) + +def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)} + +def _set_cr_type_CR3 (r_ref : Register cr_type) (v : BitVec 2) : Unit := + sorry + +def _get_cr_type_GT (v : cr_type) : BitVec 1 := + (Sail.BitVec.extractLsb v.bits 6 6) + +def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)} + +def _set_cr_type_GT (r_ref : Register cr_type) (v : BitVec 1) : Unit := + sorry + +def _get_cr_type_LT (v : cr_type) : BitVec 1 := + (Sail.BitVec.extractLsb v.bits 7 7) + +def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)} + +def _set_cr_type_LT (r_ref : Register cr_type) (v : BitVec 1) : Unit := + sorry + +def initialize_registers : Unit := + () + diff --git a/test/lean/bitfield.sail b/test/lean/bitfield.sail new file mode 100644 index 000000000..4182b05c8 --- /dev/null +++ b/test/lean/bitfield.sail @@ -0,0 +1,11 @@ +default Order dec + +$include + +bitfield cr_type : bits(8) = { + CR0 : 7 .. 4, + LT : 7, + GT : 6, + CR1 : 3 .. 2, + CR3 : 1 .. 0 +} \ No newline at end of file From c6ccac3fd1d493a851166865bea28a66b0773764 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 6 Dec 2024 16:06:07 +0000 Subject: [PATCH 02/54] Adding features --- lib/arith.sail | 9 +++---- src/bin/dune | 8 ++++++- src/sail_lean_backend/Sail/bitvec.lean | 25 +++++++++++++++++++ src/sail_lean_backend/Sail/registers.lean | 29 +++++++++++++++++++++++ 4 files changed, 66 insertions(+), 5 deletions(-) create mode 100644 src/sail_lean_backend/Sail/bitvec.lean create mode 100644 src/sail_lean_backend/Sail/registers.lean diff --git a/lib/arith.sail b/lib/arith.sail index 202d2ec5a..3bb48e3b2 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -51,19 +51,19 @@ $include // ***** Addition ***** -val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", _: "add_int"} : forall 'n 'm. +val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", lean: "HAdd.hAdd", _: "add_int"} : forall 'n 'm. (int('n), int('m)) -> int('n + 'm) -val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add", _: "add_int"} : (int, int) -> int +val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add", lean: "HAdd.hAdd", _: "add_int"} : (int, int) -> int overload operator + = {add_atom, add_int} // ***** Subtraction ***** -val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", _: "sub_int"} : forall 'n 'm. +val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "HSub.hSub", _: "sub_int"} : forall 'n 'm. (int('n), int('m)) -> int('n - 'm) -val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", _: "sub_int"} : (int, int) -> int +val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", lean: "HSub.hSub", _: "sub_int"} : (int, int) -> int overload operator - = {sub_atom, sub_int} @@ -71,6 +71,7 @@ val sub_nat = pure { ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", lem: "integerMinus", coq: "Z.sub", + lean: "HSub.hSub", _: "sub_nat" } : (nat, nat) -> nat diff --git a/src/bin/dune b/src/bin/dune index 9a00105c0..7f6006737 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -248,4 +248,10 @@ src/gen_lib/sail2_values.lem) (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as - src/sail_lean_backend/Sail/Sail.lean))) + src/sail_lean_backend/Sail/Sail.lean) + (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean + as + src/sail_lean_backend/Sail/bitvec.lean) + (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean + as + src/sail_lean_backend/Sail/registers.lean))) diff --git a/src/sail_lean_backend/Sail/bitvec.lean b/src/sail_lean_backend/Sail/bitvec.lean new file mode 100644 index 000000000..7a0ec1e06 --- /dev/null +++ b/src/sail_lean_backend/Sail/bitvec.lean @@ -0,0 +1,25 @@ +namespace Sail +namespace BitVec + +def length {w: Nat} (_: BitVec w): Nat := w + +def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := + x.signExtend w' + +def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := + x.zeroExtend w' + +def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := + x.truncate w' + +def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := + x.extractLsb' 0 w' + +def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := + x.extractLsb hi lo + +def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := + sorry + +end BitVec +end Sail diff --git a/src/sail_lean_backend/Sail/registers.lean b/src/sail_lean_backend/Sail/registers.lean new file mode 100644 index 000000000..26d122546 --- /dev/null +++ b/src/sail_lean_backend/Sail/registers.lean @@ -0,0 +1,29 @@ + +inductive register where + | Register : String → /- name -/ + Nat → /- length -/ + Nat → /- start index -/ + Bool → /- is increasing -/ + List register_field_index + → register + | UndefinedRegister : Nat → register /- length -/ + | RegisterPair : register → register → register + +structure register_ref (regstate regval a: Type) where + name: String + read_from: regstate -> a + write_to: a -> regstate -> regstate + of_regval: regval -> Option a + regval_of: a -> regval + +def read_reg {s rv a e} (reg : register_ref s rv a) : Monad e := + let k v := + match reg.of_regval v with + | some v => some v + | none => none + Read_reg reg.(name) k. + +def reg_deref {s rv a e} := @read_reg s rv a e. + +def write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv unit e := + Write_reg reg.(name) (reg.(regval_of) v) (Done tt). From c7573a81da1e04ff3db9ac26ead254e372f8e908 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 6 Dec 2024 16:08:22 +0000 Subject: [PATCH 03/54] formatting --- src/bin/dune | 4 ++-- src/sail_lean_backend/pretty_print_lean.ml | 10 ++++++---- test/lean/bitfield.sail | 2 +- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/bin/dune b/src/bin/dune index 7f6006737..a973f17a7 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -249,9 +249,9 @@ (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as src/sail_lean_backend/Sail/Sail.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean + (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean as src/sail_lean_backend/Sail/bitvec.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean + (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean as src/sail_lean_backend/Sail/registers.lean))) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 978645819..17a5ba709 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -281,11 +281,13 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | _ -> failwith "Let pattern not translatable yet." in nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e - | E_struct fexps -> let args = List.map (doc_fexp ctxt) fexps in - braces (separate comma args) + | E_struct fexps -> + let args = List.map (doc_fexp ctxt) fexps in + braces (separate comma args) | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id - | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in - braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args) + | E_struct_update (exp, fexps) -> + let args = List.map (doc_fexp ctxt) fexps in + braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp diff --git a/test/lean/bitfield.sail b/test/lean/bitfield.sail index 4182b05c8..2969f5927 100644 --- a/test/lean/bitfield.sail +++ b/test/lean/bitfield.sail @@ -8,4 +8,4 @@ bitfield cr_type : bits(8) = { GT : 6, CR1 : 3 .. 2, CR3 : 1 .. 0 -} \ No newline at end of file +} From 32bb33f63a5d130ecabae347c2fe7e526e11a126 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 9 Dec 2024 15:31:54 +0000 Subject: [PATCH 04/54] update_subrange implementation --- src/sail_lean_backend/Sail/bitvec.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/Sail/bitvec.lean b/src/sail_lean_backend/Sail/bitvec.lean index 7a0ec1e06..ae1c156ae 100644 --- a/src/sail_lean_backend/Sail/bitvec.lean +++ b/src/sail_lean_backend/Sail/bitvec.lean @@ -18,8 +18,13 @@ def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := x.extractLsb hi lo +def update_subrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w := + let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start) + let y' := mask ||| ((y.zeroExtend w) <<< start) + x &&& y' + def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := - sorry + update_subrange' x lo _ y end BitVec end Sail From 5dd4394e474474ce26760681dc740cd4c4bf2053 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 9 Dec 2024 15:45:46 +0000 Subject: [PATCH 05/54] Cleanup registers --- src/sail_lean_backend/Sail/registers.lean | 12 ------------ src/sail_lean_backend/pretty_print_lean.ml | 2 +- 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/src/sail_lean_backend/Sail/registers.lean b/src/sail_lean_backend/Sail/registers.lean index 26d122546..92552ca58 100644 --- a/src/sail_lean_backend/Sail/registers.lean +++ b/src/sail_lean_backend/Sail/registers.lean @@ -15,15 +15,3 @@ structure register_ref (regstate regval a: Type) where write_to: a -> regstate -> regstate of_regval: regval -> Option a regval_of: a -> regval - -def read_reg {s rv a e} (reg : register_ref s rv a) : Monad e := - let k v := - match reg.of_regval v with - | some v => some v - | none => none - Read_reg reg.(name) k. - -def reg_deref {s rv a e} := @read_reg s rv a e. - -def write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv unit e := - Write_reg reg.(name) (reg.(regval_of) v) (Done tt). diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 17a5ba709..8d91f9561 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -137,7 +137,7 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = parens (string "BitVec " ^^ doc_nexp ctxt m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) - | Typ_app (Id_aux (Id "register", _), t_app) -> string "Register " ^^ separate_map comma (doc_typ_app ctxt) t_app + | Typ_app (Id_aux (Id "register", _), t_app) -> string "register_ref Unit Unit " (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts) From 1222d4118a6fecdca19a6a63afb1668e5e8e380c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 9 Dec 2024 15:50:22 +0000 Subject: [PATCH 06/54] updated test --- test/lean/bitfield.lean.expected | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/test/lean/bitfield.lean.expected b/test/lean/bitfield.lean.expected index a92fe23f3..4a27a3c18 100644 --- a/test/lean/bitfield.lean.expected +++ b/test/lean/bitfield.lean.expected @@ -5,7 +5,7 @@ structure cr_type where def undefined_cr_type (lit : Unit) : cr_type := - sorry + sorry /- internal_plet -/ def Mk_cr_type (v : BitVec 8) : cr_type := {bits := v} @@ -16,8 +16,8 @@ def _get_cr_type_bits (v : cr_type) : BitVec 8 := def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)} -def _set_cr_type_bits (r_ref : Register cr_type) (v : BitVec 8) : Unit := - sorry +def _set_cr_type_bits (r_ref : register_ref Unit Unit cr_type) (v : BitVec 8) : Unit := + sorry /- internal_plet -/ def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := (Sail.BitVec.extractLsb v.bits 7 4) @@ -25,8 +25,8 @@ def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)} -def _set_cr_type_CR0 (r_ref : Register cr_type) (v : BitVec 4) : Unit := - sorry +def _set_cr_type_CR0 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 4) : Unit := + sorry /- internal_plet -/ def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 3 2) @@ -34,8 +34,8 @@ def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)} -def _set_cr_type_CR1 (r_ref : Register cr_type) (v : BitVec 2) : Unit := - sorry +def _set_cr_type_CR1 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := + sorry /- internal_plet -/ def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 1 0) @@ -43,8 +43,8 @@ def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)} -def _set_cr_type_CR3 (r_ref : Register cr_type) (v : BitVec 2) : Unit := - sorry +def _set_cr_type_CR3 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := + sorry /- internal_plet -/ def _get_cr_type_GT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 6 6) @@ -52,8 +52,8 @@ def _get_cr_type_GT (v : cr_type) : BitVec 1 := def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)} -def _set_cr_type_GT (r_ref : Register cr_type) (v : BitVec 1) : Unit := - sorry +def _set_cr_type_GT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := + sorry /- internal_plet -/ def _get_cr_type_LT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 7 7) @@ -61,8 +61,8 @@ def _get_cr_type_LT (v : cr_type) : BitVec 1 := def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)} -def _set_cr_type_LT (r_ref : Register cr_type) (v : BitVec 1) : Unit := - sorry +def _set_cr_type_LT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := + sorry /- internal_plet -/ def initialize_registers : Unit := () From 41f93f2aeb4ef7510f97155ea0eff2fbfcb256d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 10 Dec 2024 11:48:23 +0000 Subject: [PATCH 07/54] formatting --- src/sail_lean_backend/pretty_print_lean.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 8d91f9561..e21106a68 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -137,7 +137,9 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = parens (string "BitVec " ^^ doc_nexp ctxt m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) - | Typ_app (Id_aux (Id "register", _), t_app) -> string "register_ref Unit Unit " (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app + | Typ_app (Id_aux (Id "register", _), t_app) -> + string "register_ref Unit Unit " (* TODO: Replace units with real types. *) + ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts) @@ -261,8 +263,8 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *) | E_lit l -> doc_lit l | E_app (Id_aux (Id "internal_pick", _), _) -> - string "sorry /- internal_pick -/" (* TODO replace by actual implementation of internal_pick *) - | E_internal_plet _ -> string "sorry /- internal_plet -/" (* TODO replace by actual implementation of internal_plet *) + string "sorry" (* TODO replace by actual implementation of internal_pick *) + | E_internal_plet _ -> string "sorry" (* TODO replace by actual implementation of internal_plet *) | E_app (f, args) -> let d_id = if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") From d3d373f774c69663a70d12e7d89a6d85135de2e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 10 Dec 2024 12:38:32 +0000 Subject: [PATCH 08/54] fix test name --- test/lean/{bitfield.lean.expected => bitfield.expected.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename test/lean/{bitfield.lean.expected => bitfield.expected.lean} (100%) diff --git a/test/lean/bitfield.lean.expected b/test/lean/bitfield.expected.lean similarity index 100% rename from test/lean/bitfield.lean.expected rename to test/lean/bitfield.expected.lean From 07efed61306c52b09b4b2253aa2fe64dfe8d7d73 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 10 Dec 2024 12:43:44 +0000 Subject: [PATCH 09/54] fix expected output --- test/lean/bitfield.expected.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 4a27a3c18..6681fb9ac 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -5,7 +5,7 @@ structure cr_type where def undefined_cr_type (lit : Unit) : cr_type := - sorry /- internal_plet -/ + sorry def Mk_cr_type (v : BitVec 8) : cr_type := {bits := v} @@ -17,7 +17,7 @@ def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)} def _set_cr_type_bits (r_ref : register_ref Unit Unit cr_type) (v : BitVec 8) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := (Sail.BitVec.extractLsb v.bits 7 4) @@ -26,7 +26,7 @@ def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)} def _set_cr_type_CR0 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 4) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 3 2) @@ -35,7 +35,7 @@ def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)} def _set_cr_type_CR1 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 1 0) @@ -44,7 +44,7 @@ def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)} def _set_cr_type_CR3 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_GT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 6 6) @@ -53,7 +53,7 @@ def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)} def _set_cr_type_GT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_LT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 7 7) @@ -62,7 +62,7 @@ def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)} def _set_cr_type_LT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := - sorry /- internal_plet -/ + sorry def initialize_registers : Unit := () From ebc978a364a66fc4010847e861a7a027497ea552 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 17 Dec 2024 13:18:03 +0000 Subject: [PATCH 10/54] Capitalizing the Lean files --- src/bin/dune | 8 ++++---- src/sail_lean_backend/Sail/{bitvec.lean => Bitvec.lean} | 0 .../Sail/{registers.lean => Registers.lean} | 0 test/lean/bitfield.expected.lean | 2 +- test/lean/struct.lean.expected | 3 --- 5 files changed, 5 insertions(+), 8 deletions(-) rename src/sail_lean_backend/Sail/{bitvec.lean => Bitvec.lean} (100%) rename src/sail_lean_backend/Sail/{registers.lean => Registers.lean} (100%) delete mode 100644 test/lean/struct.lean.expected diff --git a/src/bin/dune b/src/bin/dune index a973f17a7..cade84321 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -249,9 +249,9 @@ (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as src/sail_lean_backend/Sail/Sail.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean + (%{workspace_root}/src/sail_lean_backend/Sail/Bitvec.lean as - src/sail_lean_backend/Sail/bitvec.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean + src/sail_lean_backend/Sail/Bitvec.lean) + (%{workspace_root}/src/sail_lean_backend/Sail/Registers.lean as - src/sail_lean_backend/Sail/registers.lean))) + src/sail_lean_backend/Sail/Registers.lean))) diff --git a/src/sail_lean_backend/Sail/bitvec.lean b/src/sail_lean_backend/Sail/Bitvec.lean similarity index 100% rename from src/sail_lean_backend/Sail/bitvec.lean rename to src/sail_lean_backend/Sail/Bitvec.lean diff --git a/src/sail_lean_backend/Sail/registers.lean b/src/sail_lean_backend/Sail/Registers.lean similarity index 100% rename from src/sail_lean_backend/Sail/registers.lean rename to src/sail_lean_backend/Sail/Registers.lean diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 6681fb9ac..f4cdc676c 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Sail.Sail structure cr_type where bits : BitVec 8 diff --git a/test/lean/struct.lean.expected b/test/lean/struct.lean.expected deleted file mode 100644 index eb29e9f6c..000000000 --- a/test/lean/struct.lean.expected +++ /dev/null @@ -1,3 +0,0 @@ -structure My_struct where - field1 : Int - field2 : Int From 7342888e8ce93b27973c2efe66e54f0f8c4de29b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 17 Dec 2024 13:24:33 +0000 Subject: [PATCH 11/54] Larger struct test file --- src/sail_lean_backend/Sail/Registers.lean | 1 - test/lean/struct.expected.lean | 8 +++++++- test/lean/struct.sail | 11 ++++++++++- 3 files changed, 17 insertions(+), 3 deletions(-) diff --git a/src/sail_lean_backend/Sail/Registers.lean b/src/sail_lean_backend/Sail/Registers.lean index 92552ca58..8b968fe69 100644 --- a/src/sail_lean_backend/Sail/Registers.lean +++ b/src/sail_lean_backend/Sail/Registers.lean @@ -1,4 +1,3 @@ - inductive register where | Register : String → /- name -/ Nat → /- length -/ diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index e3ba05431..c2a979dfd 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -4,11 +4,17 @@ open Sail structure My_struct where field1 : Int - field2 : Int + field2 : (BitVec 1) def undefined_My_struct (lit : Unit) : SailM My_struct := return sorry +def struct_field2 (s : My_struct) : (BitVec 1) := + s.field2 + +def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct := + {s with field2 := b} + def initialize_registers : Unit := () diff --git a/test/lean/struct.sail b/test/lean/struct.sail index a4470e820..5a3fc670e 100644 --- a/test/lean/struct.sail +++ b/test/lean/struct.sail @@ -4,6 +4,15 @@ $include struct My_struct = { field1 : int, - field2 : int, + field2 : bit, } +val struct_field2 : My_struct -> bit +function struct_field2(s) = { + s.field2 +} + +val struct_update_field2 : (My_struct, bit) -> My_struct +function struct_update_field2(s, b) = { + { s with field2 = b } +} \ No newline at end of file From 4a28244fe35d2b88ecc2f01f2cf9579deb376443 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 17 Dec 2024 14:31:00 +0000 Subject: [PATCH 12/54] Typo fixes --- test/lean/bitfield.expected.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index f4cdc676c..28df930d8 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -1,6 +1,6 @@ import Sail.Sail -structure cr_type where +structure cr_type where bits : BitVec 8 From ade2336d46da2aeb1b41cae06892a59fe0351efc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 17 Dec 2024 16:14:19 +0000 Subject: [PATCH 13/54] missing edit for the rebase --- test/lean/bitfield.expected.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 28df930d8..11e6c0687 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -1,4 +1,4 @@ -import Sail.Sail +import Out.Sail.Sail structure cr_type where bits : BitVec 8 From c4f05a23fc2e6069fcfe4dd18154622d904bce19 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 20 Dec 2024 14:31:31 +0100 Subject: [PATCH 14/54] Removing useless changes --- lib/arith.sail | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/arith.sail b/lib/arith.sail index 3bb48e3b2..974b2c8c3 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -54,7 +54,7 @@ $include val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", lean: "HAdd.hAdd", _: "add_int"} : forall 'n 'm. (int('n), int('m)) -> int('n + 'm) -val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add", lean: "HAdd.hAdd", _: "add_int"} : (int, int) -> int +val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", lean: "Int.add", _: "add_int"} : (int, int) -> int overload operator + = {add_atom, add_int} @@ -63,7 +63,7 @@ overload operator + = {add_atom, add_int} val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "HSub.hSub", _: "sub_int"} : forall 'n 'm. (int('n), int('m)) -> int('n - 'm) -val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", lean: "HSub.hSub", _: "sub_int"} : (int, int) -> int +val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", _: "sub_int"} : (int, int) -> int overload operator - = {sub_atom, sub_int} From 08a2c791ed31feb79f9fb4c285ab06a5b9804840 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 10 Jan 2025 13:04:34 +0000 Subject: [PATCH 15/54] Removing the addition import files because the imports in Sail.lean needed the output folder's name to work properly --- src/bin/dune | 8 +----- src/sail_lean_backend/Sail/Bitvec.lean | 30 ----------------------- src/sail_lean_backend/Sail/Registers.lean | 16 ------------ src/sail_lean_backend/Sail/Sail.lean | 7 +++++- 4 files changed, 7 insertions(+), 54 deletions(-) delete mode 100644 src/sail_lean_backend/Sail/Bitvec.lean delete mode 100644 src/sail_lean_backend/Sail/Registers.lean diff --git a/src/bin/dune b/src/bin/dune index cade84321..9a00105c0 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -248,10 +248,4 @@ src/gen_lib/sail2_values.lem) (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as - src/sail_lean_backend/Sail/Sail.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/Bitvec.lean - as - src/sail_lean_backend/Sail/Bitvec.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/Registers.lean - as - src/sail_lean_backend/Sail/Registers.lean))) + src/sail_lean_backend/Sail/Sail.lean))) diff --git a/src/sail_lean_backend/Sail/Bitvec.lean b/src/sail_lean_backend/Sail/Bitvec.lean deleted file mode 100644 index ae1c156ae..000000000 --- a/src/sail_lean_backend/Sail/Bitvec.lean +++ /dev/null @@ -1,30 +0,0 @@ -namespace Sail -namespace BitVec - -def length {w: Nat} (_: BitVec w): Nat := w - -def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := - x.signExtend w' - -def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := - x.zeroExtend w' - -def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := - x.truncate w' - -def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := - x.extractLsb' 0 w' - -def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := - x.extractLsb hi lo - -def update_subrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w := - let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start) - let y' := mask ||| ((y.zeroExtend w) <<< start) - x &&& y' - -def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := - update_subrange' x lo _ y - -end BitVec -end Sail diff --git a/src/sail_lean_backend/Sail/Registers.lean b/src/sail_lean_backend/Sail/Registers.lean deleted file mode 100644 index 8b968fe69..000000000 --- a/src/sail_lean_backend/Sail/Registers.lean +++ /dev/null @@ -1,16 +0,0 @@ -inductive register where - | Register : String → /- name -/ - Nat → /- length -/ - Nat → /- start index -/ - Bool → /- is increasing -/ - List register_field_index - → register - | UndefinedRegister : Nat → register /- length -/ - | RegisterPair : register → register → register - -structure register_ref (regstate regval a: Type) where - name: String - read_from: regstate -> a - write_to: a -> regstate -> regstate - of_regval: regval -> Option a - regval_of: a -> regval diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index b7af3a9dc..c51853073 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -22,8 +22,13 @@ def truncateLsb {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' := def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := x.extractLsb hi lo +def update_subrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w := + let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start) + let y' := mask ||| ((y.zeroExtend w) <<< start) + x &&& y' + def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := - sorry + update_subrange' x lo _ y end BitVec end Sail From e03b2a177487ee82d7a04a104e3a50e1a1985952 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 15 Jan 2025 16:23:14 +0000 Subject: [PATCH 16/54] Adding back registerRef --- src/sail_lean_backend/Sail/Sail.lean | 7 +++++++ src/sail_lean_backend/pretty_print_lean.ml | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index c51853073..1669aae3d 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -32,3 +32,10 @@ def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1) end BitVec end Sail + +structure registerRef (regstate regval a: Type) where + name: String + read_from: regstate -> a + write_to: a -> regstate -> regstate + of_regval: regval -> Option a + regval_of: a -> regval diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index e21106a68..345d03fda 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -138,7 +138,7 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) | Typ_app (Id_aux (Id "register", _), t_app) -> - string "register_ref Unit Unit " (* TODO: Replace units with real types. *) + string "registerRef Unit Unit " (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) From 8c18e46b8de33642298ddea44d05bd6a8e5c5389 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 15 Jan 2025 16:25:33 +0000 Subject: [PATCH 17/54] Formatting --- src/sail_lean_backend/pretty_print_lean.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 345d03fda..38fabe1ca 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -138,8 +138,7 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) | Typ_app (Id_aux (Id "register", _), t_app) -> - string "registerRef Unit Unit " (* TODO: Replace units with real types. *) - ^^ separate_map comma (doc_typ_app ctxt) t_app + string "registerRef Unit Unit " (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts) From a1e5fc59c7f88cf77ad3a4b688cd0d8735eb796a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 15 Jan 2025 16:43:07 +0000 Subject: [PATCH 18/54] Fixing Lean style in Sail.lean --- lib/vector.sail | 2 +- src/sail_lean_backend/Sail/Sail.lean | 20 ++++++++++---------- test/lean/bitfield.expected.lean | 24 ++++++++++++------------ 3 files changed, 23 insertions(+), 23 deletions(-) diff --git a/lib/vector.sail b/lib/vector.sail index ef14f7fa2..87b911b46 100644 --- a/lib/vector.sail +++ b/lib/vector.sail @@ -322,7 +322,7 @@ val update_subrange_bits = pure { interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec", - lean: "Sail.BitVec.update_subrange", + lean: "Sail.BitVec.updateSubrange", _: "vector_update_subrange" } : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o), bits('m - ('o - 1))) -> bits('n) $else diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 1669aae3d..85040954a 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -19,23 +19,23 @@ def truncate {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' := def truncateLsb {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' := x.extractLsb' (w - w') w' -def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := +def extractLsb {w : Nat} (x : BitVec w) (hi lo : Nat) : BitVec (hi - lo + 1) := x.extractLsb hi lo -def update_subrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w := +def updateSubrange' {w : Nat} (x : BitVec w) (start len : Nat) (y : BitVec len) : BitVec w := let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start) let y' := mask ||| ((y.zeroExtend w) <<< start) x &&& y' -def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := - update_subrange' x lo _ y +def updateSubrange {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo + 1)) : BitVec w := + updateSubrange' x lo _ y end BitVec end Sail -structure registerRef (regstate regval a: Type) where - name: String - read_from: regstate -> a - write_to: a -> regstate -> regstate - of_regval: regval -> Option a - regval_of: a -> regval +structure registerRef (regstate regval a : Type) where + name : String + read_from : regstate -> a + write_to : a -> regstate -> regstate + of_regval : regval -> Option a + regval_of : a -> regval diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 11e6c0687..0c0a6ed77 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -14,54 +14,54 @@ def _get_cr_type_bits (v : cr_type) : BitVec 8 := (Sail.BitVec.extractLsb v.bits (HSub.hSub 8 1) 0) def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := - {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)} + {v with bits := (Sail.BitVec.updateSubrange v.bits (HSub.hSub 8 1) 0 x)} -def _set_cr_type_bits (r_ref : register_ref Unit Unit cr_type) (v : BitVec 8) : Unit := +def _set_cr_type_bits (r_ref : registerRef Unit Unit cr_type) (v : BitVec 8) : Unit := sorry def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := (Sail.BitVec.extractLsb v.bits 7 4) def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := - {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)} + {v with bits := (Sail.BitVec.updateSubrange v.bits 7 4 x)} -def _set_cr_type_CR0 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 4) : Unit := +def _set_cr_type_CR0 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 4) : Unit := sorry def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 3 2) def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := - {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)} + {v with bits := (Sail.BitVec.updateSubrange v.bits 3 2 x)} -def _set_cr_type_CR1 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := +def _set_cr_type_CR1 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 2) : Unit := sorry def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 1 0) def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := - {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)} + {v with bits := (Sail.BitVec.updateSubrange v.bits 1 0 x)} -def _set_cr_type_CR3 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := +def _set_cr_type_CR3 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 2) : Unit := sorry def _get_cr_type_GT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 6 6) def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := - {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)} + {v with bits := (Sail.BitVec.updateSubrange v.bits 6 6 x)} -def _set_cr_type_GT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := +def _set_cr_type_GT (r_ref : registerRef Unit Unit cr_type) (v : BitVec 1) : Unit := sorry def _get_cr_type_LT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 7 7) def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := - {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)} + {v with bits := (Sail.BitVec.updateSubrange v.bits 7 7 x)} -def _set_cr_type_LT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := +def _set_cr_type_LT (r_ref : registerRef Unit Unit cr_type) (v : BitVec 1) : Unit := sorry def initialize_registers : Unit := From ff25fd03bd10677c23419a021593af67e930a141 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 16 Jan 2025 10:48:48 +0000 Subject: [PATCH 19/54] changing registerRef to UpperCamelCase --- src/sail_lean_backend/Sail/Sail.lean | 2 +- src/sail_lean_backend/pretty_print_lean.ml | 3 ++- test/lean/bitfield.expected.lean | 12 ++++++------ 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 85040954a..594a37610 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -33,7 +33,7 @@ def updateSubrange {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo + end BitVec end Sail -structure registerRef (regstate regval a : Type) where +structure RegisterRef (regstate regval a : Type) where name : String read_from : regstate -> a write_to : a -> regstate -> regstate diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 38fabe1ca..858ee5333 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -138,7 +138,8 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) | Typ_app (Id_aux (Id "register", _), t_app) -> - string "registerRef Unit Unit " (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app + string "RegisterRef Unit Unit " + (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 0c0a6ed77..94f3ae6c2 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -16,7 +16,7 @@ def _get_cr_type_bits (v : cr_type) : BitVec 8 := def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := {v with bits := (Sail.BitVec.updateSubrange v.bits (HSub.hSub 8 1) 0 x)} -def _set_cr_type_bits (r_ref : registerRef Unit Unit cr_type) (v : BitVec 8) : Unit := +def _set_cr_type_bits (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 8) : Unit := sorry def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := @@ -25,7 +25,7 @@ def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := {v with bits := (Sail.BitVec.updateSubrange v.bits 7 4 x)} -def _set_cr_type_CR0 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 4) : Unit := +def _set_cr_type_CR0 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 4) : Unit := sorry def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := @@ -34,7 +34,7 @@ def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.updateSubrange v.bits 3 2 x)} -def _set_cr_type_CR1 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 2) : Unit := +def _set_cr_type_CR1 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 2) : Unit := sorry def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := @@ -43,7 +43,7 @@ def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.updateSubrange v.bits 1 0 x)} -def _set_cr_type_CR3 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 2) : Unit := +def _set_cr_type_CR3 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 2) : Unit := sorry def _get_cr_type_GT (v : cr_type) : BitVec 1 := @@ -52,7 +52,7 @@ def _get_cr_type_GT (v : cr_type) : BitVec 1 := def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.updateSubrange v.bits 6 6 x)} -def _set_cr_type_GT (r_ref : registerRef Unit Unit cr_type) (v : BitVec 1) : Unit := +def _set_cr_type_GT (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 1) : Unit := sorry def _get_cr_type_LT (v : cr_type) : BitVec 1 := @@ -61,7 +61,7 @@ def _get_cr_type_LT (v : cr_type) : BitVec 1 := def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.updateSubrange v.bits 7 7 x)} -def _set_cr_type_LT (r_ref : registerRef Unit Unit cr_type) (v : BitVec 1) : Unit := +def _set_cr_type_LT (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 1) : Unit := sorry def initialize_registers : Unit := From 86f5ae80f9175450f676af652a2b30e5cd13a920 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 16 Jan 2025 12:09:54 +0000 Subject: [PATCH 20/54] Fixing after rebase --- src/sail_lean_backend/Sail/Sail.lean | 3 ++ test/lean/bitfield.expected.lean | 72 ++++++++++++++-------------- 2 files changed, 38 insertions(+), 37 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 594a37610..dc3dc9f92 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -39,3 +39,6 @@ structure RegisterRef (regstate regval a : Type) where write_to : a -> regstate -> regstate of_regval : regval -> Option a regval_of : a -> regval + +def undefined_bitvector (w : Nat) : BitVec w := + 0 diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 94f3ae6c2..a3252db13 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -1,67 +1,65 @@ import Out.Sail.Sail -structure cr_type where - bits : BitVec 8 +def cr_type := (BitVec 8) +def undefined_cr_type (lit : Unit) : (BitVec 8) := + ((undefined_bitvector 8) : (BitVec 8)) -def undefined_cr_type (lit : Unit) : cr_type := - sorry - -def Mk_cr_type (v : BitVec 8) : cr_type := - {bits := v} +def Mk_cr_type (v : (BitVec 8)) : (BitVec 8) := + v -def _get_cr_type_bits (v : cr_type) : BitVec 8 := - (Sail.BitVec.extractLsb v.bits (HSub.hSub 8 1) 0) +def _get_cr_type_bits (v : (BitVec 8)) : (BitVec 8) := + (Sail.BitVec.extractLsb v (HSub.hSub 8 1) 0) -def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := - {v with bits := (Sail.BitVec.updateSubrange v.bits (HSub.hSub 8 1) 0 x)} +def _update_cr_type_bits (v : (BitVec 8)) (x : (BitVec 8)) : (BitVec 8) := + (Sail.BitVec.updateSubrange v (HSub.hSub 8 1) 0 x) -def _set_cr_type_bits (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 8) : Unit := +def _set_cr_type_bits (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 8)) : Unit := sorry -def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := - (Sail.BitVec.extractLsb v.bits 7 4) +def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := + (Sail.BitVec.extractLsb v 7 4) -def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := - {v with bits := (Sail.BitVec.updateSubrange v.bits 7 4 x)} +def _update_cr_type_CR0 (v : (BitVec 8)) (x : (BitVec 4)) : (BitVec 8) := + (Sail.BitVec.updateSubrange v 7 4 x) -def _set_cr_type_CR0 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 4) : Unit := +def _set_cr_type_CR0 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 4)) : Unit := sorry -def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := - (Sail.BitVec.extractLsb v.bits 3 2) +def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := + (Sail.BitVec.extractLsb v 3 2) -def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := - {v with bits := (Sail.BitVec.updateSubrange v.bits 3 2 x)} +def _update_cr_type_CR1 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) := + (Sail.BitVec.updateSubrange v 3 2 x) -def _set_cr_type_CR1 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 2) : Unit := +def _set_cr_type_CR1 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : Unit := sorry -def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := - (Sail.BitVec.extractLsb v.bits 1 0) +def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := + (Sail.BitVec.extractLsb v 1 0) -def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := - {v with bits := (Sail.BitVec.updateSubrange v.bits 1 0 x)} +def _update_cr_type_CR3 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) := + (Sail.BitVec.updateSubrange v 1 0 x) -def _set_cr_type_CR3 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 2) : Unit := +def _set_cr_type_CR3 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : Unit := sorry -def _get_cr_type_GT (v : cr_type) : BitVec 1 := - (Sail.BitVec.extractLsb v.bits 6 6) +def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := + (Sail.BitVec.extractLsb v 6 6) -def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := - {v with bits := (Sail.BitVec.updateSubrange v.bits 6 6 x)} +def _update_cr_type_GT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) := + (Sail.BitVec.updateSubrange v 6 6 x) -def _set_cr_type_GT (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 1) : Unit := +def _set_cr_type_GT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : Unit := sorry -def _get_cr_type_LT (v : cr_type) : BitVec 1 := - (Sail.BitVec.extractLsb v.bits 7 7) +def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := + (Sail.BitVec.extractLsb v 7 7) -def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := - {v with bits := (Sail.BitVec.updateSubrange v.bits 7 7 x)} +def _update_cr_type_LT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) := + (Sail.BitVec.updateSubrange v 7 7 x) -def _set_cr_type_LT (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 1) : Unit := +def _set_cr_type_LT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : Unit := sorry def initialize_registers : Unit := From 8c6815ab5eaa0419732c9de08aed00cb88061aed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 16 Jan 2025 12:26:32 +0000 Subject: [PATCH 21/54] Adding a mk_struct test --- src/sail_lean_backend/pretty_print_lean.ml | 2 +- test/lean/struct.expected.lean | 4 ++++ test/lean/struct.sail | 8 ++++++++ 3 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 858ee5333..d3c449b58 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -285,7 +285,7 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e | E_struct fexps -> let args = List.map (doc_fexp ctxt) fexps in - braces (separate comma args) + braces (separate (comma ^^ space) args) | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index c2a979dfd..7b1cc29e5 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -15,6 +15,10 @@ def struct_field2 (s : My_struct) : (BitVec 1) := def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct := {s with field2 := b} +/-- Type quantifiers: i : Int -/ +def mk_struct (i : Int) (b : (BitVec 1)) : My_struct := + {field1 := i, field2 := b} + def initialize_registers : Unit := () diff --git a/test/lean/struct.sail b/test/lean/struct.sail index 5a3fc670e..4d249a4ee 100644 --- a/test/lean/struct.sail +++ b/test/lean/struct.sail @@ -15,4 +15,12 @@ function struct_field2(s) = { val struct_update_field2 : (My_struct, bit) -> My_struct function struct_update_field2(s, b) = { { s with field2 = b } +} + +val mk_struct : (int, bit) -> My_struct +function mk_struct(i, b) = { + struct { + field1 = i, + field2 = b + } } \ No newline at end of file From b34591d4d1cc952129ee7a4ed063ec93e09b585e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 16 Jan 2025 14:24:48 +0000 Subject: [PATCH 22/54] updated test output for rebase --- test/lean/bitfield.expected.lean | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index a3252db13..b100161a8 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -1,9 +1,11 @@ import Out.Sail.Sail +open Sail + def cr_type := (BitVec 8) -def undefined_cr_type (lit : Unit) : (BitVec 8) := - ((undefined_bitvector 8) : (BitVec 8)) +def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := + return ((undefined_bitvector 8) : (BitVec 8)) def Mk_cr_type (v : (BitVec 8)) : (BitVec 8) := v @@ -14,8 +16,8 @@ def _get_cr_type_bits (v : (BitVec 8)) : (BitVec 8) := def _update_cr_type_bits (v : (BitVec 8)) (x : (BitVec 8)) : (BitVec 8) := (Sail.BitVec.updateSubrange v (HSub.hSub 8 1) 0 x) -def _set_cr_type_bits (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 8)) : Unit := - sorry +def _set_cr_type_bits (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 8)) : SailM Unit := + return sorry def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := (Sail.BitVec.extractLsb v 7 4) @@ -23,8 +25,8 @@ def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := def _update_cr_type_CR0 (v : (BitVec 8)) (x : (BitVec 4)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 7 4 x) -def _set_cr_type_CR0 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 4)) : Unit := - sorry +def _set_cr_type_CR0 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 4)) : SailM Unit := + return sorry def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := (Sail.BitVec.extractLsb v 3 2) @@ -32,8 +34,8 @@ def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := def _update_cr_type_CR1 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 3 2 x) -def _set_cr_type_CR1 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : Unit := - sorry +def _set_cr_type_CR1 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit := + return sorry def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := (Sail.BitVec.extractLsb v 1 0) @@ -41,8 +43,8 @@ def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := def _update_cr_type_CR3 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 1 0 x) -def _set_cr_type_CR3 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : Unit := - sorry +def _set_cr_type_CR3 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit := + return sorry def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := (Sail.BitVec.extractLsb v 6 6) @@ -50,8 +52,8 @@ def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := def _update_cr_type_GT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 6 6 x) -def _set_cr_type_GT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : Unit := - sorry +def _set_cr_type_GT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit := + return sorry def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := (Sail.BitVec.extractLsb v 7 7) @@ -59,8 +61,8 @@ def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := def _update_cr_type_LT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 7 7 x) -def _set_cr_type_LT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : Unit := - sorry +def _set_cr_type_LT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit := + return sorry def initialize_registers : Unit := () From 8242d703389ce298f46d59a01c47febad8185795 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 16 Jan 2025 15:35:00 +0000 Subject: [PATCH 23/54] Lean style update --- src/sail_lean_backend/pretty_print_lean.ml | 4 ++-- test/lean/struct.expected.lean | 9 +++++++-- test/lean/struct.sail | 5 +++++ 3 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index d3c449b58..624ba7fab 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -285,11 +285,11 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e | E_struct fexps -> let args = List.map (doc_fexp ctxt) fexps in - braces (separate (comma ^^ space) args) + braces (space ^^ nest 2 (separate hardline args) ^^ space) | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in - braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args) + braces (space ^^ doc_exp ctxt exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index 7b1cc29e5..60424c7cc 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -13,11 +13,16 @@ def struct_field2 (s : My_struct) : (BitVec 1) := s.field2 def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct := - {s with field2 := b} + { s with field2 := b } + +/-- Type quantifiers: i : Int -/ +def struct_update_both_fields (s : My_struct) (i : Int) (b : (BitVec 1)) : My_struct := + { s with field1 := i, field2 := b } /-- Type quantifiers: i : Int -/ def mk_struct (i : Int) (b : (BitVec 1)) : My_struct := - {field1 := i, field2 := b} + { field1 := i + field2 := b } def initialize_registers : Unit := () diff --git a/test/lean/struct.sail b/test/lean/struct.sail index 4d249a4ee..9853b7d11 100644 --- a/test/lean/struct.sail +++ b/test/lean/struct.sail @@ -17,6 +17,11 @@ function struct_update_field2(s, b) = { { s with field2 = b } } +val struct_update_both_fields : (My_struct, int, bit) -> My_struct +function struct_update_both_fields(s, i, b) = { + { s with field1 = i, field2 = b } +} + val mk_struct : (int, bit) -> My_struct function mk_struct(i, b) = { struct { From 6efe914b9331952bfcd9490786d59f950400a7eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 6 Dec 2024 14:37:12 +0000 Subject: [PATCH 24/54] First batch of features --- lib/vector.sail | 2 + src/sail_lean_backend/Sail/Sail.lean | 6 ++ src/sail_lean_backend/pretty_print_lean.ml | 18 +++++- test/lean/bitfield.lean.expected | 69 ++++++++++++++++++++++ test/lean/bitfield.sail | 11 ++++ 5 files changed, 104 insertions(+), 2 deletions(-) create mode 100644 test/lean/bitfield.lean.expected create mode 100644 test/lean/bitfield.sail diff --git a/lib/vector.sail b/lib/vector.sail index 59c29d43d..ef14f7fa2 100644 --- a/lib/vector.sail +++ b/lib/vector.sail @@ -299,6 +299,7 @@ val subrange_bits = pure { interpreter: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec", + lean: "Sail.BitVec.extractLsb", _: "vector_subrange" } : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o)) -> bits('m - 'o + 1) @@ -321,6 +322,7 @@ val update_subrange_bits = pure { interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec", + lean: "Sail.BitVec.update_subrange", _: "vector_update_subrange" } : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o), bits('m - ('o - 1))) -> bits('n) $else diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 8cf943fdb..b7af3a9dc 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -19,5 +19,11 @@ def truncate {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' := def truncateLsb {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' := x.extractLsb' (w - w') w' +def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := + x.extractLsb hi lo + +def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := + sorry + end BitVec end Sail diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 868714246..eca26f252 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -137,12 +137,19 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = parens (string "BitVec " ^^ doc_nexp ctxt m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) + | Typ_app (Id_aux (Id "register", _), t_app) -> string "Register " ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts) | Typ_id (Id_aux (Id id, _)) -> string id | _ -> failwith ("Type " ^ string_of_typ_con typ ^ " " ^ string_of_typ typ ^ " not translatable yet.") +and doc_typ_app ctxt (A_aux (t, _) as typ) = + match t with + | A_typ t' -> doc_typ ctxt t' + | A_bool nc -> failwith ("Constraint " ^ string_of_n_constraint nc ^ "not translatable yet.") + | A_nexp m -> doc_nexp ctxt m + let rec captured_typ_var ((i, Typ_aux (t, _)) as typ) = match t with | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) @@ -254,8 +261,8 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *) | E_lit l -> doc_lit l | E_app (Id_aux (Id "internal_pick", _), _) -> - string "sorry" (* TODO replace by actual implementation of internal_pick *) - | E_internal_plet _ -> string "sorry" (* TODO replace by actual implementation of internal_plet *) + string "sorry /- internal_pick -/" (* TODO replace by actual implementation of internal_pick *) + | E_internal_plet _ -> string "sorry /- internal_plet -/" (* TODO replace by actual implementation of internal_plet *) | E_app (f, args) -> let d_id = if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") @@ -274,8 +281,15 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | _ -> failwith "Let pattern not translatable yet." in nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e + | E_struct fexps -> let args = List.map (doc_fexp ctxt) fexps in + braces (separate comma args) + | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id + | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in + braces (doc_exp exp ^^ string " with " ^^ separate comma args) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") +and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp + let doc_binder ctxt i t = let paranthesizer = match t with diff --git a/test/lean/bitfield.lean.expected b/test/lean/bitfield.lean.expected new file mode 100644 index 000000000..a92fe23f3 --- /dev/null +++ b/test/lean/bitfield.lean.expected @@ -0,0 +1,69 @@ +import Sail.sail + +structure cr_type where + bits : BitVec 8 + + +def undefined_cr_type (lit : Unit) : cr_type := + sorry + +def Mk_cr_type (v : BitVec 8) : cr_type := + {bits := v} + +def _get_cr_type_bits (v : cr_type) : BitVec 8 := + (Sail.BitVec.extractLsb v.bits (HSub.hSub 8 1) 0) + +def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)} + +def _set_cr_type_bits (r_ref : Register cr_type) (v : BitVec 8) : Unit := + sorry + +def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := + (Sail.BitVec.extractLsb v.bits 7 4) + +def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)} + +def _set_cr_type_CR0 (r_ref : Register cr_type) (v : BitVec 4) : Unit := + sorry + +def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := + (Sail.BitVec.extractLsb v.bits 3 2) + +def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)} + +def _set_cr_type_CR1 (r_ref : Register cr_type) (v : BitVec 2) : Unit := + sorry + +def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := + (Sail.BitVec.extractLsb v.bits 1 0) + +def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)} + +def _set_cr_type_CR3 (r_ref : Register cr_type) (v : BitVec 2) : Unit := + sorry + +def _get_cr_type_GT (v : cr_type) : BitVec 1 := + (Sail.BitVec.extractLsb v.bits 6 6) + +def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)} + +def _set_cr_type_GT (r_ref : Register cr_type) (v : BitVec 1) : Unit := + sorry + +def _get_cr_type_LT (v : cr_type) : BitVec 1 := + (Sail.BitVec.extractLsb v.bits 7 7) + +def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := + {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)} + +def _set_cr_type_LT (r_ref : Register cr_type) (v : BitVec 1) : Unit := + sorry + +def initialize_registers : Unit := + () + diff --git a/test/lean/bitfield.sail b/test/lean/bitfield.sail new file mode 100644 index 000000000..4182b05c8 --- /dev/null +++ b/test/lean/bitfield.sail @@ -0,0 +1,11 @@ +default Order dec + +$include + +bitfield cr_type : bits(8) = { + CR0 : 7 .. 4, + LT : 7, + GT : 6, + CR1 : 3 .. 2, + CR3 : 1 .. 0 +} \ No newline at end of file From c7be434d9b61b9c2609fbf0c2c9e9e0169fd7229 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 6 Dec 2024 16:06:07 +0000 Subject: [PATCH 25/54] Adding features --- lib/arith.sail | 9 +++---- src/bin/dune | 8 ++++++- src/sail_lean_backend/Sail/bitvec.lean | 25 +++++++++++++++++++ src/sail_lean_backend/Sail/registers.lean | 29 +++++++++++++++++++++++ 4 files changed, 66 insertions(+), 5 deletions(-) create mode 100644 src/sail_lean_backend/Sail/bitvec.lean create mode 100644 src/sail_lean_backend/Sail/registers.lean diff --git a/lib/arith.sail b/lib/arith.sail index 202d2ec5a..3bb48e3b2 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -51,19 +51,19 @@ $include // ***** Addition ***** -val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", _: "add_int"} : forall 'n 'm. +val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", lean: "HAdd.hAdd", _: "add_int"} : forall 'n 'm. (int('n), int('m)) -> int('n + 'm) -val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add", _: "add_int"} : (int, int) -> int +val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add", lean: "HAdd.hAdd", _: "add_int"} : (int, int) -> int overload operator + = {add_atom, add_int} // ***** Subtraction ***** -val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", _: "sub_int"} : forall 'n 'm. +val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "HSub.hSub", _: "sub_int"} : forall 'n 'm. (int('n), int('m)) -> int('n - 'm) -val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", _: "sub_int"} : (int, int) -> int +val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", lean: "HSub.hSub", _: "sub_int"} : (int, int) -> int overload operator - = {sub_atom, sub_int} @@ -71,6 +71,7 @@ val sub_nat = pure { ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", lem: "integerMinus", coq: "Z.sub", + lean: "HSub.hSub", _: "sub_nat" } : (nat, nat) -> nat diff --git a/src/bin/dune b/src/bin/dune index 9a00105c0..7f6006737 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -248,4 +248,10 @@ src/gen_lib/sail2_values.lem) (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as - src/sail_lean_backend/Sail/Sail.lean))) + src/sail_lean_backend/Sail/Sail.lean) + (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean + as + src/sail_lean_backend/Sail/bitvec.lean) + (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean + as + src/sail_lean_backend/Sail/registers.lean))) diff --git a/src/sail_lean_backend/Sail/bitvec.lean b/src/sail_lean_backend/Sail/bitvec.lean new file mode 100644 index 000000000..7a0ec1e06 --- /dev/null +++ b/src/sail_lean_backend/Sail/bitvec.lean @@ -0,0 +1,25 @@ +namespace Sail +namespace BitVec + +def length {w: Nat} (_: BitVec w): Nat := w + +def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := + x.signExtend w' + +def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := + x.zeroExtend w' + +def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := + x.truncate w' + +def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := + x.extractLsb' 0 w' + +def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := + x.extractLsb hi lo + +def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := + sorry + +end BitVec +end Sail diff --git a/src/sail_lean_backend/Sail/registers.lean b/src/sail_lean_backend/Sail/registers.lean new file mode 100644 index 000000000..26d122546 --- /dev/null +++ b/src/sail_lean_backend/Sail/registers.lean @@ -0,0 +1,29 @@ + +inductive register where + | Register : String → /- name -/ + Nat → /- length -/ + Nat → /- start index -/ + Bool → /- is increasing -/ + List register_field_index + → register + | UndefinedRegister : Nat → register /- length -/ + | RegisterPair : register → register → register + +structure register_ref (regstate regval a: Type) where + name: String + read_from: regstate -> a + write_to: a -> regstate -> regstate + of_regval: regval -> Option a + regval_of: a -> regval + +def read_reg {s rv a e} (reg : register_ref s rv a) : Monad e := + let k v := + match reg.of_regval v with + | some v => some v + | none => none + Read_reg reg.(name) k. + +def reg_deref {s rv a e} := @read_reg s rv a e. + +def write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv unit e := + Write_reg reg.(name) (reg.(regval_of) v) (Done tt). From 23d99b2d2e71fe94ed35189fc08947ae92fea076 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 6 Dec 2024 16:08:22 +0000 Subject: [PATCH 26/54] formatting --- src/bin/dune | 4 ++-- src/sail_lean_backend/pretty_print_lean.ml | 10 ++++++---- test/lean/bitfield.sail | 2 +- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/bin/dune b/src/bin/dune index 7f6006737..a973f17a7 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -249,9 +249,9 @@ (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as src/sail_lean_backend/Sail/Sail.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean + (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean as src/sail_lean_backend/Sail/bitvec.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean + (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean as src/sail_lean_backend/Sail/registers.lean))) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index eca26f252..6399769e2 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -281,11 +281,13 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | _ -> failwith "Let pattern not translatable yet." in nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e - | E_struct fexps -> let args = List.map (doc_fexp ctxt) fexps in - braces (separate comma args) + | E_struct fexps -> + let args = List.map (doc_fexp ctxt) fexps in + braces (separate comma args) | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id - | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in - braces (doc_exp exp ^^ string " with " ^^ separate comma args) + | E_struct_update (exp, fexps) -> + let args = List.map (doc_fexp ctxt) fexps in + braces (doc_exp exp ^^ string " with " ^^ separate comma args) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp diff --git a/test/lean/bitfield.sail b/test/lean/bitfield.sail index 4182b05c8..2969f5927 100644 --- a/test/lean/bitfield.sail +++ b/test/lean/bitfield.sail @@ -8,4 +8,4 @@ bitfield cr_type : bits(8) = { GT : 6, CR1 : 3 .. 2, CR3 : 1 .. 0 -} \ No newline at end of file +} From 0dddf2971e07222474a3de70285f910d74ab8e5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 9 Dec 2024 15:31:54 +0000 Subject: [PATCH 27/54] update_subrange implementation --- src/sail_lean_backend/Sail/bitvec.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/Sail/bitvec.lean b/src/sail_lean_backend/Sail/bitvec.lean index 7a0ec1e06..ae1c156ae 100644 --- a/src/sail_lean_backend/Sail/bitvec.lean +++ b/src/sail_lean_backend/Sail/bitvec.lean @@ -18,8 +18,13 @@ def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := x.extractLsb hi lo +def update_subrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w := + let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start) + let y' := mask ||| ((y.zeroExtend w) <<< start) + x &&& y' + def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := - sorry + update_subrange' x lo _ y end BitVec end Sail From 9c454ddb64c349472c2855c4c3f6943b1208d429 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 9 Dec 2024 15:45:46 +0000 Subject: [PATCH 28/54] Cleanup registers --- src/sail_lean_backend/Sail/registers.lean | 12 ------------ src/sail_lean_backend/pretty_print_lean.ml | 2 +- 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/src/sail_lean_backend/Sail/registers.lean b/src/sail_lean_backend/Sail/registers.lean index 26d122546..92552ca58 100644 --- a/src/sail_lean_backend/Sail/registers.lean +++ b/src/sail_lean_backend/Sail/registers.lean @@ -15,15 +15,3 @@ structure register_ref (regstate regval a: Type) where write_to: a -> regstate -> regstate of_regval: regval -> Option a regval_of: a -> regval - -def read_reg {s rv a e} (reg : register_ref s rv a) : Monad e := - let k v := - match reg.of_regval v with - | some v => some v - | none => none - Read_reg reg.(name) k. - -def reg_deref {s rv a e} := @read_reg s rv a e. - -def write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv unit e := - Write_reg reg.(name) (reg.(regval_of) v) (Done tt). diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 6399769e2..e36bbe590 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -137,7 +137,7 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = parens (string "BitVec " ^^ doc_nexp ctxt m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) - | Typ_app (Id_aux (Id "register", _), t_app) -> string "Register " ^^ separate_map comma (doc_typ_app ctxt) t_app + | Typ_app (Id_aux (Id "register", _), t_app) -> string "register_ref Unit Unit " (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts) From fdef34a3c66ddfed6ee4903bf1908a77078764f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 9 Dec 2024 15:50:22 +0000 Subject: [PATCH 29/54] updated test --- test/lean/bitfield.lean.expected | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/test/lean/bitfield.lean.expected b/test/lean/bitfield.lean.expected index a92fe23f3..4a27a3c18 100644 --- a/test/lean/bitfield.lean.expected +++ b/test/lean/bitfield.lean.expected @@ -5,7 +5,7 @@ structure cr_type where def undefined_cr_type (lit : Unit) : cr_type := - sorry + sorry /- internal_plet -/ def Mk_cr_type (v : BitVec 8) : cr_type := {bits := v} @@ -16,8 +16,8 @@ def _get_cr_type_bits (v : cr_type) : BitVec 8 := def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)} -def _set_cr_type_bits (r_ref : Register cr_type) (v : BitVec 8) : Unit := - sorry +def _set_cr_type_bits (r_ref : register_ref Unit Unit cr_type) (v : BitVec 8) : Unit := + sorry /- internal_plet -/ def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := (Sail.BitVec.extractLsb v.bits 7 4) @@ -25,8 +25,8 @@ def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)} -def _set_cr_type_CR0 (r_ref : Register cr_type) (v : BitVec 4) : Unit := - sorry +def _set_cr_type_CR0 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 4) : Unit := + sorry /- internal_plet -/ def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 3 2) @@ -34,8 +34,8 @@ def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)} -def _set_cr_type_CR1 (r_ref : Register cr_type) (v : BitVec 2) : Unit := - sorry +def _set_cr_type_CR1 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := + sorry /- internal_plet -/ def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 1 0) @@ -43,8 +43,8 @@ def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)} -def _set_cr_type_CR3 (r_ref : Register cr_type) (v : BitVec 2) : Unit := - sorry +def _set_cr_type_CR3 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := + sorry /- internal_plet -/ def _get_cr_type_GT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 6 6) @@ -52,8 +52,8 @@ def _get_cr_type_GT (v : cr_type) : BitVec 1 := def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)} -def _set_cr_type_GT (r_ref : Register cr_type) (v : BitVec 1) : Unit := - sorry +def _set_cr_type_GT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := + sorry /- internal_plet -/ def _get_cr_type_LT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 7 7) @@ -61,8 +61,8 @@ def _get_cr_type_LT (v : cr_type) : BitVec 1 := def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)} -def _set_cr_type_LT (r_ref : Register cr_type) (v : BitVec 1) : Unit := - sorry +def _set_cr_type_LT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := + sorry /- internal_plet -/ def initialize_registers : Unit := () From 2a2da2d42d8466c11b94a40c3c391087b854d03f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 10 Dec 2024 11:48:23 +0000 Subject: [PATCH 30/54] formatting --- src/sail_lean_backend/pretty_print_lean.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index e36bbe590..3389f1fae 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -137,7 +137,9 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) = parens (string "BitVec " ^^ doc_nexp ctxt m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int" (* TODO This probably has to be generalized *) - | Typ_app (Id_aux (Id "register", _), t_app) -> string "register_ref Unit Unit " (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app + | Typ_app (Id_aux (Id "register", _), t_app) -> + string "register_ref Unit Unit " (* TODO: Replace units with real types. *) + ^^ separate_map comma (doc_typ_app ctxt) t_app | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> underscore (* TODO check if the type of implicit arguments can really be always inferred *) | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts) @@ -261,8 +263,8 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *) | E_lit l -> doc_lit l | E_app (Id_aux (Id "internal_pick", _), _) -> - string "sorry /- internal_pick -/" (* TODO replace by actual implementation of internal_pick *) - | E_internal_plet _ -> string "sorry /- internal_plet -/" (* TODO replace by actual implementation of internal_plet *) + string "sorry" (* TODO replace by actual implementation of internal_pick *) + | E_internal_plet _ -> string "sorry" (* TODO replace by actual implementation of internal_plet *) | E_app (f, args) -> let d_id = if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") From 777ba213fb56e1e24728d28f37203b463f61de87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 10 Dec 2024 12:38:32 +0000 Subject: [PATCH 31/54] fix test name --- test/lean/{bitfield.lean.expected => bitfield.expected.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename test/lean/{bitfield.lean.expected => bitfield.expected.lean} (100%) diff --git a/test/lean/bitfield.lean.expected b/test/lean/bitfield.expected.lean similarity index 100% rename from test/lean/bitfield.lean.expected rename to test/lean/bitfield.expected.lean From 98d5eb37c5e15493d7946ae606ed4a6596ffd631 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 10 Dec 2024 12:43:44 +0000 Subject: [PATCH 32/54] fix expected output --- test/lean/bitfield.expected.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 4a27a3c18..6681fb9ac 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -5,7 +5,7 @@ structure cr_type where def undefined_cr_type (lit : Unit) : cr_type := - sorry /- internal_plet -/ + sorry def Mk_cr_type (v : BitVec 8) : cr_type := {bits := v} @@ -17,7 +17,7 @@ def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)} def _set_cr_type_bits (r_ref : register_ref Unit Unit cr_type) (v : BitVec 8) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_CR0 (v : cr_type) : BitVec 4 := (Sail.BitVec.extractLsb v.bits 7 4) @@ -26,7 +26,7 @@ def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)} def _set_cr_type_CR0 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 4) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_CR1 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 3 2) @@ -35,7 +35,7 @@ def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)} def _set_cr_type_CR1 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_CR3 (v : cr_type) : BitVec 2 := (Sail.BitVec.extractLsb v.bits 1 0) @@ -44,7 +44,7 @@ def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)} def _set_cr_type_CR3 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_GT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 6 6) @@ -53,7 +53,7 @@ def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)} def _set_cr_type_GT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := - sorry /- internal_plet -/ + sorry def _get_cr_type_LT (v : cr_type) : BitVec 1 := (Sail.BitVec.extractLsb v.bits 7 7) @@ -62,7 +62,7 @@ def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type := {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)} def _set_cr_type_LT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit := - sorry /- internal_plet -/ + sorry def initialize_registers : Unit := () From 5208f0842466fb4f9349f67ccb91043448589a71 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 17 Dec 2024 13:18:03 +0000 Subject: [PATCH 33/54] Capitalizing the Lean files --- src/bin/dune | 8 ++++---- src/sail_lean_backend/Sail/{bitvec.lean => Bitvec.lean} | 0 .../Sail/{registers.lean => Registers.lean} | 0 test/lean/bitfield.expected.lean | 2 +- test/lean/struct.lean.expected | 3 --- 5 files changed, 5 insertions(+), 8 deletions(-) rename src/sail_lean_backend/Sail/{bitvec.lean => Bitvec.lean} (100%) rename src/sail_lean_backend/Sail/{registers.lean => Registers.lean} (100%) delete mode 100644 test/lean/struct.lean.expected diff --git a/src/bin/dune b/src/bin/dune index a973f17a7..cade84321 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -249,9 +249,9 @@ (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as src/sail_lean_backend/Sail/Sail.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean + (%{workspace_root}/src/sail_lean_backend/Sail/Bitvec.lean as - src/sail_lean_backend/Sail/bitvec.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean + src/sail_lean_backend/Sail/Bitvec.lean) + (%{workspace_root}/src/sail_lean_backend/Sail/Registers.lean as - src/sail_lean_backend/Sail/registers.lean))) + src/sail_lean_backend/Sail/Registers.lean))) diff --git a/src/sail_lean_backend/Sail/bitvec.lean b/src/sail_lean_backend/Sail/Bitvec.lean similarity index 100% rename from src/sail_lean_backend/Sail/bitvec.lean rename to src/sail_lean_backend/Sail/Bitvec.lean diff --git a/src/sail_lean_backend/Sail/registers.lean b/src/sail_lean_backend/Sail/Registers.lean similarity index 100% rename from src/sail_lean_backend/Sail/registers.lean rename to src/sail_lean_backend/Sail/Registers.lean diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 6681fb9ac..f4cdc676c 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Sail.Sail structure cr_type where bits : BitVec 8 diff --git a/test/lean/struct.lean.expected b/test/lean/struct.lean.expected deleted file mode 100644 index eb29e9f6c..000000000 --- a/test/lean/struct.lean.expected +++ /dev/null @@ -1,3 +0,0 @@ -structure My_struct where - field1 : Int - field2 : Int From 1b0f304d81545101d985384e37393b177662ded8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 17 Dec 2024 13:24:33 +0000 Subject: [PATCH 34/54] Larger struct test file --- src/sail_lean_backend/Sail/Registers.lean | 1 - test/lean/struct.expected.lean | 8 +++++++- test/lean/struct.sail | 11 ++++++++++- 3 files changed, 17 insertions(+), 3 deletions(-) diff --git a/src/sail_lean_backend/Sail/Registers.lean b/src/sail_lean_backend/Sail/Registers.lean index 92552ca58..8b968fe69 100644 --- a/src/sail_lean_backend/Sail/Registers.lean +++ b/src/sail_lean_backend/Sail/Registers.lean @@ -1,4 +1,3 @@ - inductive register where | Register : String → /- name -/ Nat → /- length -/ diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index e3ba05431..c2a979dfd 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -4,11 +4,17 @@ open Sail structure My_struct where field1 : Int - field2 : Int + field2 : (BitVec 1) def undefined_My_struct (lit : Unit) : SailM My_struct := return sorry +def struct_field2 (s : My_struct) : (BitVec 1) := + s.field2 + +def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct := + {s with field2 := b} + def initialize_registers : Unit := () diff --git a/test/lean/struct.sail b/test/lean/struct.sail index a4470e820..5a3fc670e 100644 --- a/test/lean/struct.sail +++ b/test/lean/struct.sail @@ -4,6 +4,15 @@ $include struct My_struct = { field1 : int, - field2 : int, + field2 : bit, } +val struct_field2 : My_struct -> bit +function struct_field2(s) = { + s.field2 +} + +val struct_update_field2 : (My_struct, bit) -> My_struct +function struct_update_field2(s, b) = { + { s with field2 = b } +} \ No newline at end of file From 44409f54b59e3ee5f5b65b468cda1d31437b402b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 17 Dec 2024 14:31:00 +0000 Subject: [PATCH 35/54] Typo fixes --- test/lean/bitfield.expected.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index f4cdc676c..28df930d8 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -1,6 +1,6 @@ import Sail.Sail -structure cr_type where +structure cr_type where bits : BitVec 8 From 32543958aad96fc5cc1fa5ef2b2c52e7412b5933 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 17 Dec 2024 16:14:19 +0000 Subject: [PATCH 36/54] missing edit for the rebase --- test/lean/bitfield.expected.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 28df930d8..11e6c0687 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -1,4 +1,4 @@ -import Sail.Sail +import Out.Sail.Sail structure cr_type where bits : BitVec 8 From 2f44421592baf3d7e5e8083065a904d95b217c3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 20 Dec 2024 14:31:31 +0100 Subject: [PATCH 37/54] Removing useless changes --- lib/arith.sail | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/arith.sail b/lib/arith.sail index 3bb48e3b2..974b2c8c3 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -54,7 +54,7 @@ $include val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", lean: "HAdd.hAdd", _: "add_int"} : forall 'n 'm. (int('n), int('m)) -> int('n + 'm) -val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add", lean: "HAdd.hAdd", _: "add_int"} : (int, int) -> int +val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", lean: "Int.add", _: "add_int"} : (int, int) -> int overload operator + = {add_atom, add_int} @@ -63,7 +63,7 @@ overload operator + = {add_atom, add_int} val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "HSub.hSub", _: "sub_int"} : forall 'n 'm. (int('n), int('m)) -> int('n - 'm) -val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", lean: "HSub.hSub", _: "sub_int"} : (int, int) -> int +val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", _: "sub_int"} : (int, int) -> int overload operator - = {sub_atom, sub_int} From 27b82e7cc74e35079022dd102dfab5cc14d63275 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 10 Jan 2025 13:04:34 +0000 Subject: [PATCH 38/54] Removing the addition import files because the imports in Sail.lean needed the output folder's name to work properly --- src/bin/dune | 8 +----- src/sail_lean_backend/Sail/Bitvec.lean | 30 ----------------------- src/sail_lean_backend/Sail/Registers.lean | 16 ------------ src/sail_lean_backend/Sail/Sail.lean | 7 +++++- 4 files changed, 7 insertions(+), 54 deletions(-) delete mode 100644 src/sail_lean_backend/Sail/Bitvec.lean delete mode 100644 src/sail_lean_backend/Sail/Registers.lean diff --git a/src/bin/dune b/src/bin/dune index cade84321..9a00105c0 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -248,10 +248,4 @@ src/gen_lib/sail2_values.lem) (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as - src/sail_lean_backend/Sail/Sail.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/Bitvec.lean - as - src/sail_lean_backend/Sail/Bitvec.lean) - (%{workspace_root}/src/sail_lean_backend/Sail/Registers.lean - as - src/sail_lean_backend/Sail/Registers.lean))) + src/sail_lean_backend/Sail/Sail.lean))) diff --git a/src/sail_lean_backend/Sail/Bitvec.lean b/src/sail_lean_backend/Sail/Bitvec.lean deleted file mode 100644 index ae1c156ae..000000000 --- a/src/sail_lean_backend/Sail/Bitvec.lean +++ /dev/null @@ -1,30 +0,0 @@ -namespace Sail -namespace BitVec - -def length {w: Nat} (_: BitVec w): Nat := w - -def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := - x.signExtend w' - -def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := - x.zeroExtend w' - -def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := - x.truncate w' - -def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' := - x.extractLsb' 0 w' - -def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := - x.extractLsb hi lo - -def update_subrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w := - let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start) - let y' := mask ||| ((y.zeroExtend w) <<< start) - x &&& y' - -def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := - update_subrange' x lo _ y - -end BitVec -end Sail diff --git a/src/sail_lean_backend/Sail/Registers.lean b/src/sail_lean_backend/Sail/Registers.lean deleted file mode 100644 index 8b968fe69..000000000 --- a/src/sail_lean_backend/Sail/Registers.lean +++ /dev/null @@ -1,16 +0,0 @@ -inductive register where - | Register : String → /- name -/ - Nat → /- length -/ - Nat → /- start index -/ - Bool → /- is increasing -/ - List register_field_index - → register - | UndefinedRegister : Nat → register /- length -/ - | RegisterPair : register → register → register - -structure register_ref (regstate regval a: Type) where - name: String - read_from: regstate -> a - write_to: a -> regstate -> regstate - of_regval: regval -> Option a - regval_of: a -> regval diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index b7af3a9dc..c51853073 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -22,8 +22,13 @@ def truncateLsb {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' := def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) := x.extractLsb hi lo +def update_subrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w := + let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start) + let y' := mask ||| ((y.zeroExtend w) <<< start) + x &&& y' + def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w := - sorry + update_subrange' x lo _ y end BitVec end Sail From bbae47d23c0e9c8d3e9e57f6a20d5731a969bade Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 10 Jan 2025 14:32:06 +0000 Subject: [PATCH 39/54] Missed edit in rebasing --- src/sail_lean_backend/pretty_print_lean.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 3389f1fae..e21106a68 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -289,7 +289,7 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in - braces (doc_exp exp ^^ string " with " ^^ separate comma args) + braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp From 6add1739e3219d32bffada9ea5ee3aa0db783f54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 10 Jan 2025 14:32:49 +0000 Subject: [PATCH 40/54] first adding is_monadic --- src/sail_lean_backend/pretty_print_lean.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index e21106a68..b3d029bb7 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -12,9 +12,14 @@ open Pretty_print_common type context = { kid_id_renames : id option KBindings.t; (* tyvar -> argument renames *) kid_id_renames_rev : kid Bindings.t; (* reverse of kid_id_renames *) + is_monadic : bool; } -let empty_context = { kid_id_renames = KBindings.empty; kid_id_renames_rev = Bindings.empty } +let empty_context = { + kid_id_renames = KBindings.empty; + kid_id_renames_rev = Bindings.empty; + is_monadic = false; + } let add_single_kid_id_rename ctxt id kid = let kir = @@ -26,6 +31,7 @@ let add_single_kid_id_rename ctxt id kid = (* ctxt with *) kid_id_renames = KBindings.add kid (Some id) kir; kid_id_renames_rev = Bindings.add id kid ctxt.kid_id_renames_rev; + is_monadic = ctxt.is_monadic } let implicit_parens x = enclose (string "{") (string "}") x From d8c28689b123064ff13163fb6aee1043b6d3a3f2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 13 Jan 2025 14:12:04 +0000 Subject: [PATCH 41/54] internal_plet --- src/lib/state.ml | 27 +++ src/sail_lean_backend/Sail/Sail.lean | 3 + src/sail_lean_backend/pretty_print_lean.ml | 189 ++++++++++++++++++--- src/sail_lean_backend/sail_plugin_lean.ml | 6 +- 4 files changed, 195 insertions(+), 30 deletions(-) diff --git a/src/lib/state.ml b/src/lib/state.ml index 8ef47a010..d75f1aaa7 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -834,6 +834,33 @@ let register_refs_coq doc_id coq_record_update env registers = in separate hardline [generic_convs; refs; getters_setters] +let register_refs_lean doc_id doc_typ registers = + let generic_convs = separate_map hardline string [""; "variable [MonadReg m] [Monad m]"; ""; "open MonadReg"; ""] in + let register_ref (typ, id, _) = + let idd = doc_id id in + let typp = doc_typ typ in + (* let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in *) + concat + [ + string " set_"; + idd; + colon; + space; + typp; + string " -> m Unit"; + hardline; + string " get_"; + idd; + colon; + space; + string "m ("; + typp; + string ")"; + ] + in + let refs = separate_map hardline register_ref registers in + separate hardline [string "class MonadReg (m : Type -> Type) where"; refs; generic_convs] + let generate_regstate_defs ctx env ast = let defs = ast.defs in let registers = find_registers defs in diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index c51853073..22c3e5292 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -32,3 +32,6 @@ def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1) end BitVec end Sail + +def undefined_bitvector (n: Nat) : BitVec n := + 0#n diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index b3d029bb7..06834c243 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -9,16 +9,23 @@ open Rewriter open PPrint open Pretty_print_common +let prefix_recordtype = true + +type global_context = { effect_info : Effects.side_effect_info } + type context = { + global : global_context; kid_id_renames : id option KBindings.t; (* tyvar -> argument renames *) kid_id_renames_rev : kid Bindings.t; (* reverse of kid_id_renames *) is_monadic : bool; } -let empty_context = { - kid_id_renames = KBindings.empty; - kid_id_renames_rev = Bindings.empty; - is_monadic = false; +let empty_context = + { + global = { effect_info = Effects.empty_side_effect_info }; + kid_id_renames = KBindings.empty; + kid_id_renames_rev = Bindings.empty; + is_monadic = false; } let add_single_kid_id_rename ctxt id kid = @@ -28,17 +35,22 @@ let add_single_kid_id_rename ctxt id kid = | None -> ctxt.kid_id_renames in { - (* ctxt with *) + ctxt with kid_id_renames = KBindings.add kid (Some id) kir; kid_id_renames_rev = Bindings.add id kid ctxt.kid_id_renames_rev; - is_monadic = ctxt.is_monadic } let implicit_parens x = enclose (string "{") (string "}") x - -let doc_id_ctor (Id_aux (i, _)) = +let doc_id_ctor (ctxt : context) (Id_aux (i, _)) = match i with Id i -> string i | Operator x -> string (Util.zencode_string ("op " ^ x)) +let doc_id = doc_id_ctor + +let doc_field_name ctxt typ_id field_id = + if prefix_recordtype && string_of_id typ_id <> "regstate" then + doc_id ctxt typ_id ^^ string "_" ^^ doc_id ctxt field_id + else doc_id ctxt field_id + let doc_kid ctxt (Kid_aux (Var x, _) as ki) = match KBindings.find_opt ki ctxt.kid_id_renames with | Some (Some i) -> string (string_of_id i) @@ -165,7 +177,7 @@ let rec captured_typ_var ((i, Typ_aux (t, _)) as typ) = Some (i, ki) | _ -> None -let doc_typ_id ctxt (typ, fid) = flow (break 1) [doc_id_ctor fid; colon; doc_typ ctxt typ] +let doc_typ_id ctxt (typ, fid) = flow (break 1) [doc_id_ctor ctxt fid; colon; doc_typ ctxt typ] let doc_kind (K_aux (k, _)) = match k with @@ -223,6 +235,103 @@ let doc_lit (L_aux (lit, l)) = | L_string s -> utf8string ("\"" ^ lean_escape_string s ^ "\"") | L_real s -> utf8string s (* TODO test if this is really working *) +let string_of_pat_con (P_aux (p, _)) = + match p with + | P_app _ -> "P_app" + | P_wild -> "P_wild" + | P_lit _ -> "P_lit" + | P_or _ -> "P_or" + | P_not _ -> "P_not" + | P_as _ -> "P_as" + | P_typ _ -> "P_typ" + | P_id _ -> "P_id" + | P_var _ -> "P_var" + | P_vector _ -> "P_vector" + | P_vector_concat _ -> "P_vector_concat" + | P_vector_subrange _ -> "P_vector_subrange" + | P_tuple _ -> "P_tuple" + | P_list _ -> "P_list" + | P_cons _ -> "P_cons" + | P_string_append _ -> "P_string_append" + | P_struct _ -> "P_struct" + +let rec doc_pat ctxt apat_needed (P_aux (p, (l, annot))) = + let env = env_of_annot (l, annot) in + let typ = Env.expand_synonyms env (typ_of_annot (l, annot)) in + match p with + (* Special case translation of the None constructor to remove the unit arg *) + | P_app (id, _) when string_of_id id = "None" -> string "None" + | P_app (id, (_ :: _ as pats)) -> begin + let pats_pp = separate_map comma (doc_pat ctxt true) pats in + let pats_pp = match pats with [_] -> pats_pp | _ -> parens pats_pp in + let ppp = doc_unop (doc_id_ctor ctxt id) pats_pp in + if apat_needed then parens ppp else ppp + end + | P_app (id, []) -> doc_id_ctor ctxt id + | P_lit lit -> doc_lit lit + | P_wild -> underscore + | P_id id -> doc_id ctxt id + | P_var (p, _) -> doc_pat ctxt true p + | P_as (p, id) -> parens (separate space [doc_pat ctxt true p; string "as"; doc_id ctxt id]) + | P_typ (ptyp, p) -> + let doc_p = doc_pat ctxt true p in + doc_p + (* Type annotations aren't allowed everywhere in patterns in Coq *) + (*parens (doc_op colon doc_p (doc_typ typ))*) + | P_vector pats -> + let ppp = brackets (separate_map semi (fun p -> doc_pat ctxt true p) pats) in + if apat_needed then parens ppp else ppp + | P_vector_concat pats -> + raise + (Reporting.err_unreachable l __POS__ + "vector concatenation patterns should have been removed before pretty-printing" + ) + | P_vector_subrange _ -> unreachable l __POS__ "Must have been rewritten before Coq backend" + | P_tuple pats -> ( + match pats with [p] -> doc_pat ctxt apat_needed p | _ -> parens (separate_map comma_sp (doc_pat ctxt false) pats) + ) + | P_list pats -> brackets (separate_map semi (doc_pat ctxt false) pats) + | P_cons (p, p') -> + let ppp = doc_op (string "::") (doc_pat ctxt true p) (doc_pat ctxt true p') in + if apat_needed then parens ppp else ppp + | P_string_append _ -> unreachable l __POS__ "string append pattern found in Coq backend, should have been rewritten" + | P_struct (fpats, _) -> + let type_id = + match typ with + | (Typ_aux (Typ_id tid, _) | Typ_aux (Typ_app (tid, _), _)) when Env.is_record tid env -> tid + | _ -> Reporting.unreachable l __POS__ "P_struct pattern with no record type" + in + string "{|" ^^ space + ^^ separate_map (semi ^^ space) + (fun (field, pat) -> separate space [doc_field_name ctxt type_id field; coloneq; doc_pat ctxt false pat]) + fpats + ^^ space ^^ string "|}" + | P_not _ -> unreachable l __POS__ "Coq backend doesn't support not patterns" + | P_or _ -> unreachable l __POS__ "Coq backend doesn't support or patterns yet" + +let rebind_cast_pattern_vars pat typ exp = + let rec aux pat typ = + match (pat, typ) with + | P_aux (P_typ (target_typ, P_aux (P_id id, (l, ann))), _), source_typ when not (is_enum (env_of exp) id) -> + if Typ.compare target_typ source_typ == 0 then [] + else ( + let l = Parse_ast.Generated l in + let cast_annot = Type_check.replace_typ source_typ ann in + let e_annot = Type_check.mk_tannot (env_of exp) source_typ in + [LB_aux (LB_val (pat, E_aux (E_id id, (l, e_annot))), (l, ann))] + ) + | P_aux (P_tuple pats, _), Typ_aux (Typ_tuple typs, _) -> List.concat (List.map2 aux pats typs) + | _ -> [] + in + let add_lb (E_aux (_, ann) as exp) lb = E_aux (E_let (lb, exp), ann) in + (* Don't introduce new bindings at the top-level, we'd just go into a loop. *) + let lbs = + match (pat, typ) with + | P_aux (P_tuple pats, _), Typ_aux (Typ_tuple typs, _) -> List.concat (List.map2 aux pats typs) + | _ -> [] + in + List.fold_left add_lb exp lbs + let string_of_exp_con (E_aux (e, _)) = match e with | E_block _ -> "E_block" @@ -263,14 +372,28 @@ let string_of_exp_con (E_aux (e, _)) = | E_vector _ -> "E_vector" | E_let _ -> "E_let" -let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = +let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) = let env = env_of_tannot annot in match e with | E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *) | E_lit l -> doc_lit l | E_app (Id_aux (Id "internal_pick", _), _) -> string "sorry" (* TODO replace by actual implementation of internal_pick *) - | E_internal_plet _ -> string "sorry" (* TODO replace by actual implementation of internal_plet *) + | E_internal_plet (pat, e1, e2) -> + (* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *) + let e0 = doc_pat ctxt false pat in + let e1_pp = doc_exp ctxt e1 in + let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in + let e2_pp = doc_exp ctxt e2' in + (* infix 0 1 middle e1_pp e2_pp *) + let e0_pp = + begin + match pat with + | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string "" + | _ -> separate space [string "let"; e0; string ":="] ^^ space + end + in + e0_pp ^^ e1_pp ^^ hardline ^^ e2_pp | E_app (f, args) -> let d_id = if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") @@ -279,7 +402,11 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = let d_args = List.map (doc_exp ctxt) args in nest 2 (parens (flow (break 1) (d_id :: d_args))) | E_vector vals -> failwith "vector found" - | E_typ (typ, e) -> parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ]) + | E_typ (typ, e) -> begin + match e with + | E_aux (E_assign _, _) -> doc_exp ctxt e + | _ -> parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ]) + end | E_tuple es -> parens (separate_map (comma ^^ space) (doc_exp ctxt) es) | E_let (LB_aux (LB_val (lpat, lexp), _), e) -> let id = @@ -292,14 +419,20 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) = | E_struct fexps -> let args = List.map (doc_fexp ctxt) fexps in braces (separate comma args) - | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id + | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor ctxt id | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args) + | E_assign ((LE_aux (le_act, tannot) as le), e) -> string "set_" ^^ doc_lexp_deref ctxt le ^^ space ^^ doc_exp ctxt e | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") -and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp +and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor ctxt field ^^ string " := " ^^ doc_exp ctxt exp +and doc_lexp_deref ctxt (LE_aux (lexp, (l, annot))) = + match lexp with + | LE_id id -> doc_id ctxt id + | LE_typ (typ, id) -> doc_id ctxt id + | _ -> raise (Reporting.err_unreachable l __POS__ "doc_lexp_deref: Unsupported lexp") let doc_binder ctxt i t = let paranthesizer = match t with @@ -311,7 +444,7 @@ let doc_binder ctxt i t = let ctxt = match captured_typ_var (i, t) with Some (i, ki) -> add_single_kid_id_rename ctxt i ki | _ -> ctxt in (ctxt, separate space [string (string_of_id i); colon; doc_typ ctxt t] |> paranthesizer) -let doc_funcl_init (FCL_aux (FCL_funcl (id, pexp), annot)) = +let doc_funcl_init ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) = let env = env_of_tannot (snd annot) in let TypQ_aux (tq, l), typ = Env.get_val_spec_orig id env in let arg_typs, ret_typ, _ = @@ -330,7 +463,6 @@ let doc_funcl_init (FCL_aux (FCL_funcl (id, pexp), annot)) = | _ -> failwith "Argument pattern not translatable yet." ) in - let ctxt = empty_context in let ctxt, binders = List.fold_left (fun (ctxt, bs) (i, t) -> @@ -357,19 +489,19 @@ let doc_funcl_init (FCL_aux (FCL_funcl (id, pexp), annot)) = separate space ([string "def"; string (string_of_id id)] @ binders @ [colon; doc_ret_typ; coloneq]) ) -let doc_funcl_body (FCL_aux (FCL_funcl (id, pexp), annot)) = +let doc_funcl_body ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) = let _, _, exp, _ = destruct_pexp pexp in let is_monadic = effectful (effect_of exp) in if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp empty_context exp]) else doc_exp empty_context exp -let doc_funcl funcl = - let comment, signature = doc_funcl_init funcl in - comment ^^ nest 2 (signature ^^ hardline ^^ doc_funcl_body funcl) +let doc_funcl ctxt funcl = + let comment, signature = doc_funcl_init ctxt funcl in + comment ^^ nest 2 (signature ^^ hardline ^^ doc_funcl_body ctxt funcl) -let doc_fundef (FD_aux (FD_function (r, typa, fcls), fannot)) = +let doc_fundef ctxt (FD_aux (FD_function (r, typa, fcls), fannot)) = match fcls with | [] -> failwith "FD_function with empty function list" - | [funcl] -> doc_funcl funcl + | [funcl] -> doc_funcl ctxt funcl | _ -> failwith "FD_function with more than one clause" let string_of_type_def_con (TD_aux (td, _)) = @@ -385,7 +517,7 @@ let doc_typdef ctxt (TD_aux (td, tannot) as full_typdef) = match td with | TD_enum (Id_aux (Id id, _), fields, _) -> let derivers = if List.length fields > 0 then [string "Inhabited"] else [] in - let fields = List.map doc_id_ctor fields in + let fields = List.map (doc_id_ctor ctxt) fields in let fields = List.map (fun i -> space ^^ pipe ^^ space ^^ i) fields in let enums_doc = concat fields in nest 2 @@ -407,7 +539,7 @@ let doc_typdef ctxt (TD_aux (td, tannot) as full_typdef) = let doc_def ctxt (DEF_aux (aux, def_annot) as def) = match aux with - | DEF_fundef fdef -> group (doc_fundef fdef) ^/^ hardline + | DEF_fundef fdef -> group (doc_fundef ctxt fdef) ^/^ hardline | DEF_type tdef -> group (doc_typdef ctxt tdef) ^/^ hardline | _ -> empty @@ -419,8 +551,11 @@ let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.en | DEF_aux (DEF_pragma ("include_end", _, _), _) :: ds -> remove_imports ds (depth - 1) | d :: ds -> if depth > 0 then remove_imports ds depth else d :: remove_imports ds depth -let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = +let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o effect_info = let defs = remove_imports defs 0 in - let output : document = separate_map empty (doc_def empty_context) defs in - print o output; + let global = { effect_info } in + let ctxt = { empty_context with global } in + let register_refs = State.register_refs_lean (doc_id ctxt) (doc_typ ctxt) (State.find_registers defs) in + let output : document = separate_map empty (doc_def ctxt) defs in + print o (register_refs ^^ hardline ^^ output); () diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml index 45240cc0b..91e200d89 100644 --- a/src/sail_lean_backend/sail_plugin_lean.ml +++ b/src/sail_lean_backend/sail_plugin_lean.ml @@ -190,15 +190,15 @@ let create_lake_project (out_name : string) default_sail_dir = output_string project_main "open Sail\n\n"; project_main -let output (out_name : string) ast default_sail_dir = +let output (out_name : string) ast default_sail_dir effect_info = let project_main = create_lake_project out_name default_sail_dir in (* Uncomment for debug output of the Sail code after the rewrite passes *) (* Pretty_print_sail.output_ast stdout (Type_check.strip_ast ast); *) - Pretty_print_lean.pp_ast_lean ast project_main; + Pretty_print_lean.pp_ast_lean ast project_main effect_info; close_out project_main let lean_target out_name { default_sail_dir; ctx; ast; effect_info; env; _ } = let out_name = match out_name with Some f -> f | None -> "out" in - output out_name ast default_sail_dir + output out_name ast default_sail_dir effect_info let _ = Target.register ~name:"lean" ~options:lean_options ~rewrites:lean_rewrites ~asserts_termination:true lean_target From b30421f228bc9ae70f7c8db5d14aadebf489d7aa Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Mon, 13 Jan 2025 14:40:10 +0100 Subject: [PATCH 42/54] add placeholer for state monad to stateful functions --- test/lean/enum.expected.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean index d49feafc4..c0fa88e69 100644 --- a/test/lean/enum.expected.lean +++ b/test/lean/enum.expected.lean @@ -5,7 +5,7 @@ open Sail inductive E where | A | B | C deriving Inhabited -def undefined_E : SailM E := +def undefined_E : SailM E := do return (sorry : E) def initialize_registers : Unit := From aae09c27f107cc031e0efb8b924d2d3b2ae9c609 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 14 Jan 2025 13:38:30 +0000 Subject: [PATCH 43/54] changes after merge --- src/lib/state.ml | 8 ++++---- src/sail_lean_backend/pretty_print_lean.ml | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/lib/state.ml b/src/lib/state.ml index d75f1aaa7..f4c65558e 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -835,7 +835,7 @@ let register_refs_coq doc_id coq_record_update env registers = separate hardline [generic_convs; refs; getters_setters] let register_refs_lean doc_id doc_typ registers = - let generic_convs = separate_map hardline string [""; "variable [MonadReg m] [Monad m]"; ""; "open MonadReg"; ""] in + let generic_convs = separate_map hardline string [""; "variable [MonadReg]"; ""; "open MonadReg"; ""] in let register_ref (typ, id, _) = let idd = doc_id id in let typp = doc_typ typ in @@ -847,19 +847,19 @@ let register_refs_lean doc_id doc_typ registers = colon; space; typp; - string " -> m Unit"; + string " -> SailM Unit"; hardline; string " get_"; idd; colon; space; - string "m ("; + string "SailM ("; typp; string ")"; ] in let refs = separate_map hardline register_ref registers in - separate hardline [string "class MonadReg (m : Type -> Type) where"; refs; generic_convs] + separate hardline [string "class MonadReg where"; refs; generic_convs] let generate_regstate_defs ctx env ast = let defs = ast.defs in diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 06834c243..d649c6cff 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -492,11 +492,11 @@ let doc_funcl_init ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) = let doc_funcl_body ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) = let _, _, exp, _ = destruct_pexp pexp in let is_monadic = effectful (effect_of exp) in - if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp empty_context exp]) else doc_exp empty_context exp + if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp ctxt exp]) else doc_exp ctxt exp let doc_funcl ctxt funcl = - let comment, signature = doc_funcl_init ctxt funcl in - comment ^^ nest 2 (signature ^^ hardline ^^ doc_funcl_body ctxt funcl) + let signature = doc_funcl_init ctxt funcl in + nest 2 (signature ^^ hardline ^^ doc_funcl_body ctxt funcl) let doc_fundef ctxt (FD_aux (FD_function (r, typa, fcls), fannot)) = match fcls with From 829d1d3f401a3f16cf66d2899853d54ac4ea81e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 14 Jan 2025 13:39:47 +0000 Subject: [PATCH 44/54] Adding test --- test/lean/reg.expected.lean | 16 ++++++++++++++++ test/lean/reg.sail | 5 +++++ 2 files changed, 21 insertions(+) create mode 100644 test/lean/reg.expected.lean create mode 100644 test/lean/reg.sail diff --git a/test/lean/reg.expected.lean b/test/lean/reg.expected.lean new file mode 100644 index 000000000..feabf3399 --- /dev/null +++ b/test/lean/reg.expected.lean @@ -0,0 +1,16 @@ +import Reg.Sail.Sail + +open Sail + +class MonadReg where + set_R0: BitVec 64 -> SailM Unit + get_R0: SailM (BitVec 64) + +variable [MonadReg] + +open MonadReg + +def initialize_registers : SailM Unit := do + let w__0 := (undefined_bitvector 64) + set_R0 w__0 + return () diff --git a/test/lean/reg.sail b/test/lean/reg.sail new file mode 100644 index 000000000..0b2a367ab --- /dev/null +++ b/test/lean/reg.sail @@ -0,0 +1,5 @@ +default Order dec + +$include + +register R0 : bits(64) \ No newline at end of file From 07fd6d3d813e303aa9d840ab8d0f3941ef5f5cb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 14 Jan 2025 14:03:51 +0000 Subject: [PATCH 45/54] fix in case of no register --- src/sail_lean_backend/pretty_print_lean.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index d649c6cff..fbc84f56b 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -555,7 +555,8 @@ let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o effect_inf let defs = remove_imports defs 0 in let global = { effect_info } in let ctxt = { empty_context with global } in - let register_refs = State.register_refs_lean (doc_id ctxt) (doc_typ ctxt) (State.find_registers defs) in + let regs = State.find_registers defs in + let register_refs = match regs with [] -> empty | _ -> State.register_refs_lean (doc_id ctxt) (doc_typ ctxt) regs in let output : document = separate_map empty (doc_def ctxt) defs in print o (register_refs ^^ hardline ^^ output); () From 41bdd9dc75f57aae721223924a4064d8eae07f4a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 14 Jan 2025 14:47:52 +0000 Subject: [PATCH 46/54] removing extra hardline when there is no register --- src/sail_lean_backend/pretty_print_lean.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index fbc84f56b..5c1fa63e6 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -556,7 +556,9 @@ let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o effect_inf let global = { effect_info } in let ctxt = { empty_context with global } in let regs = State.find_registers defs in - let register_refs = match regs with [] -> empty | _ -> State.register_refs_lean (doc_id ctxt) (doc_typ ctxt) regs in + let register_refs = + match regs with [] -> empty | _ -> State.register_refs_lean (doc_id ctxt) (doc_typ ctxt) regs ^^ hardline + in let output : document = separate_map empty (doc_def ctxt) defs in - print o (register_refs ^^ hardline ^^ output); + print o (register_refs ^^ output); () From e064d634d4e7c72c2f9a0d63e3db673c477e0a1f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 14 Jan 2025 14:48:05 +0000 Subject: [PATCH 47/54] adding force-output to the lean tests --- test/lean/run_tests.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/lean/run_tests.py b/test/lean/run_tests.py index 8b140c16f..e38e2ecee 100755 --- a/test/lean/run_tests.py +++ b/test/lean/run_tests.py @@ -27,7 +27,7 @@ def test_lean(): tests[filename] = os.fork() if tests[filename] == 0: step('mkdir {}'.format(basename)) - step('\'{}\' {} --lean --lean-output-dir {}'.format(sail, filename, basename)) + step('\'{}\' {} --lean --lean-output-dir --lean-force-output {}'.format(sail, filename, basename)) step('diff {}/out/Out.lean {}.expected.lean'.format(basename, basename)) step('rm -r {}'.format(basename)) print_ok(filename) From 77c82863c18d474ef23683eee56c4e87dbf6daf2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 15 Jan 2025 13:15:38 +0000 Subject: [PATCH 48/54] Starting to fix the broken tests --- src/sail_lean_backend/Sail/Sail.lean | 6 ++++++ src/sail_lean_backend/pretty_print_lean.ml | 10 ++++++---- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 22c3e5292..e3abc1000 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -35,3 +35,9 @@ end Sail def undefined_bitvector (n: Nat) : BitVec n := 0#n + +def undefined_int (lit: Unit) : Int := + 0 + +def undefined_bit (lit: Unit) : BitVec 1 := + undefined_bitvector 1 diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 5c1fa63e6..aec7ab449 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -424,6 +424,7 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) = let args = List.map (doc_fexp ctxt) fexps in braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args) | E_assign ((LE_aux (le_act, tannot) as le), e) -> string "set_" ^^ doc_lexp_deref ctxt le ^^ space ^^ doc_exp ctxt e + | E_internal_return e -> nest 2 (flow (break 1) [string "return"; doc_exp ctxt e]) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor ctxt field ^^ string " := " ^^ doc_exp ctxt exp @@ -491,12 +492,13 @@ let doc_funcl_init ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) = let doc_funcl_body ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) = let _, _, exp, _ = destruct_pexp pexp in - let is_monadic = effectful (effect_of exp) in - if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp ctxt exp]) else doc_exp ctxt exp + (* let is_monadic = effectful (effect_of exp) in + if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp ctxt exp]) else doc_exp ctxt exp *) + doc_exp ctxt exp let doc_funcl ctxt funcl = - let signature = doc_funcl_init ctxt funcl in - nest 2 (signature ^^ hardline ^^ doc_funcl_body ctxt funcl) + let comment, signature = doc_funcl_init ctxt funcl in + comment ^^ nest 2 (signature ^^ hardline ^^ doc_funcl_body ctxt funcl) let doc_fundef ctxt (FD_aux (FD_function (r, typa, fcls), fannot)) = match fcls with From 272963419eee6b08350d08cdaf9f3bcee04027cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 15 Jan 2025 13:17:49 +0000 Subject: [PATCH 49/54] Formatting --- src/sail_lean_backend/pretty_print_lean.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index aec7ab449..d5ea10d3f 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -493,7 +493,7 @@ let doc_funcl_init ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) = let doc_funcl_body ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) = let _, _, exp, _ = destruct_pexp pexp in (* let is_monadic = effectful (effect_of exp) in - if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp ctxt exp]) else doc_exp ctxt exp *) + if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp ctxt exp]) else doc_exp ctxt exp *) doc_exp ctxt exp let doc_funcl ctxt funcl = From 88dce4a5949202334aeb4c9a5c1ae8670536644f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 15 Jan 2025 13:22:10 +0000 Subject: [PATCH 50/54] Fix run_tests --- test/lean/run_tests.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/lean/run_tests.py b/test/lean/run_tests.py index e38e2ecee..8b140c16f 100755 --- a/test/lean/run_tests.py +++ b/test/lean/run_tests.py @@ -27,7 +27,7 @@ def test_lean(): tests[filename] = os.fork() if tests[filename] == 0: step('mkdir {}'.format(basename)) - step('\'{}\' {} --lean --lean-output-dir --lean-force-output {}'.format(sail, filename, basename)) + step('\'{}\' {} --lean --lean-output-dir {}'.format(sail, filename, basename)) step('diff {}/out/Out.lean {}.expected.lean'.format(basename, basename)) step('rm -r {}'.format(basename)) print_ok(filename) From 3bd82785e112eaa470794d25c197b1bf3eaa3d3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 15 Jan 2025 13:24:01 +0000 Subject: [PATCH 51/54] Actually fixing --- test/lean/reg.expected.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/lean/reg.expected.lean b/test/lean/reg.expected.lean index feabf3399..41078f42a 100644 --- a/test/lean/reg.expected.lean +++ b/test/lean/reg.expected.lean @@ -1,4 +1,4 @@ -import Reg.Sail.Sail +import Out.Sail.Sail open Sail From 995a7b91435fd9df4deb3a0c01116193e0f1ac0b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 15 Jan 2025 13:38:57 +0000 Subject: [PATCH 52/54] Fixing more tests --- src/sail_lean_backend/pretty_print_lean.ml | 2 ++ test/lean/struct.expected.lean | 7 +++++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index d5ea10d3f..b9d2f317f 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -405,6 +405,8 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) = | E_typ (typ, e) -> begin match e with | E_aux (E_assign _, _) -> doc_exp ctxt e + | E_aux (E_app (Id_aux (Id "internal_pick", _), _), _) -> + string "return " ^^ parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ]) | _ -> parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ]) end | E_tuple es -> parens (separate_map (comma ^^ space) (doc_exp ctxt) es) diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index c2a979dfd..6a9dc0cd1 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -6,8 +6,11 @@ structure My_struct where field1 : Int field2 : (BitVec 1) -def undefined_My_struct (lit : Unit) : SailM My_struct := - return sorry + +def undefined_My_struct (lit : Unit) : SailM My_struct := do + let w__0 := (undefined_int ()) + let w__1 := (undefined_bit ()) + return {field1 := w__0,field2 := w__1} def struct_field2 (s : My_struct) : (BitVec 1) := s.field2 From 573e52075e4f41f72621c412dda4c7beb3021d25 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 17 Jan 2025 14:26:02 +0000 Subject: [PATCH 53/54] formating --- src/sail_lean_backend/pretty_print_lean.ml | 28 +++++++++++----------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 8a64d33cd..d301d5c16 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -380,20 +380,20 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) = | E_app (Id_aux (Id "internal_pick", _), _) -> string "sorry" (* TODO replace by actual implementation of internal_pick *) | E_internal_plet (pat, e1, e2) -> - (* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *) - let e0 = doc_pat ctxt false pat in - let e1_pp = doc_exp ctxt e1 in - let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in - let e2_pp = doc_exp ctxt e2' in - (* infix 0 1 middle e1_pp e2_pp *) - let e0_pp = - begin - match pat with - | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string "" - | _ -> separate space [string "let"; e0; string ":="] ^^ space - end - in - e0_pp ^^ e1_pp ^^ hardline ^^ e2_pp + (* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *) + let e0 = doc_pat ctxt false pat in + let e1_pp = doc_exp ctxt e1 in + let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in + let e2_pp = doc_exp ctxt e2' in + (* infix 0 1 middle e1_pp e2_pp *) + let e0_pp = + begin + match pat with + | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string "" + | _ -> separate space [string "let"; e0; string ":="] ^^ space + end + in + e0_pp ^^ e1_pp ^^ hardline ^^ e2_pp | E_app (f, args) -> let d_id = if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") From 8de835121f617f91a3089ade6f2f6db65cd07707 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 17 Jan 2025 14:28:00 +0000 Subject: [PATCH 54/54] final push before making a clean branch --- src/sail_lean_backend/pretty_print_lean.ml | 11 ++++++++--- test/lean/enum.expected.lean | 2 +- test/lean/reg.expected.lean | 8 ++++---- test/lean/struct.expected.lean | 12 +++--------- 4 files changed, 16 insertions(+), 17 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index d301d5c16..e7ead06ef 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -406,7 +406,7 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) = match e with | E_aux (E_assign _, _) -> doc_exp ctxt e | E_aux (E_app (Id_aux (Id "internal_pick", _), _), _) -> - string "return " ^^ parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ]) + string "return " ^^ nest 7 (parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ])) | _ -> parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ]) end | E_tuple es -> parens (separate_map (comma ^^ space) (doc_exp ctxt) es) @@ -425,8 +425,13 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) = | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctxt) fexps in braces (space ^^ doc_exp ctxt exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space) - | E_assign ((LE_aux (le_act, tannot) as le), e) -> string "set_" ^^ doc_lexp_deref ctxt le ^^ space ^^ doc_exp ctxt e - | E_internal_return e -> nest 2 (flow (break 1) [string "return"; doc_exp ctxt e]) + | E_assign ((LE_aux (le_act, tannot) as le), e) -> ( + match le_act with + | LE_id id | LE_typ (_, id) -> string "set_" ^^ doc_id ctxt id ^^ space ^^ doc_exp ctxt e + | LE_deref e -> string "sorry /- deref -/" + | _ -> failwith ("assign " ^ string_of_lexp le ^ "not implemented yet") + ) + | E_internal_return e -> nest 2 (string "return" ^^ space ^^ nest 5 (doc_exp ctxt e)) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor ctxt field ^^ string " := " ^^ doc_exp ctxt exp diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean index c0fa88e69..d49feafc4 100644 --- a/test/lean/enum.expected.lean +++ b/test/lean/enum.expected.lean @@ -5,7 +5,7 @@ open Sail inductive E where | A | B | C deriving Inhabited -def undefined_E : SailM E := do +def undefined_E : SailM E := return (sorry : E) def initialize_registers : Unit := diff --git a/test/lean/reg.expected.lean b/test/lean/reg.expected.lean index 41078f42a..00e105040 100644 --- a/test/lean/reg.expected.lean +++ b/test/lean/reg.expected.lean @@ -3,14 +3,14 @@ import Out.Sail.Sail open Sail class MonadReg where - set_R0: BitVec 64 -> SailM Unit - get_R0: SailM (BitVec 64) + set_R0: (BitVec 64) -> SailM Unit + get_R0: SailM ((BitVec 64)) variable [MonadReg] open MonadReg -def initialize_registers : SailM Unit := do +def initialize_registers : SailM Unit := let w__0 := (undefined_bitvector 64) set_R0 w__0 - return () + diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index 9f0e40dca..eedc24d7e 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -6,17 +6,11 @@ structure My_struct where field1 : Int field2 : (BitVec 1) - -def undefined_My_struct (lit : Unit) : SailM My_struct := do +def undefined_My_struct (lit : Unit) : SailM My_struct := let w__0 := (undefined_int ()) let w__1 := (undefined_bit ()) - return {field1 := w__0,field2 := w__1} - -def struct_field2 (s : My_struct) : (BitVec 1) := - s.field2 - -def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct := - {s with field2 := b} + return { field1 := w__0 + field2 := w__1 } def struct_field2 (s : My_struct) : (BitVec 1) := s.field2