From d9cb57d15ce6be4513ec38bf8f1baeadc2f2f872 Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Fri, 10 Jan 2025 16:38:33 -0500 Subject: [PATCH] m --- compiler/src/compiler/Pipeline.v | 68 +++++++++++++++----------------- 1 file changed, 32 insertions(+), 36 deletions(-) diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v index 568c0defd..d7bd92fe7 100644 --- 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 ->