Skip to content

Instantly share code, notes, and snippets.

@jadephilipoom
Created May 11, 2021 18:11
Show Gist options
  • Save jadephilipoom/1e8e432d27a6e41162b0ae023ffa9994 to your computer and use it in GitHub Desktop.
Save jadephilipoom/1e8e432d27a6e41162b0ae023ffa9994 to your computer and use it in GitHub Desktop.
Proposed change to riscv-coq MMIO spec
diff --git a/src/riscv/Platform/FE310ExtSpec.v b/src/riscv/Platform/FE310ExtSpec.v
index 6b1ca2d..0fb3ccc 100644
--- a/src/riscv/Platform/FE310ExtSpec.v
+++ b/src/riscv/Platform/FE310ExtSpec.v
@@ -7,7 +7,7 @@ Require Import riscv.Platform.MinimalMMIO.
Local Open Scope Z_scope.
Section MMIO.
- Context {W: Words}.
+ Context {W: Words} {Mem : map.map word byte}.
(* Using the memory layout of FE310-G000 *)
Definition isOTP (addr: word): Prop := Ox"00020000" <= word.unsigned addr < Ox"00022000".
@@ -19,6 +19,7 @@ Section MMIO.
Instance FE310_mmio: MMIOSpec := {|
isMMIOAddr(addr: word) := isOTP addr \/ isPRCI addr \/ isGPIO0 addr \/ isUART0 addr \/ isSPI1 addr;
isMMIOAligned(n: nat)(addr: word) := n = 4%nat /\ (word.unsigned addr) mod 4 = 0;
+ MMIOReadOK := fun _ _ _ _ => True;
|}.
End MMIO.
diff --git a/src/riscv/Platform/MinimalMMIO.v b/src/riscv/Platform/MinimalMMIO.v
index caf47fd..36dd097 100644
--- a/src/riscv/Platform/MinimalMMIO.v
+++ b/src/riscv/Platform/MinimalMMIO.v
@@ -22,13 +22,15 @@ Require Import riscv.Platform.Sane.
Local Open Scope Z_scope.
Local Open Scope bool_scope.
-
-Class MMIOSpec{W: Words} := {
+Class MMIOSpec{W: Words} {Mem : map.map word byte} := {
(* should not say anything about alignment, just whether it's in the MMIO range *)
isMMIOAddr: word -> Prop;
(* alignment and load size checks *)
isMMIOAligned: nat -> word -> Prop;
+
+ (* hardware guarantees on MMIO read values *)
+ MMIOReadOK : nat -> list LogItem -> word -> word -> Prop;
}.
Section Riscv.
@@ -59,8 +61,13 @@ Section Riscv.
end.
Definition nonmem_load(n: nat)(ctxid: SourceType) a mach (post: _ -> _ -> Prop) :=
- isMMIOAddr a /\ isMMIOAligned n a /\
- forall v, post v (withLogItem (@mmioLoadEvent a n v) mach).
+ isMMIOAddr a /\ isMMIOAligned n a
+ (* there exists at least one valid MMIO read value (set is nonempty) *)
+ /\ (exists v : HList.tuple byte n, MMIOReadOK n (getLog mach) a (signedByteTupleToReg v))
+ (* ...and postcondition holds for all valid read values *)
+ /\ forall v,
+ MMIOReadOK n (getLog mach) a (signedByteTupleToReg v) ->
+ post v (withLogItem (@mmioLoadEvent a n v) mach).
Definition load(n: nat)(ctxid: SourceType) a mach post :=
(ctxid = Fetch -> isXAddr4 a mach.(getXAddrs)) /\
@@ -172,20 +179,27 @@ Section Riscv.
disjoint (of_list s.(getXAddrs)) isMMIOAddr ->
interpret_action a s postF postA ->
exists s', map.undef_on s'.(getMem) isMMIOAddr /\
- disjoint (of_list s'.(getXAddrs)) isMMIOAddr /\
- (postA s' \/ exists v', postF v' s').
+ disjoint (of_list s'.(getXAddrs)) isMMIOAddr /\
+ (postA s' \/ exists v', postF v' s').
Proof.
destruct s, a; cbn -[HList.tuple];
cbv [load store nonmem_load nonmem_store]; cbn -[HList.tuple];
repeat destruct_one_match;
intuition idtac;
- do 2 eexists;
+ repeat lazymatch goal with
+ | H : postF _ ?mach |- exists _ : RiscvMachine, _ =>
+ exists mach; cbn [RiscvMachine.getMem RiscvMachine.getXAddrs]
+ | H : postA ?mach |- exists _ : RiscvMachine, _ =>
+ exists mach; cbn [RiscvMachine.getMem RiscvMachine.getXAddrs]
+ | Hexists : (exists v, ?P), Hforall : (forall v, ?P -> _) |- _ =>
+ let v := fresh "v" in
+ destruct Hexists as [v Hexists];
+ specialize (Hforall v Hexists)
+ end;
ssplit; eauto; simpl;
change removeXAddr with (@List.removeb word word.eqb _);
rewrite ?ListSet.of_list_removeb;
intuition eauto 10 using preserve_undef_on, disjoint_diff_l.
- Unshelve.
- all: repeat constructor; exact (word.of_Z 0).
Qed.
Lemma interpret_action_total'{memOk: map.ok Mem} a s post :
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment