blob: 8342b04c60314ccd0e6d770a1b0be8cb0b6cef51 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
Require Import Sail.Values.
Require Import Sail.Prompt_monad.
Require Import Sail.Prompt.
Require Import Sail.State_monad.
Import ListNotations.
(* Lifting from prompt monad to state monad *)
(*val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e*)
Fixpoint liftState {Regval Regs A E} (ra : register_accessors Regs Regval) (m : monad Regval A E) : monadS Regs A E :=
match m with
| (Done a) => returnS a
| (Read_mem rk a sz k) => bindS (read_mem_bytesS rk a sz) (fun v => liftState ra (k v))
| (Read_memt rk a sz k) => bindS (read_memt_bytesS rk a sz) (fun v => liftState ra (k v))
| (Write_mem wk a sz v k) => bindS (write_mem_bytesS wk a sz v) (fun v => liftState ra (k v))
| (Write_memt wk a sz v t k) => bindS (write_memt_bytesS wk a sz v t) (fun v => liftState ra (k v))
| (Read_reg r k) => bindS (read_regvalS ra r) (fun v => liftState ra (k v))
| (Excl_res k) => bindS (excl_resultS tt) (fun v => liftState ra (k v))
| (Choose _ k) => bindS (choose_boolS tt) (fun v => liftState ra (k v))
| (Write_reg r v k) => seqS (write_regvalS ra r v) (liftState ra k)
| (Write_ea _ _ _ k) => liftState ra k
| (Footprint k) => liftState ra k
| (Barrier _ k) => liftState ra k
| (Print _ k) => liftState ra k (* TODO *)
| (Fail descr) => failS descr
| (Exception e) => throwS e
end.
Local Open Scope bool_scope.
(*val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)*)
Definition emitEventS {Regval Regs} `{forall (x y : Regval), Decidable (x = y)} (ra : register_accessors Regs Regval) (e : event Regval) (s : sequential_state Regs) : option (sequential_state Regs) :=
match e with
| E_read_mem _ addr sz v =>
option_bind (get_mem_bytes addr sz s) (fun '(v', _) =>
if generic_eq v' v then Some s else None)
| E_read_memt _ addr sz (v, tag) =>
option_bind (get_mem_bytes addr sz s) (fun '(v', tag') =>
if generic_eq v' v && generic_eq tag' tag then Some s else None)
| E_write_mem _ addr sz v success =>
if success then Some (put_mem_bytes addr sz v B0 s) else None
| E_write_memt _ addr sz v tag success =>
if success then Some (put_mem_bytes addr sz v tag s) else None
| E_read_reg r v =>
let (read_reg, _) := ra in
option_bind (read_reg r s.(ss_regstate)) (fun v' =>
if generic_eq v' v then Some s else None)
| E_write_reg r v =>
let (_, write_reg) := ra in
option_bind (write_reg r v s.(ss_regstate)) (fun rs' =>
Some {| ss_regstate := rs'; ss_memstate := s.(ss_memstate); ss_tagstate := s.(ss_tagstate) |})
| _ => Some s
end.
Local Close Scope bool_scope.
(*val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)*)
Fixpoint runTraceS {Regval Regs} `{forall (x y : Regval), Decidable (x = y)} (ra : register_accessors Regs Regval) (t : trace Regval) (s : sequential_state Regs) : option (sequential_state Regs) :=
match t with
| [] => Some s
| e :: t' => option_bind (emitEventS ra e s) (runTraceS ra t')
end.
|
