Lean: Memory model (#965)

This closes #959. Adds SailTinyArm as a test.

Co-authored-by: Léo Stefanesco <[email protected]>

lib/concurrency_interface/common.sail

@@ -48,7 +48,7 @@ $sail_internal
 
 $target_set emulator_or_isla isla c ocaml interpreter systemverilog
 $target_set emulator c ocaml interpreter systemverilog
-$target_set prover lem coq
+$target_set prover lem coq lean
 
 $ifndef _CONCURRENCY_INTERFACE_COMMON
 $define _CONCURRENCY_INTERFACE_COMMON

lib/concurrency_interface/read_write.sail

@@ -53,6 +53,7 @@ $include <concurrency_interface/common.sail>
 
 $option -lem_extern_type Access_variety
 $option -coq_extern_type Access_variety
+$option -lean_extern_type Access_variety
 enum Access_variety = {
   AV_plain,
   AV_exclusive,
@@ -61,6 +62,7 @@ enum Access_variety = {
 
 $option -lem_extern_type Access_strength
 $option -coq_extern_type Access_strength
+$option -lean_extern_type Access_strength
 enum Access_strength = {
   AS_normal,
   AS_rel_or_acq, // Release or acquire
@@ -69,13 +71,15 @@ enum Access_strength = {
 
 $option -lem_extern_type Explicit_access_kind
 $option -coq_extern_type Explicit_access_kind
+$option -lean_extern_type Explicit_access_kind
 struct Explicit_access_kind = {
   variety : Access_variety,
   strength : Access_strength
 }
 
 $option -lem_extern_type Access_kind
 $option -coq_extern_type Access_kind
+$option -lean_extern_type Access_kind
 union Access_kind('arch_ak : Type) = {
   AK_explicit: Explicit_access_kind,
   AK_ifetch : unit, // Instruction fetch
@@ -85,6 +89,7 @@ union Access_kind('arch_ak : Type) = {
 
 $option -lem_extern_type Mem_read_request
 $option -coq_extern_type Mem_read_request
+$option -lean_extern_type Mem_read_request
 struct Mem_read_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
                         'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),
@@ -181,6 +186,7 @@ with
 
 $option -lem_extern_type Mem_write_request
 $option -coq_extern_type Mem_write_request
+$option -lean_extern_type Mem_write_request
 struct Mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
                          'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),

lib/result.sail

@@ -56,6 +56,7 @@ $include <option.sail>
 
 $option -lem_extern_type result
 $option -coq_extern_type result
+$option -lean_extern_type result
 union result('a : Type, 'b : Type) = {
     Ok : 'a,
     Err : 'b

src/sail_lean_backend/Sail/Sail.lean

@@ -1,4 +1,5 @@
 import Std.Data.DHashMap
+import Std.Data.HashMap
 namespace Sail
 
 section Regs
@@ -41,22 +42,36 @@ def trivialChoiceSource : ChoiceSource where
     | .fin _ => 0
     | .bitvector _ => 0
 
+class Arch where
+  va_size : Nat
+  pa : Type
+  arch_ak : Type
+  translation : Type
+  abort : Type
+  barrier : Type
+  cache_op : Type
+  tlb_op : Type
+  fault : Type
+  sys_reg_id : Type
+
 /- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/
 inductive Error where
   | Exit
   | Unreachable
+  | OutOfMemoryRange (n : Nat)
   | Assertion (s : String)
 open Error
 
 def Error.print : Error → String
-| Exit => "Exit"
-| Unreachable => "Unreachable"
-| Assertion s => s!"Assertion failed: {s}"
+  | Exit => "Exit"
+  | Unreachable => "Unreachable"
+  | OutOfMemoryRange n => s!"{n} Out of Memory Range"
+  | Assertion s => s!"Assertion failed: {s}"
 
 structure SequentialState (RegisterType : Register → Type) (c : ChoiceSource) where
   regs : Std.DHashMap Register RegisterType
   choiceState : c.α
-  mem : Unit
+  mem : Std.HashMap Nat (BitVec 8)
   tags : Unit
   sail_output : Array String -- TODO: be able to use the IO monad to run
 
@@ -122,7 +137,104 @@ def vectorUpdate (v : Vector α m) (n : Nat) (a : α) := v.set! n a
 def assert (p : Bool) (s : String) : PreSailM RegisterType c Unit :=
   if p then pure () else throw (Assertion s)
 
-/- def print_effect (s : String) : IO Unit := IO.print s -/
+section ConcurrencyInterface
+
+inductive Access_variety where
+| AV_plain
+| AV_exclusive
+| AV_atomic_rmw
+export Access_variety (AV_plain AV_exclusive AV_atomic_rmw)
+
+inductive Access_strength where
+| AS_normal
+| AS_rel_or_acq
+| AS_acq_rcpc
+export Access_strength(AS_normal AS_rel_or_acq AS_acq_rcpc)
+
+structure Explicit_access_kind where
+  variety : Access_variety
+  strength : Access_strength
+
+inductive Access_kind (arch : Type) where
+  | AK_explicit (_ : Explicit_access_kind)
+  | AK_ifetch (_ : Unit)
+  | AK_ttw (_ : Unit)
+  | AK_arch (_ : arch)
+export Access_kind(AK_explicit AK_ifetch AK_ttw AK_arch)
+
+inductive Result (α : Type) (β : Type) where
+  | Ok (_ : α)
+  | Err (_ : β)
+export Result(Ok Err)
+
+structure Mem_read_request
+  (n : Nat) (vasize : Nat) (pa : Type) (ts : Type) (arch_ak : Type) where
+  access_kind : Access_kind arch_ak
+  va : (Option (BitVec vasize))
+  pa : pa
+  translation : ts
+  size : Int
+  tag : Bool
+
+structure Mem_write_request
+  (n : Nat) (vasize : Nat) (pa : Type) (ts : Type) (arch_ak : Type) where
+  access_kind : Access_kind arch_ak
+  va : (Option (BitVec vasize))
+  pa : pa
+  translation : ts
+  size : Int
+  value : (Option (BitVec (8 * n)))
+  tag : (Option Bool)
+
+def writeByte (addr : Nat) (value : BitVec 8) : PreSailM RegisterType c PUnit := do
+  match (← get).mem.containsThenInsert addr value with
+    | (true, m) => modify fun s => { s with mem := m }
+    | (false, _) => throw (OutOfMemoryRange addr)
+
+def writeBytes (addr : Nat) (value : BitVec (8 * n)) : PreSailM RegisterType c Bool := do
+  let list := List.ofFn (λ i : Fin n => (addr + i, value.extractLsb' (8 * i) 8))
+  List.forM list (λ (a, v) => writeByte a v)
+  pure true
+
+def sail_mem_write [Arch] (req : Mem_write_request n vasize (BitVec pa_size) ts arch) : PreSailM RegisterType c (Result (Option Bool) Arch.abort) := do
+  let addr := req.pa.toNat
+  let b ← match req.value with
+    | some v => writeBytes addr v
+    | none => pure true
+  pure (Ok (some b))
+
+def write_ram (addr_size data_size : Nat) (_hex_ram addr : BitVec addr_size) (value : BitVec (8 * data_size)) :
+    PreSailM RegisterType c Unit := do
+  let _ ← writeBytes addr.toNat value
+  pure ()
+
+def readByte (addr : Nat) : PreSailM RegisterType c (BitVec 8) := do
+  let .some s := (← get).mem.get? addr
+    | throw (OutOfMemoryRange addr)
+  pure s
+
+def readBytes (size : Nat) (addr : Nat) : PreSailM RegisterType c ((BitVec (8 * size)) × Option Bool) :=
+  match size with
+  | 0 => pure (default, none)
+  | n + 1 => do
+    let b ← readByte addr
+    let (bytes, bool) ← readBytes n (addr+1)
+    have h : 8 + 8 * n = 8 * (n + 1) := by omega
+    return (h ▸ b.append bytes, bool)
+
+def sail_mem_read [Arch] (req : Mem_read_request n vasize (BitVec pa_size) ts arch) : PreSailM RegisterType c (Result ((BitVec (8 * n)) × (Option Bool)) Arch.abort) := do
+  let addr := req.pa.toNat
+  let value ← readBytes n addr
+  pure (Ok value)
+
+def read_ram (addr_size data_size : Nat) (_hex_ram addr : BitVec addr_size) : PreSailM RegisterType c (BitVec (8 * data_size)) := do
+  let ⟨bytes, _⟩ ← readBytes data_size addr.toNat
+  pure bytes
+
+
+def sail_barrier (_ : α) : PreSailM RegisterType c Unit := pure ()
+
+end ConcurrencyInterface
 
 def print_effect (str : String) : PreSailM RegisterType c Unit :=
   modify fun s ↦ { s with sail_output := s.sail_output.push str }

src/sail_lean_backend/pretty_print_lean.ml

@@ -9,6 +9,9 @@ open Rewriter
 open PPrint
 open Pretty_print_common
 
+(* Command line options *)
+let opt_extern_types : string list ref = ref []
+
 type global_context = { effect_info : Effects.side_effect_info }
 
 let the_main_function_has_been_seen = ref false
@@ -365,6 +368,27 @@ let string_of_pat_con (P_aux (p, _)) =
   | P_string_append _ -> "P_string_append"
   | P_struct _ -> "P_struct"
 
+let string_of_def (DEF_aux (d, _)) =
+  match d with
+  | DEF_type _ -> "DEF_type"
+  | DEF_constraint _ -> "DEF_constraint"
+  | DEF_fundef _ -> "DEF_fundef"
+  | DEF_mapdef _ -> "DEF_mapdef"
+  | DEF_impl _ -> "DEF_impl"
+  | DEF_let _ -> "DEF_let"
+  | DEF_val (VS_aux (VS_val_spec (_, id, _), _)) -> "DEF_val " ^ string_of_id id
+  | DEF_outcome _ -> "DEF_outcome"
+  | DEF_instantiation _ -> "DEF_instantiation"
+  | DEF_fixity _ -> "DEF_fixity"
+  | DEF_overload _ -> "DEF_overload"
+  | DEF_default _ -> "DEF_default"
+  | DEF_scattered _ -> "DEF_scattered"
+  | DEF_measure _ -> "DEF_measure"
+  | DEF_loop_measures _ -> "DEF_loop_measures"
+  | DEF_register _ -> "DEF_register"
+  | DEF_internal_mutrec _ -> "DEF_internal_mutrec"
+  | DEF_pragma _ -> "DEF_pragma"
+
 (** Fix identifiers to match the standard Lean library. *)
 let fixup_match_id (Id_aux (id, l) as id') =
   match id with Id id -> Id_aux (Id (match id with "Some" -> "some" | "None" -> "none" | _ -> id), l) | _ -> id'
@@ -496,7 +520,11 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
       else wrap_with_pure as_monadic (parens (separate space [doc_exp false ctx e; colon; doc_typ ctx typ]))
   | E_tuple es -> wrap_with_pure as_monadic (parens (separate_map (comma ^^ space) d_of_arg es))
   | E_let (LB_aux (LB_val (lpat, lexp), _), e) ->
-      let id_typ = doc_pat lpat in
+      let id_typ =
+        match pat_is_plain_binder env lpat with
+        | Some (_, Some typ) -> doc_pat lpat ^^ space ^^ colon ^^ space ^^ doc_typ ctx typ
+        | _ -> doc_pat lpat
+      in
       let decl_val =
         if effectful (effect_of lexp) then [string "←"; string "do"; doc_exp true ctx lexp]
         else [coloneq; doc_exp false ctx lexp]
@@ -516,9 +544,7 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
         (braces (space ^^ doc_exp false ctx exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space))
   | E_match (discr, brs) ->
       let cases = separate_map hardline (doc_match_clause as_monadic ctx) brs in
-      string (match_or_match_bv brs)
-      ^^ doc_exp (effectful (effect_of discr)) ctx discr
-      ^^ string " with" ^^ hardline ^^ cases
+      string (match_or_match_bv brs) ^^ doc_exp false ctx discr ^^ string " with" ^^ hardline ^^ cases
   | E_assign ((LE_aux (le_act, tannot) as le), e) -> (
       match le_act with
       | LE_id id | LE_typ (_, id) -> string "writeReg " ^^ doc_id_ctor id ^^ space ^^ doc_exp false ctx e
@@ -695,6 +721,8 @@ let rec doc_defs_rec ctx defs types docdefs =
   | [] -> (types, docdefs)
   | DEF_aux (DEF_fundef fdef, _) :: defs' ->
       doc_defs_rec ctx defs' types (docdefs ^^ group (doc_fundef ctx fdef) ^/^ hardline)
+  | DEF_aux (DEF_type tdef, _) :: defs' when List.mem (string_of_id (id_of_type_def tdef)) !opt_extern_types ->
+      doc_defs_rec ctx defs' types docdefs
   | DEF_aux (DEF_type tdef, _) :: defs' ->
       doc_defs_rec ctx defs' (types ^^ group (doc_typdef ctx tdef) ^/^ hardline) docdefs
   | DEF_aux (DEF_let (LB_aux (LB_val (pat, exp), _)), _) :: defs' ->
@@ -757,6 +785,28 @@ let doc_monad_abbrev (has_registers : bool) =
   in
   separate space [string "abbrev"; string "SailM"; coloneq; pp_register_type] ^^ hardline ^^ hardline
 
+let doc_instantiations ctx env =
+  let params = Monad_params.find_monad_parameters env in
+  match params with
+  | None -> empty
+  | Some params ->
+      nest 2
+        (separate hardline
+           [
+             string "instance : Arch where";
+             string "va_size := 64";
+             string "pa := " ^^ doc_typ ctx params.pa_type;
+             string "abort := " ^^ doc_typ ctx params.abort_type;
+             string "translation := " ^^ doc_typ ctx params.translation_summary_type;
+             string "fault := " ^^ doc_typ ctx params.fault_type;
+             string "tlb_op := " ^^ doc_typ ctx params.tlbi_type;
+             string "cache_op := " ^^ doc_typ ctx params.cache_op_type;
+             string "barrier := " ^^ doc_typ ctx params.barrier_type;
+             string "arch_ak := " ^^ doc_typ ctx params.arch_ak_type;
+             string "sys_reg_id := " ^^ doc_typ ctx params.sys_reg_id_type ^^ hardline;
+           ]
+        )
+      ^^ hardline
 let main_function_stub =
   nest 2
     (separate hardline
@@ -769,13 +819,16 @@ let main_function_stub =
     )
 
 let pp_ast_lean (env : Type_check.env) effect_info ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o =
+  (* TODO: remove the following line once we can handle the includes *)
   let defs = remove_imports defs 0 in
   let regs = State.find_registers defs in
   let global = { effect_info } in
+  let ctx = initial_context env global in
   let has_registers = List.length regs > 0 in
   let register_refs = if has_registers then doc_reg_info env global regs else empty in
   let monad = doc_monad_abbrev has_registers in
-  let types, fundefs = doc_defs (initial_context env global) defs in
+  let instantiations = doc_instantiations ctx env in
+  let types, fundefs = doc_defs ctx defs in
   let main_function = if !the_main_function_has_been_seen then main_function_stub else empty in
-  print o (types ^^ register_refs ^^ monad ^^ fundefs ^^ main_function);
+  print o (types ^^ register_refs ^^ monad ^^ instantiations ^^ fundefs ^^ main_function);
   !the_main_function_has_been_seen

src/sail_lean_backend/sail_plugin_lean.ml

@@ -85,6 +85,10 @@ let lean_options =
       Arg.Unit (fun () -> opt_lean_force_output := true),
       "removes the content of the output directory if it is non-empty"
     );
+    ( Flag.create ~prefix:["lean"] ~arg:"typename" "extern_type",
+      Arg.String Pretty_print_lean.(fun ty -> opt_extern_types := ty :: !opt_extern_types),
+      "do not generate a definition for the type"
+    );
   ]
 
 (* TODO[javra]: Currently these are the same as the Coq rewrites, we might want to change them. *)