summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_prompt_monad.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/coq/Sail2_prompt_monad.v')
-rw-r--r--lib/coq/Sail2_prompt_monad.v298
1 files changed, 208 insertions, 90 deletions
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v
index 2715b5e7..39567520 100644
--- a/lib/coq/Sail2_prompt_monad.v
+++ b/lib/coq/Sail2_prompt_monad.v
@@ -2,27 +2,28 @@ Require Import String.
(*Require Import Sail_impl_base*)
Require Import Sail2_instr_kinds.
Require Import Sail2_values.
-
-
+Require bbv.Word.
+Import ListNotations.
Definition register_name := string.
Definition address := list bitU.
Inductive monad regval a e :=
| Done : a -> monad regval a e
- (* Read a number : bytes from memory, returned in little endian order *)
- | Read_mem : read_kind -> address -> nat -> (list memory_byte -> monad regval a e) -> monad regval a e
- (* Read the tag : a memory address *)
- | Read_tag : address -> (bitU -> monad regval a e) -> monad regval a e
- (* Tell the system a write is imminent, at address lifted, : size nat *)
- | Write_ea : write_kind -> address -> nat -> monad regval a e -> monad regval a e
+ (* Read a number of bytes from memory, returned in little endian order,
+ with or without a tag. The first nat specifies the address, the second
+ the number of bytes. *)
+ | Read_mem : read_kind -> nat -> nat -> (list memory_byte -> monad regval a e) -> monad regval a e
+ | Read_memt : read_kind -> nat -> nat -> ((list memory_byte * bitU) -> monad regval a e) -> monad regval a e
+ (* Tell the system a write is imminent, at the given address and with the
+ given size. *)
+ | Write_ea : write_kind -> nat -> nat -> monad regval a e -> monad regval a e
(* Request the result : store-exclusive *)
| Excl_res : (bool -> monad regval a e) -> monad regval a e
- (* Request to write memory at last signalled address. Memory value should be 8
- times the size given in ea signal, given in little endian order *)
- | Write_memv : list memory_byte -> (bool -> monad regval a e) -> monad regval a e
- (* Request to write the tag at last signalled address. *)
- | Write_tag : address -> bitU -> (bool -> monad regval a e) -> monad regval a e
+ (* Request to write a memory value of the given size at the given address,
+ with or without a tag. *)
+ | Write_mem : write_kind -> nat -> nat -> list memory_byte -> (bool -> monad regval a e) -> monad regval a e
+ | Write_memt : write_kind -> nat -> nat -> list memory_byte -> bitU -> (bool -> monad regval a e) -> monad regval a e
(* Tell the system to dynamically recalculate dependency footprint *)
| Footprint : monad regval a e -> monad regval a e
(* Request a memory barrier *)
@@ -31,50 +32,70 @@ Inductive monad regval a e :=
| Read_reg : register_name -> (regval -> monad regval a e) -> monad regval a e
(* Request to write register *)
| Write_reg : register_name -> regval -> monad regval a e -> monad regval a e
- | Undefined : (bool -> monad regval a e) -> monad regval a e
- (*Result : a failed assert with possible error message to report*)
+ (* Request to choose a Boolean, e.g. to resolve an undefined bit. The string
+ argument may be used to provide information to the system about what the
+ Boolean is going to be used for. *)
+ | Choose : string -> (bool -> monad regval a e) -> monad regval a e
+ (* Print debugging or tracing information *)
+ | Print : string -> monad regval a e -> monad regval a e
+ (*Result of a failed assert with possible error message to report*)
| Fail : string -> monad regval a e
- | Error : string -> monad regval a e
- (* Exception : type e *)
+ (* Exception of type e *)
| Exception : e -> monad regval a e.
- (* TODO: Reading/writing tags *)
Arguments Done [_ _ _].
Arguments Read_mem [_ _ _].
-Arguments Read_tag [_ _ _].
+Arguments Read_memt [_ _ _].
Arguments Write_ea [_ _ _].
Arguments Excl_res [_ _ _].
-Arguments Write_memv [_ _ _].
-Arguments Write_tag [_ _ _].
+Arguments Write_mem [_ _ _].
+Arguments Write_memt [_ _ _].
Arguments Footprint [_ _ _].
Arguments Barrier [_ _ _].
Arguments Read_reg [_ _ _].
Arguments Write_reg [_ _ _].
-Arguments Undefined [_ _ _].
+Arguments Choose [_ _ _].
+Arguments Print [_ _ _].
Arguments Fail [_ _ _].
-Arguments Error [_ _ _].
Arguments Exception [_ _ _].
+Inductive event {regval} :=
+ | E_read_mem : read_kind -> nat -> nat -> list memory_byte -> event
+ | E_read_memt : read_kind -> nat -> nat -> (list memory_byte * bitU) -> event
+ | E_write_mem : write_kind -> nat -> nat -> list memory_byte -> bool -> event
+ | E_write_memt : write_kind -> nat -> nat -> list memory_byte -> bitU -> bool -> event
+ | E_write_ea : write_kind -> nat -> nat -> event
+ | E_excl_res : bool -> event
+ | E_barrier : barrier_kind -> event
+ | E_footprint : event
+ | E_read_reg : register_name -> regval -> event
+ | E_write_reg : register_name -> regval -> event
+ | E_choose : string -> bool -> event
+ | E_print : string -> event.
+Arguments event : clear implicits.
+
+Definition trace regval := list (event regval).
+
(*val return : forall rv a e. a -> monad rv a e*)
Definition returnm {rv A E} (a : A) : monad rv A E := Done a.
(*val bind : forall rv a b e. monad rv a e -> (a -> monad rv b e) -> monad rv b e*)
Fixpoint bind {rv A B E} (m : monad rv A E) (f : A -> monad rv B E) := match m with
| Done a => f a
- | Read_mem rk a sz k => Read_mem rk a sz (fun v => bind (k v) f)
- | Read_tag a k => Read_tag a (fun v => bind (k v) f)
- | Write_memv descr k => Write_memv descr (fun v => bind (k v) f)
- | Write_tag a t k => Write_tag a t (fun v => bind (k v) f)
- | Read_reg descr k => Read_reg descr (fun v => bind (k v) f)
- | Excl_res k => Excl_res (fun v => bind (k v) f)
- | Undefined k => Undefined (fun v => bind (k v) f)
- | Write_ea wk a sz k => Write_ea wk a sz (bind k f)
- | Footprint k => Footprint (bind k f)
- | Barrier bk k => Barrier bk (bind k f)
- | Write_reg r v k => Write_reg r v (bind k f)
- | Fail descr => Fail descr
- | Error descr => Error descr
- | Exception e => Exception e
+ | Read_mem rk a sz k => Read_mem rk a sz (fun v => bind (k v) f)
+ | Read_memt rk a sz k => Read_memt rk a sz (fun v => bind (k v) f)
+ | Write_mem wk a sz v k => Write_mem wk a sz v (fun v => bind (k v) f)
+ | Write_memt wk a sz v t k => Write_memt wk a sz v t (fun v => bind (k v) f)
+ | Read_reg descr k => Read_reg descr (fun v => bind (k v) f)
+ | Excl_res k => Excl_res (fun v => bind (k v) f)
+ | Choose descr k => Choose descr (fun v => bind (k v) f)
+ | Write_ea wk a sz k => Write_ea wk a sz (bind k f)
+ | Footprint k => Footprint (bind k f)
+ | Barrier bk k => Barrier bk (bind k f)
+ | Write_reg r v k => Write_reg r v (bind k f)
+ | Print msg k => Print msg (bind k f)
+ | Fail descr => Fail descr
+ | Exception e => Exception e
end.
Notation "m >>= f" := (bind m f) (at level 50, left associativity).
@@ -86,8 +107,11 @@ Notation "m >> n" := (bind0 m n) (at level 50, left associativity).
(*val exit : forall rv a e. unit -> monad rv a e*)
Definition exit {rv A E} (_ : unit) : monad rv A E := Fail "exit".
+(*val choose_bool : forall 'rv 'e. string -> monad 'rv bool 'e*)
+Definition choose_bool {rv E} descr : monad rv bool E := Choose descr returnm.
+
(*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*)
-Definition undefined_bool {rv e} (_:unit) : monad rv bool e := Undefined returnm.
+Definition undefined_bool {rv e} (_:unit) : monad rv bool e := choose_bool "undefined_bool".
(*val assert_exp : forall rv e. bool -> string -> monad rv unit e*)
Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E :=
@@ -104,21 +128,21 @@ Definition throw {rv A E} e : monad rv A E := Exception e.
(*val try_catch : forall rv a e1 e2. monad rv a e1 -> (e1 -> monad rv a e2) -> monad rv a e2*)
Fixpoint try_catch {rv A E1 E2} (m : monad rv A E1) (h : E1 -> monad rv A E2) := match m with
- | Done a => Done a
- | Read_mem rk a sz k => Read_mem rk a sz (fun v => try_catch (k v) h)
- | Read_tag a k => Read_tag a (fun v => try_catch (k v) h)
- | Write_memv descr k => Write_memv descr (fun v => try_catch (k v) h)
- | Write_tag a t k => Write_tag a t (fun v => try_catch (k v) h)
- | Read_reg descr k => Read_reg descr (fun v => try_catch (k v) h)
- | Excl_res k => Excl_res (fun v => try_catch (k v) h)
- | Undefined k => Undefined (fun v => try_catch (k v) h)
- | Write_ea wk a sz k => Write_ea wk a sz (try_catch k h)
- | Footprint k => Footprint (try_catch k h)
- | Barrier bk k => Barrier bk (try_catch k h)
- | Write_reg r v k => Write_reg r v (try_catch k h)
- | Fail descr => Fail descr
- | Error descr => Error descr
- | Exception e => h e
+ | Done a => Done a
+ | Read_mem rk a sz k => Read_mem rk a sz (fun v => try_catch (k v) h)
+ | Read_memt rk a sz k => Read_memt rk a sz (fun v => try_catch (k v) h)
+ | Write_mem wk a sz v k => Write_mem wk a sz v (fun v => try_catch (k v) h)
+ | Write_memt wk a sz v t k => Write_memt wk a sz v t (fun v => try_catch (k v) h)
+ | Read_reg descr k => Read_reg descr (fun v => try_catch (k v) h)
+ | Excl_res k => Excl_res (fun v => try_catch (k v) h)
+ | Choose descr k => Choose descr (fun v => try_catch (k v) h)
+ | Write_ea wk a sz k => Write_ea wk a sz (try_catch k h)
+ | Footprint k => Footprint (try_catch k h)
+ | Barrier bk k => Barrier bk (try_catch k h)
+ | Write_reg r v k => Write_reg r v (try_catch k h)
+ | Print msg k => Print msg (try_catch k h)
+ | Fail descr => Fail descr
+ | Exception e => h e
end.
(* For early return, we abuse exceptions by throwing and catching
@@ -158,9 +182,23 @@ match x with
| None => Fail msg
end.
+(*val read_memt_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e*)
+Definition read_memt_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memory_byte * bitU) E :=
+ Read_memt rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm.
+
+(*val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e*)
+Definition read_memt {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B * bitU) E :=
+ bind
+ (read_memt_bytes rk addr sz)
+ (fun '(bytes, tag) =>
+ match of_bits (bits_of_mem_bytes bytes) with
+ | Some v => returnm (v, tag)
+ | None => Fail "bits_of_mem_bytes"
+ end).
+
(*val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e*)
Definition read_mem_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memory_byte) E :=
- Read_mem rk (bits_of addr) (Z.to_nat sz) returnm.
+ Read_mem rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm.
(*val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e*)
Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B) E :=
@@ -169,50 +207,56 @@ Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : mo
(fun bytes =>
maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))).
-(*val read_tag : forall rv a e. Bitvector a => a -> monad rv bitU e*)
-Definition read_tag {rv a e} `{Bitvector a} (addr : a) : monad rv bitU e :=
- Read_tag (bits_of addr) returnm.
-
(*val excl_result : forall rv e. unit -> monad rv bool e*)
Definition excl_result {rv e} (_:unit) : monad rv bool e :=
let k successful := (returnm successful) in
Excl_res k.
-Definition write_mem_ea {rv a E} `{Bitvector a} wk (addr: a) sz : monad rv unit E :=
- Write_ea wk (bits_of addr) (Z.to_nat sz) (Done tt).
-
-Definition write_mem_val {rv a e} `{Bitvector a} (v : a) : monad rv bool e := match mem_bytes_of_bits v with
- | Some v => Write_memv v returnm
- | None => Fail "write_mem_val"
-end.
-
-(*val write_tag : forall rv a e. Bitvector 'a => 'a -> bitU -> monad rv bool e*)
-Definition write_tag {rv a e} (addr : mword a) (b : bitU) : monad rv bool e := Write_tag (bits_of addr) b returnm.
+Definition write_mem_ea {rv a E} wk (addr: mword a) sz : monad rv unit E :=
+ Write_ea wk (Word.wordToNat (get_word addr)) (Z.to_nat sz) (Done tt).
+
+(*val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+ write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e*)
+Definition write_mem {rv a b E} wk (addr : mword a) sz (v : mword b) : monad rv bool E :=
+ match (mem_bytes_of_bits v, Word.wordToNat (get_word addr)) with
+ | (Some v, addr) =>
+ Write_mem wk addr (Z.to_nat sz) v returnm
+ | _ => Fail "write_mem"
+ end.
+
+(*val write_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+ write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e*)
+Definition write_memt {rv a b E} wk (addr : mword a) sz (v : mword b) tag : monad rv bool E :=
+ match (mem_bytes_of_bits v, Word.wordToNat (get_word addr)) with
+ | (Some v, addr) =>
+ Write_memt wk addr (Z.to_nat sz) v tag returnm
+ | _ => Fail "write_mem"
+ end.
Definition read_reg {s rv a e} (reg : register_ref s rv a) : monad rv a e :=
let k v :=
match reg.(of_regval) v with
| Some v => Done v
- | None => Error "read_reg: unrecognised value"
+ | None => Fail "read_reg: unrecognised value"
end
in
Read_reg reg.(name) k.
(* TODO
-val read_reg_range : forall s r rv a e. Bitvector a => register_ref s rv r -> integer -> integer -> monad rv a e
-Definition read_reg_range reg i j :=
- read_reg_aux of_bits (external_reg_slice reg (natFromInteger i,natFromInteger j))
+val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e
+let read_reg_range reg i j =
+ read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j))
-Definition read_reg_bit reg i :=
- read_reg_aux (fun v -> v) (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
- returnm (extract_only_element v)
+let read_reg_bit reg i =
+ read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v ->
+ return (extract_only_element v)
-Definition read_reg_field reg regfield :=
+let read_reg_field reg regfield =
read_reg_aux (external_reg_field_whole reg regfield)
-Definition read_reg_bitfield reg regfield :=
+let read_reg_bitfield reg regfield =
read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
- returnm (extract_only_element v)*)
+ return (extract_only_element v)*)
Definition reg_deref {s rv a e} := @read_reg s rv a e.
@@ -221,27 +265,101 @@ Definition write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv u
Write_reg reg.(name) (reg.(regval_of) v) (Done tt).
(* TODO
-Definition write_reg reg v :=
+let write_reg reg v =
write_reg_aux (external_reg_whole reg) v
-Definition write_reg_range reg i j v :=
- write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
-Definition write_reg_pos reg i v :=
- let iN := natFromInteger i in
+let write_reg_range reg i j v =
+ write_reg_aux (external_reg_slice reg (nat_of_int i,nat_of_int j)) v
+let write_reg_pos reg i v =
+ let iN = nat_of_int i in
write_reg_aux (external_reg_slice reg (iN,iN)) [v]
-Definition write_reg_bit := write_reg_pos
-Definition write_reg_field reg regfield v :=
+let write_reg_bit = write_reg_pos
+let write_reg_field reg regfield v =
write_reg_aux (external_reg_field_whole reg regfield.field_name) v
-Definition write_reg_field_bit reg regfield bit :=
+let write_reg_field_bit reg regfield bit =
write_reg_aux (external_reg_field_whole reg regfield.field_name)
(Vector [bit] 0 (is_inc_of_reg reg))
-Definition write_reg_field_range reg regfield i j v :=
- write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
-Definition write_reg_field_pos reg regfield i v :=
+let write_reg_field_range reg regfield i j v =
+ write_reg_aux (external_reg_field_slice reg regfield.field_name (nat_of_int i,nat_of_int j)) v
+let write_reg_field_pos reg regfield i v =
write_reg_field_range reg regfield i i [v]
-Definition write_reg_field_bit := write_reg_field_pos*)
+let write_reg_field_bit = write_reg_field_pos*)
(*val barrier : forall rv e. barrier_kind -> monad rv unit e*)
Definition barrier {rv e} bk : monad rv unit e := Barrier bk (Done tt).
(*val footprint : forall rv e. unit -> monad rv unit e*)
Definition footprint {rv e} (_ : unit) : monad rv unit e := Footprint (Done tt).
+
+(* Event traces *)
+
+Local Open Scope bool_scope.
+
+(*val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e)*)
+Definition emitEvent {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (m : monad Regval A E) (e : event Regval) : option (monad Regval A E) :=
+ match (e, m) with
+ | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) =>
+ if read_kind_beq rk' rk && Nat.eqb a' a && Nat.eqb sz' sz then Some (k v) else None
+ | (E_read_memt rk a sz vt, Read_memt rk' a' sz' k) =>
+ if read_kind_beq rk' rk && Nat.eqb a' a && Nat.eqb sz' sz then Some (k vt) else None
+ | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) =>
+ if write_kind_beq wk' wk && Nat.eqb a' a && Nat.eqb sz' sz && generic_eq v' v then Some (k r) else None
+ | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) =>
+ if write_kind_beq wk' wk && Nat.eqb a' a && Nat.eqb sz' sz && generic_eq v' v && generic_eq tag' tag then Some (k r) else None
+ | (E_read_reg r v, Read_reg r' k) =>
+ if generic_eq r' r then Some (k v) else None
+ | (E_write_reg r v, Write_reg r' v' k) =>
+ if generic_eq r' r && generic_eq v' v then Some k else None
+ | (E_write_ea wk a sz, Write_ea wk' a' sz' k) =>
+ if write_kind_beq wk' wk && Nat.eqb a' a && Nat.eqb sz' sz then Some k else None
+ | (E_barrier bk, Barrier bk' k) =>
+ if barrier_kind_beq bk' bk then Some k else None
+ | (E_print m, Print m' k) =>
+ if generic_eq m' m then Some k else None
+ | (E_excl_res v, Excl_res k) => Some (k v)
+ | (E_choose descr v, Choose descr' k) => if generic_eq descr' descr then Some (k v) else None
+ | (E_footprint, Footprint k) => Some k
+ | _ => None
+end.
+
+Definition option_bind {A B : Type} (a : option A) (f : A -> option B) : option B :=
+match a with
+| Some x => f x
+| None => None
+end.
+
+(*val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)*)
+Fixpoint runTrace {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (t : trace Regval) (m : monad Regval A E) : option (monad Regval A E) :=
+match t with
+ | [] => Some m
+ | e :: t' => option_bind (emitEvent m e) (runTrace t')
+end.
+
+(*val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool*)
+Definition final {Regval A E} (m : monad Regval A E) : bool :=
+match m with
+ | Done _ => true
+ | Fail _ => true
+ | Exception _ => true
+ | _ => false
+end.
+
+(*val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
+Definition hasTrace {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (t : trace Regval) (m : monad Regval A E) : bool :=
+match runTrace t m with
+ | Some m => final m
+ | None => false
+end.
+
+(*val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
+Definition hasException {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (t : trace Regval) (m : monad Regval A E) :=
+match runTrace t m with
+ | Some (Exception _) => true
+ | _ => false
+end.
+
+(*val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
+Definition hasFailure {Regval A E} `{forall (x y : Regval), Decidable (x = y)} (t : trace Regval) (m : monad Regval A E) :=
+match runTrace t m with
+ | Some (Fail _) => true
+ | _ => false
+end.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:55:50 +0000