m

mit-plv · Jan 10, 2025 · d9cb57d · d9cb57d
1 parent dedd1ec
commit d9cb57d
Showing 1 changed file with 32 additions and 36 deletions.
diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v
@@ -153,10 +153,8 @@ Section WithWordAndMem.
     Context {PR: MetricPrimitives PRParams}.
     Context {iset: InstructionSet}.
     Context {BWM: bitwidth_iset width iset}.
-    Context (compile_ext_call : string_keyed_map Z -> Z -> Z -> FlatImp.stmt Z ->
-                                list Instruction).
-    Context (leak_ext_call : word -> string_keyed_map Z -> Z -> Z -> FlatImp.stmt Z ->
-                             list word -> list LeakageEvent).
+    Context (compile_ext_call : string_keyed_map Z -> Z -> Z -> FlatImp.stmt Z -> list Instruction).
+    Context (leak_ext_call : word -> string_keyed_map Z -> Z -> Z -> FlatImp.stmt Z -> list word -> list LeakageEvent).
     Context (compile_ext_call_correct: forall resvars extcall argvars,
                 compiles_FlatToRiscv_correctly compile_ext_call leak_ext_call compile_ext_call
                                                (FlatImp.SInteract resvars extcall argvars)).
@@ -190,20 +188,20 @@ Section WithWordAndMem.
     Definition ParamsNoDup{Var: Type}: (list Var * list Var * FlatImp.stmt Var) -> Prop :=
       fun '(argnames, retnames, body) => NoDup argnames /\ NoDup retnames.
 
-    Definition SrcLang : Lang :=
-      {|
-        Program := Semantics.env (*why do we use 'string_keyed_map' everywhere except here?*);
-        Valid := map.forall_values ExprImp.valid_fun;
-        Call := locals_based_call_spec (fun pick_sp e => @MetricLeakageSemantics.exec _ _ _ _ _ _ e pick_sp) false; |}.
+    Definition SrcLang : Lang := {|
+      Program := Semantics.env;
+      Valid := map.forall_values ExprImp.valid_fun;
+      Call := locals_based_call_spec (fun pick_sp e => @MetricLeakageSemantics.exec _ _ _ _ _ _ e pick_sp) false;
+    |}.
 
     (* |                 *)
     (* | FlattenExpr     *)
     (* V                 *)
-    Definition FlatWithStrVars: Lang :=
-      {|
-        Program := string_keyed_map (list string * list string * FlatImp.stmt string);
-        Valid := map.forall_values ParamsNoDup;
-        Call := locals_based_call_spec (fun pick_sp e => @FlatImp.exec _ _ _ _ _ _ _ _ PreSpill isRegStr e pick_sp) false; |}.
+    Definition FlatWithStrVars: Lang := {|
+      Program := string_keyed_map (list string * list string * FlatImp.stmt string);
+      Valid := map.forall_values ParamsNoDup;
+      Call := locals_based_call_spec (fun pick_sp e => @FlatImp.exec _ _ _ _ _ _ _ _ PreSpill isRegStr e pick_sp) false;
+    |}.
 
     (* |                 *)
     (* | UseImmediate    *)
@@ -218,33 +216,33 @@ Section WithWordAndMem.
     (* |                 *)
     (* | RegAlloc        *)
     (* V                 *)
-    Definition FlatWithZVars: Lang :=
-      {|
-        Program := string_keyed_map (list Z * list Z * FlatImp.stmt Z);
-        Valid := map.forall_values ParamsNoDup;
-        Call := locals_based_call_spec (fun pick_sp e => @FlatImp.exec _ _ _ _ _ _ _ _ PreSpill isRegZ e pick_sp) false; |}.
+    Definition FlatWithZVars: Lang := {|
+      Program := string_keyed_map (list Z * list Z * FlatImp.stmt Z);
+      Valid := map.forall_values ParamsNoDup;
+      Call := locals_based_call_spec (fun pick_sp e => @FlatImp.exec _ _ _ _ _ _ _ _ PreSpill isRegZ e pick_sp) false;
+    |}.
 
     (* |                 *)
     (* | Spilling        *)
     (* V                 *)
-    Definition FlatWithRegs: Lang :=
-      {|
-        Program := string_keyed_map (list Z * list Z * FlatImp.stmt Z);
-        Valid := map.forall_values FlatToRiscvDef.valid_FlatImp_fun;
-        Call := locals_based_call_spec (fun e pick_sp => @FlatImp.exec _ _ _ _ _ _ _ _ PostSpill isRegZ pick_sp e) true; |}.
+    Definition FlatWithRegs: Lang := {|
+      Program := string_keyed_map (list Z * list Z * FlatImp.stmt Z);
+      Valid := map.forall_values FlatToRiscvDef.valid_FlatImp_fun;
+      Call := locals_based_call_spec (fun e pick_sp => @FlatImp.exec _ _ _ _ _ _ _ _ PostSpill isRegZ pick_sp e) true;
+    |}.
 
     (* |                 *)
     (* | FlatToRiscv     *)
     (* V                 *)
-    Definition RiscvLang (p_funcs stack_pastend ret_addr : word) : Lang :=
-      {|
-        Program :=
-          list Instruction *      (* <- code of all functions concatenated       *)
-            string_keyed_map Z *    (* <- position (offset) for each function      *)
-            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); |}.
+    Definition RiscvLang (p_funcs stack_pastend ret_addr : word) : Lang := {|
+      Program :=
+        list Instruction *      (* <- code of all functions concatenated       *)
+        string_keyed_map Z *    (* <- position (offset) for each function      *)
+        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);
+    |}.
 
     Lemma flatten_functions_NoDup: forall funs funs',
         (forall f argnames retnames body,
@@ -577,8 +575,7 @@ Section WithWordAndMem.
       intros.
       eapply FlatImp.exec.weaken.
       - eapply spill_fun_correct; try eassumption.
-        unfold call_spec. intros * E. rewrite E in *. fwd.
-        (*eapply FlatImp.exec.exec_ext.*) exact H1p2.
+        unfold call_spec. intros * E. rewrite E in *. fwd. exact H1p2.
       - cbv beta. intros. fwd. eexists. intuition eauto.
         do 2 eexists. intuition eauto. rewrite remove_n_r_spec.
         rewrite H2p1p2. rewrite rev_involutive. reflexivity.
@@ -783,7 +780,6 @@ Section WithWordAndMem.
         (initial: MetricRiscvMachine),
         NoDup (map fst fs) ->
         MetricLeakageSemantics.call (pick_sp := pick_sp) (map.of_list fs) fname kH t mH argvals (cost_spill_spec mcH) post ->
-        forall mcL,
         map.get (map.of_list finfo) fname = Some f_rel_pos ->
         req_stack_size <= word.unsigned (word.sub stack_hi stack_lo) / bytes_per_word ->
         word.unsigned (word.sub stack_hi stack_lo) mod bytes_per_word = 0 ->