use vm_compute instead of Ltac to check instruction bounds

mit-plv · Oct 13, 2022 · 335e57a · 335e57a
1 parent 8293653
commit 335e57a
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 8 deletions.
diff --git a/compiler/src/compiler/CompilerInvariant.v b/compiler/src/compiler/CompilerInvariant.v
@@ -2,6 +2,7 @@ Require Import coqutil.Tactics.rewr.
 Require Import coqutil.Map.Interface coqutil.Map.Properties.
 Require Import coqutil.Word.Interface coqutil.Word.Properties.
 Require Import coqutil.Byte.
+Require Import riscv.Utility.bverify.
 Require Import bedrock2.Array.
 Require Import bedrock2.Map.SeparationLogic.
 Require Import compiler.SeparationLogic.
@@ -174,7 +175,7 @@ Section Pipeline1.
       required_stack_space <= word.unsigned (word.sub (stack_pastend ml) (stack_start ml)) / bytes_per_word /\
       word.unsigned ml.(code_start) + Z.of_nat (List.length (instrencode instrs)) <=
         word.unsigned ml.(code_pastend) /\
-      Forall (fun i => verify i iset \/ valid_InvalidInstruction i) instrs /\
+      bvalidInstructions iset instrs = true /\
       (imem ml.(code_start) ml.(code_pastend) instrs *
        mem_available ml.(heap_start) ml.(heap_pastend) *
        mem_available ml.(stack_start) ml.(stack_pastend))%sep initial.(getMem) /\
@@ -211,6 +212,7 @@ Section Pipeline1.
         destruct mlOk.
         destruct M0 as [v M0].
         * apply ptsto_bytes_to_program; try assumption.
+          eapply bvalidInstructions_valid. assumption.
         * unfold ptsto_bytes in Imem.
           eapply ptsto_bytes_range; try eassumption.
       + unfold imem in *.
@@ -220,6 +222,7 @@ Section Pipeline1.
         eapply iff1ToEq.
         destruct mlOk.
         eapply ptsto_bytes_to_program; try eassumption.
+        eapply bvalidInstructions_valid. assumption.
     - eapply @ll_inv_is_invariant; eassumption.
     - eapply ll_inv_implies_prefix_of_good. eassumption.
   Qed.

diff --git a/deps/riscv-coq b/deps/riscv-coq
diff --git a/end2end/src/end2end/End2EndLightbulb.v b/end2end/src/end2end/End2EndLightbulb.v
@@ -289,9 +289,6 @@ Proof.
 
   - vm_compute. intros. discriminate.
   - vm_compute. intros. discriminate.
-  - (* Here we prove that all > 700 instructions are valid, using Ltac.
-       If this becomes a bottleneck, we'll have to do this in Gallina in the compile function. *)
-    unfold lightbulb_insts. repeat (apply Forall_cons || apply Forall_nil).
-    all: left; vm_compute; try intuition discriminate.
   - vm_compute. reflexivity.
-Time Qed. (* takes more than 25s *)
+  - vm_compute. reflexivity.
+Time Qed. (* takes ca 2s *)
diff --git a/end2end/src/end2end/End2EndPipeline.v b/end2end/src/end2end/End2EndPipeline.v
@@ -15,6 +15,7 @@ Require riscv.Platform.Memory.
 Require Import riscv.Spec.PseudoInstructions.
 Require Import riscv.Proofs.EncodeBound.
 Require Import riscv.Proofs.DecodeEncode.
+Require Import riscv.Utility.bverify.
 Require Import riscv.Platform.Run.
 Require Import riscv.Utility.MkMachineWidth.
 Require Import riscv.Utility.Monads. Import MonadNotations.
@@ -307,7 +308,7 @@ Section Connect.
     required_stack_space <= word.unsigned (word.sub (stack_pastend ml) (stack_start ml)) / bytes_per_word ->
     word.unsigned (code_start ml) + Z.of_nat (Datatypes.length (instrencode instrs)) <=
       word.unsigned (code_pastend ml) ->
-    Forall (fun i : Instruction => verify i iset \/ valid_InvalidInstruction i) instrs ->
+    bvalidInstructions iset instrs = true ->
     valid_src_funs funimplsList = true ->
     (* Assumptions on the Kami level: *)
     kami_mem_contains_bytes (instrencode instrs) ml.(code_start) memInit ->