diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 17:36:30 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 17:36:30 +0100 |
| commit | ab15e9d17f999637ae16b2913b3c6f4f71f79e37 (patch) | |
| tree | 7412ea595a15bdb20997602b959c8f58a4a5e019 /riscV/CSE2depsproof.v | |
| parent | d14c78013f654ca586681136ba291f1487f1b586 (diff) | |
| download | compcert-kvx-ab15e9d17f999637ae16b2913b3c6f4f71f79e37.tar.gz compcert-kvx-ab15e9d17f999637ae16b2913b3c6f4f71f79e37.zip | |
fix for risc-V
Diffstat (limited to 'riscV/CSE2depsproof.v')
| -rw-r--r-- | riscV/CSE2depsproof.v | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v index ee500965..2ed12658 100644 --- a/riscV/CSE2depsproof.v +++ b/riscV/CSE2depsproof.v @@ -36,7 +36,6 @@ Section MEMORY_WRITE. Variable addrw addrr valw valr : val. Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. - Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. Section INDEXED_AWAY. Variable ofsw ofsr : ptrofs. @@ -49,8 +48,9 @@ Section MEMORY_WRITE. forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr - \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, - Mem.loadv chunkr m2 addrr = Some valr. + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. intros. @@ -62,7 +62,6 @@ Section MEMORY_WRITE. simpl in *. inv ADDRR. inv ADDRW. - rewrite <- READ. destruct base; try discriminate. eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). exact STORE. @@ -80,7 +79,7 @@ Section MEMORY_WRITE. Theorem load_store_away : can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> - Mem.loadv chunkr m2 addrr = Some valr. + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. Proof. intro SWAP. unfold can_swap_accesses_ofs in SWAP. @@ -102,16 +101,15 @@ Section SOUNDNESS. Lemma may_overlap_sound: forall m m' : mem, - forall chunk addr args chunk' addr' args' v a a' vl rs, + forall chunk addr args chunk' addr' args' v a a' rs, (eval_addressing genv sp addr (rs ## args)) = Some a -> (eval_addressing genv sp addr' (rs ## args')) = Some a' -> (may_overlap chunk addr args chunk' addr' args') = false -> (Mem.storev chunk m a v) = Some m' -> - (Mem.loadv chunk' m a') = Some vl -> - (Mem.loadv chunk' m' a') = Some vl. + (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a'). Proof. intros until rs. - intros ADDR ADDR' OVERLAP STORE LOAD. + intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. { (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. |