m

compiler/src/compiler/LowerPipeline.v

@@ -1,3 +1,4 @@
+
 Require Import bedrock2.LeakageSemantics.
 Require Import Coq.Logic.FunctionalExtensionality.
 Require Import coqutil.Map.Interface.
@@ -134,8 +135,6 @@ Section LowerPipeline.
   Context {word: word.word width} {word_ok: word.ok word}.
   Context {locals: map.map Z word} {locals_ok: map.ok locals}.
   Context {mem: map.map word byte} {mem_ok: map.ok mem}.
-  (*Context (leak_ext_call: pos_map -> Z -> Z -> stmt Z -> list word -> list LeakageEvent).*)
-
 
   Add Ring wring : (word.ring_theory (word := word))
       (preprocess [autorewrite with rew_word_morphism],
@@ -392,11 +391,11 @@ Section LowerPipeline.
       compiles_FlatToRiscv_correctly compile_ext_call leak_ext_call compile_ext_call
                                      (FlatImp.SInteract resvars extcall argvars).
 
-  Definition riscv_call(p: list Instruction * pos_map * Z)(s: word(*p_funcs*) * word (*stack_pastend*) * word (*ret_addr*))
-             (f_name: string)(kL: list LeakageEvent)(t: Semantics.trace)(mH: mem)(argvals: list word)(mc: MetricLog)
-             (post: list LeakageEvent -> Semantics.trace -> mem -> list word -> MetricLog -> Prop): Prop :=
+  Definition riscv_call(p: list Instruction * pos_map * Z)
+    (p_funcs stack_pastend ret_addr : word)(f_name: string)(kL: list LeakageEvent)
+    (t: Semantics.trace)(mH: mem)(argvals: list word)(mc: MetricLog)
+    (post: list LeakageEvent -> Semantics.trace -> mem -> list word -> MetricLog -> Prop): Prop :=
     let '(instrs, finfo, req_stack_size) := p in
-    let '(p_funcs, stack_pastend, ret_addr) := s in
     exists f_rel_pos,
       map.get finfo f_name = Some f_rel_pos /\
       forall stack_start Rdata Rexec (initial: MetricRiscvMachine),
@@ -509,7 +508,7 @@ Section LowerPipeline.
                 exists retvals, map.getmany_of_list l' retnames = Some retvals /\
                              post kH' t' m' retvals mc')) ->
       forall mcL,
-        riscv_call p2 (p_funcs, stack_pastend, ret_addr) fname kL t m argvals mcL
+        riscv_call p2 p_funcs stack_pastend ret_addr fname kL t m argvals mcL
           (fun kL' t m a mcL' =>
              exists mcH' kH' kH'',
                metricsLeq (mcL' - mcL) (mcH' - mcH) /\
@@ -629,7 +628,7 @@ Section LowerPipeline.
       + eassumption.
       + assumption.
       + unfold machine_ok in *. fwd. assumption.
-      + Search (getTrace initial). rewrite H1. reflexivity.
+      + rewrite H1. reflexivity.
       + simpl_g_get. reflexivity.
       + unfold machine_ok in *. subst. fwd.
         unfold goodMachine; simpl_g_get. ssplit.

compiler/src/compiler/Pipeline.v

@@ -246,7 +246,7 @@ Section WithWordAndMem.
             Z;                      (* <- required stack space in XLEN-bit words   *)
         (* bounds in instructions are checked by `ptsto_instr` *)
         Valid '(insts, finfo, req_stack_size) := True;
-        Call := (fun _ p => riscv_call p (p_funcs, stack_pastend, ret_addr)); |}.
+        Call := (fun _ p => riscv_call p p_funcs stack_pastend ret_addr); |}.
 
     Lemma flatten_functions_NoDup: forall funs funs',
         (forall f argnames retnames body,
@@ -588,15 +588,15 @@ Section WithWordAndMem.
     Qed.
 
     Lemma riscv_call_weaken :
-      forall p s funcname
+      forall p p_funcs stack_pastend ret_addr funcname
         k t m argvals mc post1,
-        riscv_call p s funcname k t m argvals mc post1 ->
+        riscv_call p p_funcs stack_pastend ret_addr funcname k t m argvals mc post1 ->
         forall post2,
           (forall k' t' m' retvals mc',
               post1 k' t' m' retvals mc' -> post2 k' t' m' retvals mc') ->
-          riscv_call p s funcname k t m argvals mc post2.
+          riscv_call p p_funcs stack_pastend ret_addr funcname k t m argvals mc post2.
     Proof.
-      intros. cbv [riscv_call] in *. destruct p. destruct p. destruct s as [ [? ?] ?].
+      intros. cbv [riscv_call] in *. destruct p. destruct p.
       destruct H as [f_rel_pos H]. exists f_rel_pos. intuition eauto.
       cbv [runsTo]. eapply runsToNonDet.runsTo_weaken. 1: eapply H2.
       all: try eassumption. simpl. intros. fwd. do 3 eexists.