diff options
Diffstat (limited to 'lib/coq/Prompt_monad.v')
| -rw-r--r-- | lib/coq/Prompt_monad.v | 367 |
1 files changed, 367 insertions, 0 deletions
diff --git a/lib/coq/Prompt_monad.v b/lib/coq/Prompt_monad.v new file mode 100644 index 00000000..5f54ad0d --- /dev/null +++ b/lib/coq/Prompt_monad.v @@ -0,0 +1,367 @@ +Require Import String. +(*Require Import Sail_impl_base*) +Require Import Sail.Instr_kinds. +Require Import Sail.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 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 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 *) + | Barrier : barrier_kind -> monad regval a e -> monad regval a e + (* Request to read register, will track dependency when mode.track_values *) + | 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 + (* 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 + (* Exception of type e *) + | Exception : e -> monad regval a e. + +Arguments Done [_ _ _]. +Arguments Read_mem [_ _ _]. +Arguments Read_memt [_ _ _]. +Arguments Write_ea [_ _ _]. +Arguments Excl_res [_ _ _]. +Arguments Write_mem [_ _ _]. +Arguments Write_memt [_ _ _]. +Arguments Footprint [_ _ _]. +Arguments Barrier [_ _ _]. +Arguments Read_reg [_ _ _]. +Arguments Write_reg [_ _ _]. +Arguments Choose [_ _ _]. +Arguments Print [_ _ _]. +Arguments Fail [_ _ _]. +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_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). +(*val (>>) : forall rv b e. monad rv unit e -> monad rv b e -> monad rv b e*) +Definition bind0 {rv A E} (m : monad rv unit E) (n : monad rv A E) := + m >>= fun (_ : unit) => n. +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 := choose_bool "undefined_bool". + +Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. + +(*val assert_exp : forall rv e. bool -> string -> monad rv unit e*) +Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E := + if exp then Done tt else Fail msg. + +Definition assert_exp' {rv E} (exp :bool) msg : monad rv (exp = true) E := + if exp return monad rv (exp = true) E then Done eq_refl else Fail msg. +Definition bindH {rv A P E} (m : monad rv P E) (n : monad rv A E) := + m >>= fun (H : P) => n. +Notation "m >>> n" := (bindH m n) (at level 50, left associativity). + +(*val throw : forall rv a e. e -> monad rv a e*) +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_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 + the return value. The exception type is "either r e", where "inr e" + represents a proper exception and "inl r" an early return : value "r". *) +Definition monadR rv a r e := monad rv a (sum r e). + +(*val early_return : forall rv a r e. r -> monadR rv a r e*) +Definition early_return {rv A R E} (r : R) : monadR rv A R E := throw (inl r). + +(*val catch_early_return : forall rv a e. monadR rv a a e -> monad rv a e*) +Definition catch_early_return {rv A E} (m : monadR rv A A E) := + try_catch m + (fun r => match r with + | inl a => returnm a + | inr e => throw e + end). + +(* Lift to monad with early return by wrapping exceptions *) +(*val liftR : forall rv a r e. monad rv a e -> monadR rv a r e*) +Definition liftR {rv A R E} (m : monad rv A E) : monadR rv A R E := + try_catch m (fun e => throw (inr e)). + +(* Catch exceptions in the presence : early returns *) +(*val try_catchR : forall rv a r e1 e2. monadR rv a r e1 -> (e1 -> monadR rv a r e2) -> monadR rv a r e2*) +Definition try_catchR {rv A R E1 E2} (m : monadR rv A R E1) (h : E1 -> monadR rv A R E2) := + try_catch m + (fun r => match r with + | inl r => throw (inl r) + | inr e => h e + end). + +(*val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e*) +Definition maybe_fail {rv A E} msg (x : option A) : monad rv A E := +match x with + | Some a => returnm a + | 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 (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 (addrsz : Z) (addr : mword A) sz : monad rv (mword B) E := + bind + (read_mem_bytes rk addr sz) + (fun bytes => + maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))). + +(*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} wk (addrsz : Z) (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 -> integer -> 'a -> integer -> 'b -> monad 'rv bool 'e*) +Definition write_mem {rv a b E} wk (addrsz : Z) (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 => 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 +let read_reg_range reg i j = + read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j)) + +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) + +let read_reg_field reg regfield = + read_reg_aux (external_reg_field_whole reg regfield) + +let read_reg_bitfield reg regfield = + read_reg_aux (external_reg_field_whole reg regfield) >>= fun v -> + return (extract_only_element v)*) + +Definition reg_deref {s rv a e} := @read_reg s rv a e. + +(*Parameter write_reg : forall {s rv a e}, register_ref s rv a -> a -> monad rv unit e.*) +Definition 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). + +(* TODO +let write_reg reg v = + write_reg_aux (external_reg_whole reg) v +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] +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 +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)) +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] +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. |