From 1cd381a5e51912430acbc5c790aa3f0e04f4eb2d Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Thu, 13 Apr 2023 04:48:42 -0400 Subject: [PATCH 01/14] starting file for new phase --- compiler/src/compiler/DeadAssignmentDef.v | 69 +++++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 compiler/src/compiler/DeadAssignmentDef.v diff --git a/compiler/src/compiler/DeadAssignmentDef.v b/compiler/src/compiler/DeadAssignmentDef.v new file mode 100644 index 00000000..fdb505f8 --- /dev/null +++ b/compiler/src/compiler/DeadAssignmentDef.v @@ -0,0 +1,69 @@ +Require Import compiler.util.Common. +Require Import compiler.FlatImp. +Require Import Coq.Lists.List. Import ListNotations. +Require Import bedrock2.Syntax. +Require Import coqutil.Tactics.fwd. +Require Import String. +Open Scope Z_scope. + +Local Notation var := String.string (only parsing). + +Section WithArgs. + Context (is5BitImmediate : Z -> bool). + Context (is12BitImmediate: Z -> bool). + + Context {env: map.map String.string (list var * list var * stmt var)}. + + Fixpoint useImmediate(s: stmt string) : stmt string := + match s with + | SIf c s1 s2 => SIf c (useImmediate s1) (useImmediate s2) + | SLoop s1 c s2 => SLoop (useImmediate s1) c (useImmediate s2) + | SStackalloc v1 sz1 s => SStackalloc v1 sz1 (useImmediate s) + | SSeq s1 s2 => + let default := SSeq (useImmediate s1) (useImmediate s2) in + match s1, s2 with + | SLit v1 l1, SOp v2 op v2a (Var v2b) => + match op with + | Syntax.bopname.add + | Syntax.bopname.and + | Syntax.bopname.or + | Syntax.bopname.xor => if (is12BitImmediate l1) then + if eqb v1 v2b then + SSeq s1 (SOp v2 op v2a (Const l1)) + else if eqb v1 v2a then + SSeq s1 (SOp v2 op v2b (Const l1)) + else default + else default + | Syntax.bopname.ltu + | Syntax.bopname.lts => if (is12BitImmediate l1) then + if eqb v1 v2b then + SSeq s1 (SOp v2 op v2a (Const l1)) + else default + else default + | Syntax.bopname.srs + | Syntax.bopname.sru + | Syntax.bopname.slu => if (is5BitImmediate l1) then + if eqb v1 v2b then + SSeq s1 (SOp v2 op v2a (Const l1)) + else default + else default + | Syntax.bopname.sub => if (is12BitImmediate (-l1)) then + if eqb v1 v2b then + SSeq s1 (SOp v2 Syntax.bopname.add v2a (Const (-l1))) + else default + else default + | _ => default + end + | _, _ => default + end + | _ => s + end. + + Definition useimmediate_function: (list string * list string * stmt string) -> result (list string * list string * stmt string) := + fun '(argnames, retnames, body) => + let body' := useImmediate body in + Success (argnames, retnames, body'). + + Definition useimmediate_functions : env -> result env := + map.try_map_values useimmediate_function. +End WithArgs. From 29ad116ec162f6102cad12e8dc323fb3a7228ae5 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Thu, 13 Apr 2023 13:48:32 -0400 Subject: [PATCH 02/14] first pass at phase implementation --- compiler/src/compiler/DeadAssignmentDef.v | 102 ++++++------ compiler/src/compiler/Pipeline.v | 26 +++- .../src/compilerExamples/deadAssExample.v | 147 ++++++++++++++++++ 3 files changed, 225 insertions(+), 50 deletions(-) create mode 100644 compiler/src/compilerExamples/deadAssExample.v diff --git a/compiler/src/compiler/DeadAssignmentDef.v b/compiler/src/compiler/DeadAssignmentDef.v index fdb505f8..e4f62c91 100644 --- a/compiler/src/compiler/DeadAssignmentDef.v +++ b/compiler/src/compiler/DeadAssignmentDef.v @@ -5,65 +5,73 @@ Require Import bedrock2.Syntax. Require Import coqutil.Tactics.fwd. Require Import String. Open Scope Z_scope. - +Require Import coqutil.Map.MapEauto. +Require Import coqutil.Datatypes.ListSet. Local Notation var := String.string (only parsing). Section WithArgs. - Context (is5BitImmediate : Z -> bool). - Context (is12BitImmediate: Z -> bool). Context {env: map.map String.string (list var * list var * stmt var)}. - Fixpoint useImmediate(s: stmt string) : stmt string := + Local Notation bcond := (@FlatImp.bcond var). + + Definition accessed_vars_bcond(c: bcond): list var := + match c with + | CondBinary _ x y => list_union String.eqb [x] [y] + | CondNez x => [x] + end. + + Fixpoint live(s: stmt var)(used_after: list var): list var := match s with - | SIf c s1 s2 => SIf c (useImmediate s1) (useImmediate s2) - | SLoop s1 c s2 => SLoop (useImmediate s1) c (useImmediate s2) - | SStackalloc v1 sz1 s => SStackalloc v1 sz1 (useImmediate s) + | SSet x y + | SLoad _ x y _ + | SInlinetable _ x _ y => + list_union String.eqb [y] (list_diff String.eqb used_after [x]) + | SStore _ a x _ => list_union String.eqb [a; x] used_after + | SStackalloc x _ body => list_diff String.eqb (live body used_after) [x] + | SLit x _ => list_diff String.eqb used_after [x] + | SOp x _ y z => let var_z := match z with + | Var vz => [vz] + | Const _ => [] + end in + list_union String.eqb ([y] ++ var_z) (list_diff String.eqb used_after [x]) + | SIf c s1 s2 => list_union String.eqb + (list_union String.eqb (live s1 used_after) (live s2 used_after)) + (accessed_vars_bcond c) + | SSeq s1 s2 => live s1 (live s2 used_after) + | SLoop s1 c s2 => + live s1 (list_union String.eqb (accessed_vars_bcond c) (list_union String.eqb used_after (live s2 []))) + | SSkip => used_after + | SCall binds _ args + | SInteract binds _ args => list_union String.eqb args (list_diff String.eqb used_after binds) + end. + + Fixpoint deadAssignment(used_after: list var)(s: stmt var) : stmt var := + let deadAssignment' := deadAssignment used_after in + match s with + | SIf c s1 s2 => SIf c (deadAssignment' s1) (deadAssignment' s2) + | SLoop s1 c s2 => SLoop s1 c s2 (* loops are scary so skipping this case for now *) + | SStackalloc v1 sz1 s => SStackalloc v1 sz1 (deadAssignment' s) | SSeq s1 s2 => - let default := SSeq (useImmediate s1) (useImmediate s2) in - match s1, s2 with - | SLit v1 l1, SOp v2 op v2a (Var v2b) => - match op with - | Syntax.bopname.add - | Syntax.bopname.and - | Syntax.bopname.or - | Syntax.bopname.xor => if (is12BitImmediate l1) then - if eqb v1 v2b then - SSeq s1 (SOp v2 op v2a (Const l1)) - else if eqb v1 v2a then - SSeq s1 (SOp v2 op v2b (Const l1)) - else default - else default - | Syntax.bopname.ltu - | Syntax.bopname.lts => if (is12BitImmediate l1) then - if eqb v1 v2b then - SSeq s1 (SOp v2 op v2a (Const l1)) - else default - else default - | Syntax.bopname.srs - | Syntax.bopname.sru - | Syntax.bopname.slu => if (is5BitImmediate l1) then - if eqb v1 v2b then - SSeq s1 (SOp v2 op v2a (Const l1)) - else default - else default - | Syntax.bopname.sub => if (is12BitImmediate (-l1)) then - if eqb v1 v2b then - SSeq s1 (SOp v2 Syntax.bopname.add v2a (Const (-l1))) - else default - else default - | _ => default - end - | _, _ => default - end + let s2' := deadAssignment' s2 in + let s1_used_after := live s2' used_after in + SSeq (deadAssignment s1_used_after s1) (s2') + | SLit x v => + if existsb (String.eqb x) used_after + then s else SSkip + | SOp x op v1 v2 => + if existsb (String.eqb x) used_after + then s else SSkip | _ => s end. - Definition useimmediate_function: (list string * list string * stmt string) -> result (list string * list string * stmt string) := + Definition deadassignment_function: (list string * list string * stmt string) -> result (list string * list string * stmt string) := fun '(argnames, retnames, body) => - let body' := useImmediate body in + let body' := deadAssignment retnames body in Success (argnames, retnames, body'). - Definition useimmediate_functions : env -> result env := - map.try_map_values useimmediate_function. + Definition deadassignment_functions : env -> result env := + map.try_map_values deadassignment_function. + + End WithArgs. diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v index 6dd84f8b..429d8c0f 100644 --- a/compiler/src/compiler/Pipeline.v +++ b/compiler/src/compiler/Pipeline.v @@ -51,8 +51,9 @@ Require Import coqutil.Tactics.autoforward. Require Import compiler.FitsStack. Require Import compiler.LowerPipeline. Require Import bedrock2.WeakestPreconditionProperties. -Require Import compiler.UseImmediateDef. -Require Import compiler.UseImmediate. +Require Export compiler.UseImmediateDef. +Require Export compiler.UseImmediate. +Require Export compiler.DeadAssignmentDef. Import Utility. Section WithWordAndMem. @@ -440,7 +441,8 @@ Section WithWordAndMem. (compose_phases (useimmediate_functions is5BitImmediate is12BitImmediate) (compose_phases regalloc_functions (compose_phases spill_functions - (riscvPhase compile_ext_call))))). + (riscvPhase compile_ext_call))))). + Lemma composed_compiler_correct: phase_correct SrcLang RiscvLang composed_compile. Proof. @@ -459,6 +461,24 @@ Section WithWordAndMem. | Failure e => Failure e end. + (* only for testing the dead assignment phase, remove in the future *) + Definition composed_compile': + string_keyed_map (list string * list string * cmd) -> + result (list Instruction * string_keyed_map Z * Z) := + (compose_phases flatten_functions + (compose_phases (useimmediate_functions is5BitImmediate is12BitImmediate) + (compose_phases deadassignment_functions + (compose_phases regalloc_functions + (compose_phases spill_functions + (riscvPhase compile_ext_call)))))). + + (* only for testing the dead assignment phase, remove in the future *) + Definition compile'(funs: list (string * (list string * list string * cmd))): + result (list Instruction * list (string * Z) * Z) := + match composed_compile' (map.of_list funs) with + | Success (insts, pos, space) => Success (insts, map.tuples pos, space) + | Failure e => Failure e + end. Definition valid_src_fun: (string * (list string * list string * cmd)) -> bool := fun '(name, (args, rets, body)) => andb (List.list_eqb String.eqb (List.dedup String.eqb args) args) diff --git a/compiler/src/compilerExamples/deadAssExample.v b/compiler/src/compilerExamples/deadAssExample.v new file mode 100644 index 00000000..363ec57e --- /dev/null +++ b/compiler/src/compilerExamples/deadAssExample.v @@ -0,0 +1,147 @@ +Require Import compiler.ExprImp. +Require Import compiler.Pipeline. +Require Import compiler.DeadAssignmentDef. +Require Import riscv.Spec.Decode. +Require Import riscv.Utility.Words32Naive. +Require Import riscv.Utility.DefaultMemImpl32. +Require riscv.Utility.InstructionNotations. +Require Import riscv.Utility.Encode. +Require Import coqutil.Map.SortedList. +Require coqutil.Map.SortedListString. +Require Import compiler.MemoryLayout. +Require riscv.Utility.bverify. +Open Scope Z_scope. +Open Scope string_scope. +Open Scope ilist_scope. + +Local Instance funpos_env: map.map string Z := SortedListString.map _. + + + (* dead assignments because of immediate optimization *) + + (* loading a constant into a variable usually assigns the constant first to a + temp variable, but with the useimmediate optimization the temp variable shouldn't + be used *) + Definition test_constant : (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.seq + (cmd.set "ret_val" (expr.literal 420)) + (cmd.set "ret_val" (expr.literal 69))))). + + (* making sure that the optimization doesn't optimize out an assignment to the + same variable (e.g. x = x + constant), and that it recurses into a stack alloc. *) + Definition test_stackalloc : (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.stackalloc "x" 4 + (cmd.seq (cmd.set "x" (expr.literal 127)) + (cmd.seq (cmd.set "x" (expr.op bopname.add (expr.var "x") + (expr.literal 85))) + (cmd.set "ret_val" (expr.var "x"))))))). + + + (* checking that if-else's are recursed into *) + Definition test_ifelse : (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.seq (cmd.set "ret_val" (expr.literal 91)) + (cmd.cond + (expr.var "ret_val") + (cmd.set "ret_val" (expr.literal 63)) + (cmd.seq + (cmd.set "ret_val" (expr.literal 123)) + (cmd.set "ret_val" (expr.literal 369))) + )))). + +(* test to avoid breaking loops by doing nothing in a loop *) + Definition test_loop : (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.stackalloc "x" 4 + (cmd.seq (cmd.set "ret_val" (expr.literal 1)) + (cmd.while (expr.var "x") + (cmd.seq + (cmd.set "ret_val" + (expr.op bopname.add + (expr.var "ret_val") + (expr.var "ret_val"))) + (cmd.set "x" + (expr.op bopname.sub + (expr.var "x") + (expr.literal 1))))))))). + + +(* test to check breaking a call*) + Definition test_call_fn : (string * (list string * list string * cmd)) + := ("add", (["x"; "y"], ["ret_val"], + (cmd.set "ret_val" + (expr.op bopname.add + (expr.var "x") + (expr.var "y"))))). + + Definition test_call: (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.call ["ret_val"] "add" [expr.literal 101; expr.literal 123]))). + + + Definition compile_ext_call(posenv: funpos_env)(mypos stackoffset: Z)(s: FlatImp.stmt Z) : list Instruction := []. + +Local Instance RV32I_bitwidth: FlatToRiscvCommon.bitwidth_iset 32 RV32I. +Proof. reflexivity. Qed. + +Definition multi_compile funs_lists := + List.all_success + (List.map + (fun x => '(insts, _, _) <- (compile compile_ext_call x) ;; Success insts) funs_lists). + +(* Expressing nested list literals as [[x]] is wonky + because of [[]] being used for list of Instructions *) +Definition imm_asm: list (list Instruction). + let r := eval cbv in (multi_compile + ([test_constant] :: + [test_stackalloc] :: + [test_ifelse] :: + [test_loop] :: + [test_call_fn; test_call] :: [])) in set (res := r). + match goal with + | res := Success (?x) |- _ => exact x + end. +Defined. + + + +Definition multi_compile' funs_lists := + List.all_success + (List.map + (fun x => '(insts, _, _) <- (compile' compile_ext_call x) ;; Success insts) funs_lists). + +Definition imm_asm' : list (list Instruction). + let r := eval cbv in (multi_compile' + ([test_constant] :: + [test_stackalloc] :: + [test_ifelse] :: + [test_loop] :: + [test_call_fn; test_call] :: [])) in set (res := r). + match goal with + | res := Success (?x) |- _ => exact x + end. +Defined. + +Module PrintAssembly. + Import riscv.Utility.InstructionNotations. + Goal True. let r := eval unfold imm_asm in imm_asm in idtac (* r *) . Abort. +End PrintAssembly. + + +Module PrintAssembly'. + Import riscv.Utility.InstructionNotations. + Goal True. let r := eval unfold imm_asm' in imm_asm' in idtac (* r *) . Abort. + +End PrintAssembly'. + +Module CheckAssembly. + Goal Forall (bverify.validInstructions RV32I) imm_asm. + repeat (constructor; [solve + [apply bverify.bvalidInstructions_valid; + vm_compute; reflexivity] + | ]). + constructor. + Qed. +End CheckAssembly. From 5d3efab852164f35827c69ba3c33ac40da914295 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Tue, 18 Apr 2023 07:32:22 -0400 Subject: [PATCH 03/14] first pass at loop implementation, outline of correctness proof --- compiler/src/compiler/DeadAssignment.v | 34 +++++++++ compiler/src/compiler/DeadAssignmentDef.v | 20 +++++- compiler/src/compiler/Pipeline.v | 36 ++++++++++ .../src/compilerExamples/deadAssExample.v | 72 +++++++++++++------ 4 files changed, 138 insertions(+), 24 deletions(-) create mode 100644 compiler/src/compiler/DeadAssignment.v diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v new file mode 100644 index 00000000..03b9f3be --- /dev/null +++ b/compiler/src/compiler/DeadAssignment.v @@ -0,0 +1,34 @@ +Require Import compiler.util.Common. +Require Import compiler.FlatImp. +Require Import Coq.Lists.List. Import ListNotations. +Require Import bedrock2.Syntax. +Require Import coqutil.Tactics.fwd. +Require Import String. +Require Import compiler.DeadAssignmentDef. +Require Import bedrock2.MetricLogging. + +Local Notation var := String.string (only parsing). + +Section WithArguments. + Context {width : Z}. + Context {BW : Bitwidth.Bitwidth width }. + Context {word : word width } {word_ok : word.ok word}. + Context {env : map.map string (list var * list var * stmt var) } {env_ok : map.ok env}. + Context {mem : map.map word (Init.Byte.byte : Type) } {mem_ok: map.ok mem}. + Context {locals : map.map string word } {locals_ok: map.ok locals}. + Context {ext_spec : Semantics.ExtSpec} {ext_spec_ok: Semantics.ext_spec.ok ext_spec}. + + Local Hint Constructors exec: core. +(* + Lemma deadassignment_correct_aux: + forall eH eL, + deadassignment_functions eH = Success eL -> + forall sH t m mcH lH post, + exec eH sH t m lH mcH post -> + exec eL (??? sH) t m lH mcH post. + Proof. + induction 2. + (* most cases stay the same *) + all: try solve [simpl; eauto]. + Admitted. *) +End WithArguments. diff --git a/compiler/src/compiler/DeadAssignmentDef.v b/compiler/src/compiler/DeadAssignmentDef.v index e4f62c91..85b13596 100644 --- a/compiler/src/compiler/DeadAssignmentDef.v +++ b/compiler/src/compiler/DeadAssignmentDef.v @@ -50,16 +50,30 @@ Section WithArgs. let deadAssignment' := deadAssignment used_after in match s with | SIf c s1 s2 => SIf c (deadAssignment' s1) (deadAssignment' s2) - | SLoop s1 c s2 => SLoop s1 c s2 (* loops are scary so skipping this case for now *) + | SLoop s1 c s2 => + let after_s1 := (list_union String.eqb (used_after) (accessed_vars_bcond c)) + in let after_s2 := live s2 after_s1 + in let after_s1' := (list_union + String.eqb + used_after + (list_union + String.eqb + (after_s2) + (accessed_vars_bcond c))) + in let after_s2' := live s2 after_s1' + in SLoop (deadAssignment after_s1' s1) c (deadAssignment after_s2' s2) | SStackalloc v1 sz1 s => SStackalloc v1 sz1 (deadAssignment' s) | SSeq s1 s2 => let s2' := deadAssignment' s2 in let s1_used_after := live s2' used_after in SSeq (deadAssignment s1_used_after s1) (s2') - | SLit x v => + | SLit x _ => + if existsb (String.eqb x) used_after + then s else SSkip + | SOp x _ _ _ => if existsb (String.eqb x) used_after then s else SSkip - | SOp x op v1 v2 => + | SSet x _ => if existsb (String.eqb x) used_after then s else SSkip | _ => s diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v index 429d8c0f..2f22991b 100644 --- a/compiler/src/compiler/Pipeline.v +++ b/compiler/src/compiler/Pipeline.v @@ -300,6 +300,42 @@ Section WithWordAndMem. - eauto. Qed. + Lemma deadassignment_functions_NoDup: forall funs funs', + (forall f argnames retnames body, + map.get funs f = Some (argnames, retnames, body) -> NoDup argnames /\ NoDup retnames) -> + (deadassignment_functions funs = Success funs') -> + forall f argnames retnames body, + map.get funs' f = Some (argnames, retnames, body) -> NoDup argnames /\ NoDup retnames. + Proof. + unfold deadassignment_functions. intros. + eapply map.try_map_values_bw in H0. + 2: { eassumption. } + unfold deadassignment_function in *. + fwd. + eapply H. + eassumption. + Qed. + + Lemma deadassignment_correct: phase_correct FlatWithStrVars FlatWithStrVars deadassignment_functions. + Proof. + unfold FlatWithStrVars. + split; cbn. + { unfold map.forall_values, ParamsNoDup. intros. + destruct v as ((argnames & retnames) & body). + eapply deadassignment_functions_NoDup; try eassumption. + intros. specialize H0 with (1 := H2). + simpl in H0. assumption. + } + + unfold locals_based_call_spec. intros. fwd. + pose proof H0 as GI. + unfold deadassignment_functions in GI. + eapply map.try_map_values_fw in GI. 2: eassumption. + unfold deadassignment_function in GI. fwd. + eexists _, _, _, _. split. 1: eassumption. split. 1: eassumption. + intros. + Admitted. + Lemma regalloc_functions_NoDup: forall funs funs', regalloc_functions funs = Success funs' -> forall f argnames retnames body, diff --git a/compiler/src/compilerExamples/deadAssExample.v b/compiler/src/compilerExamples/deadAssExample.v index 363ec57e..23a6cdec 100644 --- a/compiler/src/compilerExamples/deadAssExample.v +++ b/compiler/src/compilerExamples/deadAssExample.v @@ -51,21 +51,6 @@ Local Instance funpos_env: map.map string Z := SortedListString.map _. (cmd.set "ret_val" (expr.literal 369))) )))). -(* test to avoid breaking loops by doing nothing in a loop *) - Definition test_loop : (string * (list string * list string * cmd)) - := ("main", ([]: list string, ["ret_val"], - (cmd.stackalloc "x" 4 - (cmd.seq (cmd.set "ret_val" (expr.literal 1)) - (cmd.while (expr.var "x") - (cmd.seq - (cmd.set "ret_val" - (expr.op bopname.add - (expr.var "ret_val") - (expr.var "ret_val"))) - (cmd.set "x" - (expr.op bopname.sub - (expr.var "x") - (expr.literal 1))))))))). (* test to check breaking a call*) @@ -78,8 +63,53 @@ Local Instance funpos_env: map.map string Z := SortedListString.map _. Definition test_call: (string * (list string * list string * cmd)) := ("main", ([]: list string, ["ret_val"], - (cmd.call ["ret_val"] "add" [expr.literal 101; expr.literal 123]))). - + (cmd.call ["ret_val"] "add" [expr.literal 131; expr.literal (-97)]))). + (* test to check simple loops *) + Definition test_loop_fn : (string * (list string * list string * cmd)) + := ("add", (["x"; "y"], ["ret_val"], + (cmd.seq (cmd.set "ret_val" (expr.var "x")) + (cmd.while + (expr.op + bopname.or + (expr.op + bopname.lts + (expr.var "y") + (expr.literal 0)) + (expr.op + bopname.lts + (expr.literal 0) + (expr.var "y"))) + (cmd.cond + (expr.op + bopname.lts + (expr.var "y") + (expr.literal 0)) + (cmd.seq + (cmd.set "ret_val" + (expr.op + bopname.sub + (expr.var "ret_val") + (expr.literal 1))) + (cmd.set "y" + (expr.op + bopname.add + (expr.var "y") + (expr.literal 1)))) + (cmd.seq + (cmd.set "ret_val" + (expr.op + bopname.add + (expr.var "ret_val") + (expr.literal 1))) + (cmd.set "y" + (expr.op + bopname.sub + (expr.var "y") + (expr.literal 1))))))))). + + Definition test_loop: (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.call ["ret_val"] "add" [expr.literal 131; expr.literal (-97)]))). Definition compile_ext_call(posenv: funpos_env)(mypos stackoffset: Z)(s: FlatImp.stmt Z) : list Instruction := []. @@ -98,7 +128,7 @@ Definition imm_asm: list (list Instruction). ([test_constant] :: [test_stackalloc] :: [test_ifelse] :: - [test_loop] :: + [test_loop_fn; test_loop] :: [test_call_fn; test_call] :: [])) in set (res := r). match goal with | res := Success (?x) |- _ => exact x @@ -117,7 +147,7 @@ Definition imm_asm' : list (list Instruction). ([test_constant] :: [test_stackalloc] :: [test_ifelse] :: - [test_loop] :: + [test_loop_fn; test_loop] :: [test_call_fn; test_call] :: [])) in set (res := r). match goal with | res := Success (?x) |- _ => exact x @@ -132,12 +162,12 @@ End PrintAssembly. Module PrintAssembly'. Import riscv.Utility.InstructionNotations. - Goal True. let r := eval unfold imm_asm' in imm_asm' in idtac (* r *) . Abort. + Goal True. let r := eval unfold imm_asm' in imm_asm' in idtac (* r *) . Abort. End PrintAssembly'. Module CheckAssembly. - Goal Forall (bverify.validInstructions RV32I) imm_asm. + Goal Forall (bverify.validInstructions RV32I) imm_asm'. repeat (constructor; [solve [apply bverify.bvalidInstructions_valid; vm_compute; reflexivity] From a05a6b151833309d441b76e0838f6f4277634723 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Sat, 22 Apr 2023 22:46:52 -0400 Subject: [PATCH 04/14] first pass at possible correctness lemma; changes to example --- compiler/src/compiler/DeadAssignment.v | 290 +++++++++++++++++- compiler/src/compiler/DeadAssignmentDef.v | 14 +- .../src/compilerExamples/deadAssExample.v | 101 +++--- 3 files changed, 328 insertions(+), 77 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index 03b9f3be..4746418c 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -6,6 +6,7 @@ Require Import coqutil.Tactics.fwd. Require Import String. Require Import compiler.DeadAssignmentDef. Require Import bedrock2.MetricLogging. +Require Import coqutil.Datatypes.PropSet. Local Notation var := String.string (only parsing). @@ -19,16 +20,291 @@ Section WithArguments. Context {ext_spec : Semantics.ExtSpec} {ext_spec_ok: Semantics.ext_spec.ok ext_spec}. Local Hint Constructors exec: core. -(* +(* claim that +- after-optimization program assigns less than before-optimization (in locals) +- but return values always the same? as fxn of inputs? *) + (* after-optimization contain all before-optimization variables that were live *) + + (* old lemma breaks if post checks dead variables *) + (* Hint Resolve : map_hints. Copy style from FlatToRiscvFunctions *) + Lemma agree_on_refl : + forall keySet (m : locals), + map.agree_on keySet m m. + Proof. + intros. + unfold map.agree_on. + intros. + reflexivity. + Qed. + + Lemma sameset_in: + forall (s1 s2: set string), + sameset s1 s2 -> + forall k, k \in s1 <-> k \in s2. + Proof. + intros. + unfold iff. + propositional idtac. + - unfold sameset in H. + destruct H. + unfold subset in H. + eauto. + - unfold sameset in H. + destruct H. + unfold subset in H0. + eauto. + Qed. + + Lemma union_iff: + forall {E: Type} (s1 s2: set E) (x : E), + union s1 s2 x <-> s1 x \/ s2 x. + Proof. + intros. + unfold iff. + propositional idtac. + Qed. + + + Lemma existsb_of_list : + forall k keySet, + existsb (eqb k) keySet = true <-> k \in of_list keySet. + Proof. + intros. + simpl. + unfold iff. + propositional idtac. + - induction keySet. + + simpl in Hyp. discriminate. + + eapply sameset_in. + * eapply of_list_cons. + * unfold add. eapply union_iff. + simpl in Hyp. + apply Bool.orb_prop in Hyp. + destruct Hyp. + -- left. unfold singleton_set. eapply eqb_eq. rewrite eqb_sym. assumption. + -- right. eapply IHkeySet. eassumption. + - induction keySet. + + unfold of_list in Hyp. simpl in Hyp. + auto. + + simpl. assert (sameset (of_list (a :: keySet)) (add (of_list keySet) a) ) by apply of_list_cons. + assert (k \in (add (of_list keySet) a)). + { eapply sameset_in; eauto. } + unfold add in H0. + eapply union_iff in H0. destruct H0. + * unfold singleton_set in H0. rewrite H0. + rewrite eqb_refl. + rewrite Bool.orb_true_l. + reflexivity. + * assert (existsb (eqb k) keySet = true). + -- eapply IHkeySet. eapply H0. + -- rewrite H1. rewrite Bool.orb_true_r. reflexivity. + Qed. + + + + Lemma agree_on_not_in: + forall keySet (m: locals) x, + existsb (String.eqb x) keySet = false -> + forall y, + map.agree_on (PropSet.of_list keySet) (map.put m x y) m. + Proof. + intros. + unfold map.agree_on. + intros. + rewrite map.get_put_dec. + destr (x =? k)%string. + - apply existsb_of_list in H0. + rewrite H in H0. discriminate. + - reflexivity. + Qed. + + + Lemma agree_on_subset: + forall s1 s2 (m1 m2: locals), + map.agree_on s2 m1 m2 -> + subset s1 s2 -> + map.agree_on s1 m1 m2. + Proof. + intros. + unfold map.agree_on in *. + intros. + unfold subset in *. + apply H0 in H1. + eapply H. + eassumption. + Qed. + + + Lemma deadassignment_correct_aux: forall eH eL, deadassignment_functions eH = Success eL -> - forall sH t m mcH lH post, - exec eH sH t m lH mcH post -> - exec eL (??? sH) t m lH mcH post. + forall sH t m mcH lH postH, + exec eH sH t m lH mcH postH -> + forall used_after lL, + map.agree_on (of_list (live sH used_after)) lH lL + -> exec eL (deadAssignment used_after sH) t m lH mcH + (fun t' m' lL' mcL' => + exists lH' mcH', + map.agree_on (PropSet.of_list used_after) lH' lL' + /\ postH t' m' lH' mcH' ). Proof. induction 2. - (* most cases stay the same *) - all: try solve [simpl; eauto]. - Admitted. *) + 9: { simpl; eauto. + intros. destr (existsb (eqb x) (used_after)). + all: simpl. + - eapply @exec.set; eauto. + eexists. eexists. + split. + 2: eassumption. apply agree_on_refl. + - eapply @exec.skip; eauto. + eexists. eexists. + split. + 2: eassumption. + eapply agree_on_not_in. + assumption. + } + { simpl. + intros. + eapply @exec.interact; eauto. + intros. apply H3 in H5. + destruct H5. destruct H5. + eexists. split. + * eassumption. + * intros. eapply H6 in H7. + eexists. eexists. + split. + 2: { eapply H7. } + apply agree_on_refl. + } + { simpl. intros. + all: admit. + (* + eapply @exec.call; eauto. + * unfold deadassignment_functions in H. + unfold deadassignment_function in H. + simpl in H. + eapply map.try_map_values_fw in H. + 2: { eapply H0. } + destruct H. + destruct H. + inversion H. + rewrite <- H8 in H6. + apply H6. + * admit. + * admit. *) + } + { simpl. intros. + eapply @exec.load; eauto. + destr (find (eqb a) (List.removeb eqb x used_after)). + * eexists. eexists. + split. + 2: { eassumption. } + apply agree_on_refl. + * eexists. eexists. split. + 2: { eassumption. } + apply agree_on_refl. + } + { simpl. intros. + destr (find (eqb v) (used_after)). + - destr (find (eqb a) (used_after)). + * eapply @exec.store; eauto. + eexists. eexists. split. 2: eassumption. + apply agree_on_refl. + * eapply @exec.store; eauto. + eexists. eexists. split. 2: eassumption. + apply agree_on_refl. + - destr (find (eqb a) (v :: used_after)). + * eapply @exec.store; eauto. + eexists. eexists. split. 2: eassumption. + apply agree_on_refl. + * eapply @exec.store; eauto. + eexists. eexists. split. 2: eassumption. + apply agree_on_refl. + } + { simpl. intros. + eapply @exec.inlinetable; eauto. + eexists. eexists. split. 2: eassumption. + apply agree_on_refl. + } + { simpl. intros. + apply @exec.stackalloc; auto. + simpl. intros. + eapply @exec.weaken. + -- eapply H2. + ++ eassumption. + ++ eassumption. + ++ eapply agree_on_refl. + -- simpl. intros. + propositional idtac. + } + { simpl. intros. + destr (existsb (eqb x) used_after). + -- eapply @exec.lit; eauto. + eexists. eexists. split. + 2: eassumption. + apply agree_on_refl. + -- eapply @exec.skip; eauto. + eexists. eexists. split. + 2: eassumption. + eapply agree_on_not_in. + assumption. + } + { simpl. intros. + destr (existsb (eqb x) used_after). + -- eapply @exec.op; eauto. + eexists. eexists. split. + 2: eassumption. + apply agree_on_refl. + -- eapply @exec.skip; eauto. + eexists. eexists. split. + 2: eassumption. + eapply agree_on_not_in. + assumption. + } + { simpl. intros. + eapply @exec.if_true; eauto. + eapply IHexec. + all: eauto. + eapply agree_on_subset. + -- eapply H2. + -- unfold subset. intros. + rewrite ListSet.of_list_list_union. + apply in_union_l. + rewrite ListSet.of_list_list_union. + apply in_union_l. + assumption. + } + { simpl. intros. + eapply @exec.if_false; eauto. + eapply IHexec. + all: eauto. + eapply agree_on_subset. + -- eapply H2. + -- unfold subset. intros. + rewrite ListSet.of_list_list_union. + apply in_union_l. + rewrite ListSet.of_list_list_union. + apply in_union_r. + assumption. + } + { simpl. intros. + (* exec.loop *) + all: admit. + } + { simpl. + intros. + all: admit. + (* exec.seq *) + } + { simpl. + intros. + eapply @exec.skip; eauto. + eexists. eexists. + split. + 2: eassumption. + apply agree_on_refl. + } + all: admit. + Admitted. End WithArguments. diff --git a/compiler/src/compiler/DeadAssignmentDef.v b/compiler/src/compiler/DeadAssignmentDef.v index 85b13596..0c447d52 100644 --- a/compiler/src/compiler/DeadAssignmentDef.v +++ b/compiler/src/compiler/DeadAssignmentDef.v @@ -51,17 +51,9 @@ Section WithArgs. match s with | SIf c s1 s2 => SIf c (deadAssignment' s1) (deadAssignment' s2) | SLoop s1 c s2 => - let after_s1 := (list_union String.eqb (used_after) (accessed_vars_bcond c)) - in let after_s2 := live s2 after_s1 - in let after_s1' := (list_union - String.eqb - used_after - (list_union - String.eqb - (after_s2) - (accessed_vars_bcond c))) - in let after_s2' := live s2 after_s1' - in SLoop (deadAssignment after_s1' s1) c (deadAssignment after_s2' s2) + let used_after_s1 := (list_union String.eqb (accessed_vars_bcond c) (list_union String.eqb used_after (live s2 []))) in + let used_after_s2 := (live s1 used_after_s1) in + SLoop (deadAssignment used_after_s1 s1) c (deadAssignment used_after_s2 s2) | SStackalloc v1 sz1 s => SStackalloc v1 sz1 (deadAssignment' s) | SSeq s1 s2 => let s2' := deadAssignment' s2 in diff --git a/compiler/src/compilerExamples/deadAssExample.v b/compiler/src/compilerExamples/deadAssExample.v index 23a6cdec..5336ad73 100644 --- a/compiler/src/compilerExamples/deadAssExample.v +++ b/compiler/src/compilerExamples/deadAssExample.v @@ -24,92 +24,75 @@ Local Instance funpos_env: map.map string Z := SortedListString.map _. be used *) Definition test_constant : (string * (list string * list string * cmd)) := ("main", ([]: list string, ["ret_val"], - (cmd.seq - (cmd.set "ret_val" (expr.literal 420)) - (cmd.set "ret_val" (expr.literal 69))))). + (cmd.set "ret_val" (expr.literal 4193)))). - (* making sure that the optimization doesn't optimize out an assignment to the - same variable (e.g. x = x + constant), and that it recurses into a stack alloc. *) + (* making sure that the optimization recurses into a stack alloc. *) Definition test_stackalloc : (string * (list string * list string * cmd)) := ("main", ([]: list string, ["ret_val"], (cmd.stackalloc "x" 4 - (cmd.seq (cmd.set "x" (expr.literal 127)) - (cmd.seq (cmd.set "x" (expr.op bopname.add (expr.var "x") - (expr.literal 85))) - (cmd.set "ret_val" (expr.var "x"))))))). + (cmd.seq (cmd.set "x" (expr.literal 1303)) + (cmd.stackalloc "y" 4 + (cmd.seq (cmd.set "y" (expr.literal 1217)) + (cmd.set "ret_val" (expr.var "x")))))))). (* checking that if-else's are recursed into *) Definition test_ifelse : (string * (list string * list string * cmd)) := ("main", ([]: list string, ["ret_val"], - (cmd.seq (cmd.set "ret_val" (expr.literal 91)) - (cmd.cond - (expr.var "ret_val") - (cmd.set "ret_val" (expr.literal 63)) - (cmd.seq - (cmd.set "ret_val" (expr.literal 123)) - (cmd.set "ret_val" (expr.literal 369))) - )))). - + (cmd.stackalloc "x" 4 + (cmd.stackalloc "y" 4 + (cmd.seq (cmd.set "x" (expr.literal 7307)) + (cmd.seq (cmd.set "y" (expr.literal 1711)) + (cmd.cond + (expr.literal 9) + (cmd.set "ret_val" (expr.literal 6409)) + (cmd.set "ret_val" (expr.var "x"))))))))). (* test to check breaking a call*) Definition test_call_fn : (string * (list string * list string * cmd)) - := ("add", (["x"; "y"], ["ret_val"], - (cmd.set "ret_val" - (expr.op bopname.add - (expr.var "x") - (expr.var "y"))))). + := ("first_arg", (["x"; "y"], ["ret_val"], + (cmd.set "ret_val" (expr.var "x")))). Definition test_call: (string * (list string * list string * cmd)) := ("main", ([]: list string, ["ret_val"], - (cmd.call ["ret_val"] "add" [expr.literal 131; expr.literal (-97)]))). + (cmd.stackalloc "x" 4 + (cmd.stackalloc "y" 4 + (cmd.stackalloc "z" 4 + (cmd.seq (cmd.set "x" (expr.literal 7307)) + (cmd.seq (cmd.set "y" (expr.literal 1711)) + (cmd.seq (cmd.set "z" (expr.literal 9231)) + (cmd.call ["ret_val"] "first_arg" [expr.var "x"; expr.var "y"]))))))))). + (* test to check simple loops *) Definition test_loop_fn : (string * (list string * list string * cmd)) - := ("add", (["x"; "y"], ["ret_val"], - (cmd.seq (cmd.set "ret_val" (expr.var "x")) + := ("return_1019", (["x"; "y"], ["ret_val"], + (cmd.seq (cmd.set "ret_val" (expr.literal 0)) (cmd.while (expr.op - bopname.or - (expr.op - bopname.lts - (expr.var "y") - (expr.literal 0)) - (expr.op - bopname.lts - (expr.literal 0) - (expr.var "y"))) - (cmd.cond - (expr.op - bopname.lts - (expr.var "y") - (expr.literal 0)) - (cmd.seq - (cmd.set "ret_val" - (expr.op - bopname.sub - (expr.var "ret_val") - (expr.literal 1))) - (cmd.set "y" - (expr.op - bopname.add - (expr.var "y") - (expr.literal 1)))) + bopname.sub + (expr.var "ret_val") + (expr.literal 1019) + ) + (cmd.seq + (cmd.set "x" (expr.op + bopname.add + (expr.var "x") + (expr.literal 706))) (cmd.seq (cmd.set "ret_val" (expr.op bopname.add (expr.var "ret_val") (expr.literal 1))) - (cmd.set "y" - (expr.op - bopname.sub - (expr.var "y") - (expr.literal 1))))))))). + (cmd.set "y" (expr.op + bopname.xor + (expr.var "x") + (expr.literal 4902))))))))). Definition test_loop: (string * (list string * list string * cmd)) := ("main", ([]: list string, ["ret_val"], - (cmd.call ["ret_val"] "add" [expr.literal 131; expr.literal (-97)]))). + (cmd.call ["ret_val"] "return_1019" [expr.literal 131; expr.literal (-97)]))). Definition compile_ext_call(posenv: funpos_env)(mypos stackoffset: Z)(s: FlatImp.stmt Z) : list Instruction := []. @@ -156,13 +139,13 @@ Defined. Module PrintAssembly. Import riscv.Utility.InstructionNotations. - Goal True. let r := eval unfold imm_asm in imm_asm in idtac (* r *) . Abort. + Goal True. let r := eval unfold imm_asm in imm_asm in idtac (* r *). Abort. End PrintAssembly. Module PrintAssembly'. Import riscv.Utility.InstructionNotations. - Goal True. let r := eval unfold imm_asm' in imm_asm' in idtac (* r *) . Abort. + Goal True. let r := eval unfold imm_asm' in imm_asm' in idtac (* r *). Abort. End PrintAssembly'. From cda6dd871c742e4c9f2de3ce35c9d799df205f7d Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Mon, 1 May 2023 23:12:11 -0400 Subject: [PATCH 05/14] small progress on dead assignment proof --- compiler/src/compiler/DeadAssignment.v | 136 ++++++++++++++++++++----- 1 file changed, 113 insertions(+), 23 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index 4746418c..dba50bbd 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -136,6 +136,53 @@ Section WithArguments. + + Lemma agree_on_getmany : + forall rets (x st1 : locals), + map.agree_on (of_list rets) x st1 -> + map.getmany_of_list x rets = map.getmany_of_list st1 rets. + Proof. + intros. + induction rets. + - unfold map.getmany_of_list. simpl. reflexivity. + - unfold map.getmany_of_list. + simpl. + simpl in H. assert (map.agree_on (of_list rets) x st1). + { eapply agree_on_subset. + + eapply H. + + unfold subset. + intros. eapply of_list_cons. + unfold add. + eapply in_union_r. + eassumption. + } + assert (map.agree_on (singleton_set a) x st1). + { eapply agree_on_subset. + + eapply H. + + unfold subset. + intros. eapply of_list_cons. + unfold add. + eapply in_union_l. + eassumption. + } + assert (map.get x a = map.get st1 a). + { unfold map.agree_on in H1. + eapply H1. + unfold singleton_set. + reflexivity. + } + rewrite H2. + destruct (map.get st1 a). + 2: reflexivity. + replace (List.option_all (map (map.get x) rets)) with (map.getmany_of_list x rets) by (unfold map.getmany_of_list; reflexivity). + replace (List.option_all (map (map.get st1) rets)) with (map.getmany_of_list st1 rets) by (unfold map.getmany_of_list; reflexivity). + eapply IHrets in H0. + rewrite H0. + reflexivity. + Qed. + + + Lemma deadassignment_correct_aux: forall eH eL, deadassignment_functions eH = Success eL -> @@ -150,20 +197,6 @@ Section WithArguments. /\ postH t' m' lH' mcH' ). Proof. induction 2. - 9: { simpl; eauto. - intros. destr (existsb (eqb x) (used_after)). - all: simpl. - - eapply @exec.set; eauto. - eexists. eexists. - split. - 2: eassumption. apply agree_on_refl. - - eapply @exec.skip; eauto. - eexists. eexists. - split. - 2: eassumption. - eapply agree_on_not_in. - assumption. - } { simpl. intros. eapply @exec.interact; eauto. @@ -178,9 +211,7 @@ Section WithArguments. apply agree_on_refl. } { simpl. intros. - all: admit. - (* - eapply @exec.call; eauto. + eapply @exec.call. * unfold deadassignment_functions in H. unfold deadassignment_function in H. simpl in H. @@ -191,8 +222,36 @@ Section WithArguments. inversion H. rewrite <- H8 in H6. apply H6. - * admit. - * admit. *) + * eassumption. + * eassumption. + * eapply IHexec. + (* for each index in len(argvs) + l[args[i]] = argvs[i]; + for each index in len(argvs) + st0[params[i]] = argvs[i] + (assuming distinct which we might also need to prove?) + + idea: show that live fbody rets = args or params and + then construct the appropriate lH? + ?? + *) + admit. + * intros. destruct H6. destruct H6. + destruct H6. eapply H4 in H7. + destruct H7. destruct H7. + destruct H7. destruct H8. + eexists. eexists. + split. + -- eapply agree_on_getmany in H6. + rewrite <- H6. + eassumption. + -- split. + ++ eapply H8. + ++ eexists. eexists. + split. + 2: eapply H9. + eapply agree_on_refl. + } { simpl. intros. eapply @exec.load; eauto. @@ -262,6 +321,20 @@ Section WithArguments. eapply agree_on_not_in. assumption. } + { simpl; eauto. + intros. destr (existsb (eqb x) (used_after)). + all: simpl. + - eapply @exec.set; eauto. + eexists. eexists. + split. + 2: eassumption. apply agree_on_refl. + - eapply @exec.skip; eauto. + eexists. eexists. + split. + 2: eassumption. + eapply agree_on_not_in. + assumption. + } { simpl. intros. eapply @exec.if_true; eauto. eapply IHexec. @@ -294,8 +367,26 @@ Section WithArguments. } { simpl. intros. - all: admit. - (* exec.seq *) + eapply @exec.seq; eauto. + - eapply IHexec. + eapply agree_on_subset. + + eapply H3. + + (* show that + of_list (live (deadAss used_after s2) used_after) + is subset of (live s2 used_after), and that + forall s1 u u', + subset u u' -> + subset (of_list (live s1 u)) (of_list live s1 u') *) + admit. + - simpl. intros. + eapply H2. + (* context has that there exists some lH' and mcH', + but goal has that a specific lH and mcH that satisfy mid + eexists. eexists. + all: eauto. + all: ad mit. + exec.seq *) + all: admit. } { simpl. intros. @@ -305,6 +396,5 @@ Section WithArguments. 2: eassumption. apply agree_on_refl. } - all: admit. - Admitted. + Admitted. End WithArguments. From 83c5436d5677d33319e0c857a607c79741592a49 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Wed, 17 May 2023 12:53:48 -0400 Subject: [PATCH 06/14] in-progress to make everything compile w/o invocation of dead assignment --- compiler/src/compiler/DeadAssignment.v | 623 ++++++++++++------- compiler/src/compiler/DeadAssignmentHelper.v | 289 +++++++++ 2 files changed, 681 insertions(+), 231 deletions(-) create mode 100644 compiler/src/compiler/DeadAssignmentHelper.v diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index dba50bbd..79ed645e 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -5,6 +5,7 @@ Require Import bedrock2.Syntax. Require Import coqutil.Tactics.fwd. Require Import String. Require Import compiler.DeadAssignmentDef. +Require Import compiler.DeadAssignmentHelper. Require Import bedrock2.MetricLogging. Require Import coqutil.Datatypes.PropSet. @@ -20,168 +21,382 @@ Section WithArguments. Context {ext_spec : Semantics.ExtSpec} {ext_spec_ok: Semantics.ext_spec.ok ext_spec}. Local Hint Constructors exec: core. -(* claim that -- after-optimization program assigns less than before-optimization (in locals) -- but return values always the same? as fxn of inputs? *) - (* after-optimization contain all before-optimization variables that were live *) - (* old lemma breaks if post checks dead variables *) - (* Hint Resolve : map_hints. Copy style from FlatToRiscvFunctions *) - Lemma agree_on_refl : - forall keySet (m : locals), - map.agree_on keySet m m. + Lemma live_monotone : + forall s used_after used_after', + subset (of_list used_after) (of_list used_after') -> + subset (of_list (live s used_after)) (of_list (live s used_after')). Proof. - intros. - unfold map.agree_on. - intros. - reflexivity. - Qed. + induction s; intros. - Lemma sameset_in: - forall (s1 s2: set string), - sameset s1 s2 -> - forall k, k \in s1 <-> k \in s2. - Proof. - intros. - unfold iff. - propositional idtac. - - unfold sameset in H. - destruct H. - unfold subset in H. - eauto. - - unfold sameset in H. - destruct H. - unfold subset in H0. - eauto. - Qed. + - (* SLoad *) + simpl. + destr (find (eqb a) (List.removeb eqb x used_after)). + + eapply find_some in E. + destr E. + eapply eqb_eq in H1. + subst. + eapply in_of_list in H0. + repeat rewrite ListSet.of_list_removeb in *. - Lemma union_iff: - forall {E: Type} (s1 s2: set E) (x : E), - union s1 s2 x <-> s1 x \/ s2 x. - Proof. - intros. - unfold iff. - propositional idtac. - Qed. + assert (subset (diff (of_list used_after) (singleton_set x)) (diff (of_list used_after') (singleton_set x))) by (eauto using subset_diff). + assert (s \in diff (of_list used_after') (singleton_set x)) by eauto. + rewrite <- ListSet.of_list_removeb in H2. - Lemma existsb_of_list : - forall k keySet, - existsb (eqb k) keySet = true <-> k \in of_list keySet. - Proof. - intros. - simpl. - unfold iff. - propositional idtac. - - induction keySet. - + simpl in Hyp. discriminate. - + eapply sameset_in. - * eapply of_list_cons. - * unfold add. eapply union_iff. - simpl in Hyp. - apply Bool.orb_prop in Hyp. - destruct Hyp. - -- left. unfold singleton_set. eapply eqb_eq. rewrite eqb_sym. assumption. - -- right. eapply IHkeySet. eassumption. - - induction keySet. - + unfold of_list in Hyp. simpl in Hyp. - auto. - + simpl. assert (sameset (of_list (a :: keySet)) (add (of_list keySet) a) ) by apply of_list_cons. - assert (k \in (add (of_list keySet) a)). - { eapply sameset_in; eauto. } - unfold add in H0. - eapply union_iff in H0. destruct H0. - * unfold singleton_set in H0. rewrite H0. - rewrite eqb_refl. - rewrite Bool.orb_true_l. - reflexivity. - * assert (existsb (eqb k) keySet = true). - -- eapply IHkeySet. eapply H0. - -- rewrite H1. rewrite Bool.orb_true_r. reflexivity. - Qed. + destr (find (eqb s) (List.removeb eqb x used_after')). + * rewrite ListSet.of_list_removeb. auto. + * eapply find_none in E. + 2: eapply H2. + rewrite eqb_refl in E. discriminate. + + simpl. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + * destr (find (eqb a) (List.removeb eqb x used_after')). + -- eapply find_some in E0. + destr E0. + eapply eqb_eq in H1. + subst. + eauto using in_singleton. + -- rewrite of_list_cons. + unfold add. eapply subset_union_rl. + eapply subset_ref. + * destr (find (eqb a) (List.removeb eqb x used_after')). + -- do 2 (rewrite ListSet.of_list_removeb). + eauto using subset_diff. + -- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + do 2 (rewrite ListSet.of_list_removeb). + eauto using subset_diff. + - (* SStore *) + simpl. + destr (find (eqb v) used_after). + + eapply find_some in E. + destr E. + eapply eqb_eq in H1. + subst. + assert (of_list used_after s) by (propositional idtac). + assert (of_list used_after' s). + { eapply H. auto. } + destr (find (eqb s) used_after'). + * destr (find (eqb a) used_after). + -- eapply find_some in E0. destr E0. + eapply eqb_eq in H4. + symmetry in H4. + subst. + assert (of_list used_after' a). + { eapply H. auto. } + destr (find (eqb a) used_after'). + ++ auto. + ++ eapply find_none in E0. + 2: { eapply H4. } + rewrite eqb_refl in E0. discriminate. + -- destr (find (eqb a) used_after'). + ++ rewrite of_list_cons. + unfold add. + eapply find_some in E1. + destr E1. + eapply eqb_eq in H4. + subst. + apply subset_union_l. + ** eauto using in_singleton. + ** eauto. + ++ repeat rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** apply subset_union_rl. + eapply subset_ref. + ** apply subset_union_rr. + auto. + * destr (find (eqb a) used_after). + -- eapply find_some in E0. destr E0. + eapply eqb_eq in H4. + symmetry in H4. + subst. + assert (of_list used_after' a). + { eapply H. auto. } + destr (find (eqb a) (s :: used_after')). + ++ rewrite of_list_cons. + unfold add. + eauto using subset_union_rr. + ++ rewrite of_list_cons. + unfold add. + eauto using subset_union_rr. + -- rewrite of_list_cons. + unfold add. + apply subset_union_l. + ++ destr (find (eqb a) (s :: used_after')). + ** eapply find_some in E1. + destr E1. + eapply eqb_eq in H4. + symmetry in H4. + subst. + eauto using in_singleton. + ** rewrite of_list_cons. + unfold add. + apply subset_union_rl. + eauto using subset_refl. + ++ destr (find (eqb a) (s :: used_after')). + ** rewrite of_list_cons. + unfold add. + apply subset_union_rr. + eauto. + ** rewrite of_list_cons. + unfold add. + apply subset_union_rr. + rewrite of_list_cons. + unfold add. + apply subset_union_rr. + eauto. + + destr (find (eqb a) (v :: used_after)). + * eapply find_some in E0. + destr E0. + eapply eqb_eq in H1. + symmetry in H1. + subst. + eapply in_inv in H0. + propositional idtac. + -- destr (find (eqb a) used_after'). + ++ simpl. rewrite E0. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + ** eapply in_singleton. + apply find_some in E0. + destr E0. + eapply eqb_eq in H1. + subst. + auto. + ** auto. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** destr (find (eqb a) (a :: used_after')). + --- rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + --- rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + ** destr (find (eqb a) (a :: used_after')). + --- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + assumption. + --- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + rewrite of_list_cons. + unfold add. + apply subset_union_rr. + assumption. + -- destr (find (eqb v) used_after'). + ++ rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** apply find_some in E0. + destr E0. + apply eqb_eq in H2. + symmetry in H2. subst. + destr (find (eqb a) used_after'). + --- eapply find_some in E0. + destr E0. eapply eqb_eq in H3. + subst. + auto using in_singleton. + --- eapply subset_trans. + 2: { rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + eapply subset_ref. } + eauto using in_singleton. + ** destr (find (eqb a) used_after'). + --- auto. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + auto. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** destr (find (eqb a) (v :: used_after')). + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + apply subset_ref. + ** destr (find (eqb a) (v :: used_after')). + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + assumption. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + assumption. + * simpl in E0. + destr (a =? v)%string; [ discriminate | ]. + destr (find (eqb v) used_after'). + -- apply find_some in E2. + destr E2. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb a) used_after'). + ++ apply find_some in E2. + destr E2. + apply eqb_eq in H2. + symmetry in H2. + subst. + rewrite of_list_cons. + unfold add. + apply subset_union_l; [ eauto using in_singleton | ]. + rewrite of_list_cons. + unfold add. + apply subset_union_l; [ eauto using in_singleton | eauto ]. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + ** rewrite of_list_cons. + unfold add. + apply subset_union_l. + --- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + eauto using in_singleton. + --- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + eauto. + -- rewrite of_list_cons. + unfold add. + apply subset_union_l. + ++ destr (find (eqb a) (v :: used_after')). + ** simpl in E3. + destr ((a =? v)%string). + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + --- apply find_some in E3. + destr E3. + apply eqb_eq in H1. + symmetry in H1. + subst. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + eauto using in_singleton. + ** rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ++ destr (find (eqb a) (v :: used_after')). + ** simpl in E3. + destr ((a =? v)%string). + --- + (* context here has something like + v <> v in premises, which should + make this trivial, but unsure how *) + rewrite of_list_cons. + unfold add. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + +++ eapply subset_union_rl. + eapply subset_ref. + +++ eauto using subset_union_rr. + --- rewrite of_list_cons. + unfold add. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + +++ eapply subset_union_rl. + eapply subset_ref. + +++ eauto using subset_union_rr. + ** rewrite of_list_cons. + unfold add. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + --- eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + --- eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + auto. + - simpl. + destr (find (eqb i) (List.removeb eqb x used_after)). + + apply find_some in E. + destr E. + apply eqb_eq in H1. + symmetry in H1. + subst. + all: admit. + Admitted. - Lemma agree_on_not_in: - forall keySet (m: locals) x, - existsb (String.eqb x) keySet = false -> - forall y, - map.agree_on (PropSet.of_list keySet) (map.put m x y) m. + Lemma deadAssignment_subset : + forall s1 s2 used_after, + subset (of_list (live s1 used_after)) (of_list (live s2 used_after)) -> + subset (of_list (live (deadAssignment used_after s1) used_after)) (of_list (live (deadAssignment used_after s2) used_after)). Proof. - intros. - unfold map.agree_on. - intros. - rewrite map.get_put_dec. - destr (x =? k)%string. - - apply existsb_of_list in H0. - rewrite H in H0. discriminate. - - reflexivity. - Qed. + Abort. - - Lemma agree_on_subset: - forall s1 s2 (m1 m2: locals), - map.agree_on s2 m1 m2 -> - subset s1 s2 -> - map.agree_on s1 m1 m2. + Lemma deadAssignment_subset' : + forall s u u', + subset (of_list u') (of_list u) -> + subset + (of_list (live (deadAssignment u s) u')) + (of_list (live s u)). Proof. - intros. - unfold map.agree_on in *. - intros. - unfold subset in *. - apply H0 in H1. - eapply H. - eassumption. - Qed. - - - + induction s. + Abort. - Lemma agree_on_getmany : - forall rets (x st1 : locals), - map.agree_on (of_list rets) x st1 -> - map.getmany_of_list x rets = map.getmany_of_list st1 rets. + Lemma deadassignment_live: + forall sH used_after, + subset + (of_list (live (deadAssignment used_after sH) used_after)) + (of_list (live sH used_after)). Proof. - intros. - induction rets. - - unfold map.getmany_of_list. simpl. reflexivity. - - unfold map.getmany_of_list. - simpl. - simpl in H. assert (map.agree_on (of_list rets) x st1). - { eapply agree_on_subset. - + eapply H. - + unfold subset. - intros. eapply of_list_cons. - unfold add. - eapply in_union_r. - eassumption. - } - assert (map.agree_on (singleton_set a) x st1). - { eapply agree_on_subset. - + eapply H. - + unfold subset. - intros. eapply of_list_cons. - unfold add. - eapply in_union_l. - eassumption. - } - assert (map.get x a = map.get st1 a). - { unfold map.agree_on in H1. - eapply H1. - unfold singleton_set. - reflexivity. - } - rewrite H2. - destruct (map.get st1 a). - 2: reflexivity. - replace (List.option_all (map (map.get x) rets)) with (map.getmany_of_list x rets) by (unfold map.getmany_of_list; reflexivity). - replace (List.option_all (map (map.get st1) rets)) with (map.getmany_of_list st1 rets) by (unfold map.getmany_of_list; reflexivity). - eapply IHrets in H0. - rewrite H0. - reflexivity. - Qed. - - + induction sH. + all: intros; try solve [simpl; eapply subset_refl]. + - (* SStackalloc *) + simpl. repeat (rewrite ListSet.of_list_removeb). eauto using subset_diff. + - (* SLit *) + simpl. destr (existsb (eqb x) used_after); simpl. + + eapply subset_ref. + + rewrite ListSet.of_list_removeb. + eapply sameset_sym. + eapply sameset_sym. + eauto using sameset_diff_not_in. + - (* SOp *) + simpl. destr (existsb (eqb x) used_after); simpl; [ eapply subset_ref | ]. + destr z; simpl. + + destr (find (eqb v) (List.removeb eqb x used_after)). + all: admit. + Admitted. Lemma deadassignment_correct_aux: forall eH eL, @@ -189,7 +404,7 @@ Section WithArguments. forall sH t m mcH lH postH, exec eH sH t m lH mcH postH -> forall used_after lL, - map.agree_on (of_list (live sH used_after)) lH lL + map.agree_on (of_list (live (deadAssignment used_after sH) used_after)) lH lL -> exec eL (deadAssignment used_after sH) t m lH mcH (fun t' m' lL' mcL' => exists lH' mcH', @@ -203,12 +418,7 @@ Section WithArguments. intros. apply H3 in H5. destruct H5. destruct H5. eexists. split. - * eassumption. - * intros. eapply H6 in H7. - eexists. eexists. - split. - 2: { eapply H7. } - apply agree_on_refl. + all: eauto using agree_on_refl. } { simpl. intros. eapply @exec.call. @@ -224,18 +434,7 @@ Section WithArguments. apply H6. * eassumption. * eassumption. - * eapply IHexec. - (* for each index in len(argvs) - l[args[i]] = argvs[i]; - for each index in len(argvs) - st0[params[i]] = argvs[i] - (assuming distinct which we might also need to prove?) - - idea: show that live fbody rets = args or params and - then construct the appropriate lH? - ?? - *) - admit. + * eapply IHexec. apply agree_on_refl. * intros. destruct H6. destruct H6. destruct H6. eapply H4 in H7. destruct H7. destruct H7. @@ -256,89 +455,40 @@ Section WithArguments. { simpl. intros. eapply @exec.load; eauto. destr (find (eqb a) (List.removeb eqb x used_after)). - * eexists. eexists. - split. - 2: { eassumption. } - apply agree_on_refl. - * eexists. eexists. split. - 2: { eassumption. } - apply agree_on_refl. + all: eauto using agree_on_refl. } { simpl. intros. - destr (find (eqb v) (used_after)). - - destr (find (eqb a) (used_after)). - * eapply @exec.store; eauto. - eexists. eexists. split. 2: eassumption. - apply agree_on_refl. - * eapply @exec.store; eauto. - eexists. eexists. split. 2: eassumption. - apply agree_on_refl. - - destr (find (eqb a) (v :: used_after)). - * eapply @exec.store; eauto. - eexists. eexists. split. 2: eassumption. - apply agree_on_refl. - * eapply @exec.store; eauto. - eexists. eexists. split. 2: eassumption. - apply agree_on_refl. + destr (find (eqb v) used_after). + - destr (find (eqb a) used_after); eauto using agree_on_refl. + - destr (find (eqb a) (v :: used_after)); eauto using agree_on_refl. } { simpl. intros. - eapply @exec.inlinetable; eauto. - eexists. eexists. split. 2: eassumption. - apply agree_on_refl. + eauto using agree_on_refl. } { simpl. intros. + all: eauto using agree_on_refl. apply @exec.stackalloc; auto. simpl. intros. eapply @exec.weaken. - -- eapply H2. - ++ eassumption. - ++ eassumption. - ++ eapply agree_on_refl. + -- eauto using agree_on_refl. -- simpl. intros. propositional idtac. } { simpl. intros. destr (existsb (eqb x) used_after). - -- eapply @exec.lit; eauto. - eexists. eexists. split. - 2: eassumption. - apply agree_on_refl. - -- eapply @exec.skip; eauto. - eexists. eexists. split. - 2: eassumption. - eapply agree_on_not_in. - assumption. + all: eauto 6 using agree_on_refl, agree_on_not_in. } { simpl. intros. destr (existsb (eqb x) used_after). - -- eapply @exec.op; eauto. - eexists. eexists. split. - 2: eassumption. - apply agree_on_refl. - -- eapply @exec.skip; eauto. - eexists. eexists. split. - 2: eassumption. - eapply agree_on_not_in. - assumption. + all: eauto 6 using agree_on_refl, agree_on_not_in. } { simpl; eauto. - intros. destr (existsb (eqb x) (used_after)). - all: simpl. - - eapply @exec.set; eauto. - eexists. eexists. - split. - 2: eassumption. apply agree_on_refl. - - eapply @exec.skip; eauto. - eexists. eexists. - split. - 2: eassumption. - eapply agree_on_not_in. - assumption. + intros. destr (existsb (eqb x) used_after). + all: eauto 6 using agree_on_refl, agree_on_not_in. } { simpl. intros. eapply @exec.if_true; eauto. eapply IHexec. - all: eauto. eapply agree_on_subset. -- eapply H2. -- unfold subset. intros. @@ -362,22 +512,33 @@ Section WithArguments. assumption. } { simpl. intros. + eapply @exec.loop; eauto. (* exec.loop *) all: admit. } { simpl. intros. - eapply @exec.seq; eauto. - - eapply IHexec. + eapply @exec.seq. + - (* specialize (IHexec (live s2 used_after)). + specialize IHexec with (1 := H3). + apply IHexec in H3. + eapply IHexec. *) + + eapply IHexec. eapply agree_on_subset. + eapply H3. - + (* show that + + admit. (* eapply live_monotone. *) + (* replace (live sH used_after) with (live sH used_after') + where subset used_after used_after' + *) + + (* show that of_list (live (deadAss used_after s2) used_after) is subset of (live s2 used_after), and that forall s1 u u', subset u u' -> subset (of_list (live s1 u)) (of_list live s1 u') *) - admit. + - simpl. intros. eapply H2. (* context has that there exists some lH' and mcH', diff --git a/compiler/src/compiler/DeadAssignmentHelper.v b/compiler/src/compiler/DeadAssignmentHelper.v new file mode 100644 index 00000000..5ee73f8b --- /dev/null +++ b/compiler/src/compiler/DeadAssignmentHelper.v @@ -0,0 +1,289 @@ +Require Import compiler.util.Common. +Require Import compiler.FlatImp. +Require Import Coq.Lists.List. Import ListNotations. +Require Import bedrock2.Syntax. +Require Import coqutil.Tactics.fwd. +Require Import String. +Require Import compiler.DeadAssignmentDef. +Require Import bedrock2.MetricLogging. +Require Import coqutil.Datatypes.PropSet. + +Local Notation var := String.string (only parsing). + +Section WithArguments. + Context {width : Z}. + Context {BW : Bitwidth.Bitwidth width }. + Context {word : word width } {word_ok : word.ok word}. + Context {locals : map.map string word } {locals_ok: map.ok locals}. + + Lemma agree_on_refl : + forall keySet (m : locals), + map.agree_on keySet m m. + Proof. + intros. + unfold map.agree_on. + intros. + reflexivity. + Qed. + + + Lemma sameset_in: + forall (s1 s2: set string), + sameset s1 s2 -> + forall k, k \in s1 <-> k \in s2. + Proof. + intros. + unfold iff. + propositional idtac. + - unfold sameset in H. + destruct H. + unfold subset in H. + eauto. + - unfold sameset in H. + destruct H. + unfold subset in H0. + eauto. + Qed. + + Lemma union_iff: + forall {E: Type} (s1 s2: set E) (x : E), + union s1 s2 x <-> s1 x \/ s2 x. + Proof. + intros. + unfold iff. + propositional idtac. + Qed. + + + Lemma existsb_of_list : + forall k keySet, + existsb (eqb k) keySet = true <-> k \in of_list keySet. + Proof. + intros. + simpl. + unfold iff. + propositional idtac. + - induction keySet. + + simpl in Hyp. discriminate. + + eapply sameset_in. + * eapply of_list_cons. + * unfold add. eapply union_iff. + simpl in Hyp. + apply Bool.orb_prop in Hyp. + destruct Hyp. + -- left. unfold singleton_set. eapply eqb_eq. rewrite eqb_sym. assumption. + -- right. eapply IHkeySet. eassumption. + - induction keySet. + + unfold of_list in Hyp. simpl in Hyp. + auto. + + simpl. assert (sameset (of_list (a :: keySet)) (add (of_list keySet) a) ) by apply of_list_cons. + assert (k \in (add (of_list keySet) a)). + { eapply sameset_in; eauto. } + unfold add in H0. + eapply union_iff in H0. destruct H0. + * unfold singleton_set in H0. rewrite H0. + rewrite eqb_refl. + rewrite Bool.orb_true_l. + reflexivity. + * assert (existsb (eqb k) keySet = true). + -- eapply IHkeySet. eapply H0. + -- rewrite H1. rewrite Bool.orb_true_r. reflexivity. + Qed. + + + + Lemma agree_on_not_in: + forall keySet (m: locals) x, + existsb (String.eqb x) keySet = false -> + forall y, + map.agree_on (PropSet.of_list keySet) (map.put m x y) m. + Proof. + intros. + unfold map.agree_on. + intros. + rewrite map.get_put_dec. + destr (x =? k)%string. + - apply existsb_of_list in H0. + rewrite H in H0. discriminate. + - reflexivity. + Qed. + + + Lemma agree_on_subset: + forall s1 s2 (m1 m2: locals), + map.agree_on s2 m1 m2 -> + subset s1 s2 -> + map.agree_on s1 m1 m2. + Proof. + intros. + unfold map.agree_on in *. + intros. + unfold subset in *. + eauto. + Qed. + + Lemma sameset_implies_subset: + forall (s1 s2: set string), + sameset s1 s2 -> + subset s1 s2. + Proof. + unfold sameset, subset. + intros. destr H; auto. + Qed. + + Lemma agree_on_sameset: + forall s1 s2 (m1 m2: locals), + map.agree_on s2 m1 m2 -> + sameset s1 s2 -> + map.agree_on s1 m1 m2. + Proof. + intros. + eauto using agree_on_subset, sameset_implies_subset. + Qed. + + Lemma agree_on_cons: + forall (h: string) t (m1 m2: locals), + map.agree_on (of_list (h :: t)) m1 m2 + -> map.get m1 h = map.get m2 h /\ + map.agree_on (of_list t) m1 m2. + Proof. + intros. + eapply agree_on_sameset in H. + 2: { eapply sameset_sym. eapply of_list_cons. } + unfold add in H. + split. + - assert (map.agree_on (singleton_set h) m1 m2). + { + eapply agree_on_subset. + - eapply H. + - eapply subset_union_rl. + eapply sameset_implies_subset. + eapply sameset_ref. + } + unfold map.agree_on in H0. + eapply H0. + unfold singleton_set. + eapply eq_refl. + - eapply agree_on_subset. + + eapply H. + + eapply subset_union_rr. + eapply sameset_implies_subset. + eapply sameset_ref. + Qed. + + Lemma agree_on_getmany : + forall rets (x st1 : locals), + map.agree_on (of_list rets) x st1 -> + map.getmany_of_list x rets = map.getmany_of_list st1 rets. + Proof. + intros. + unfold map.getmany_of_list. + induction rets; simpl; [ reflexivity | ]. + eapply agree_on_cons in H. + destr H. + rewrite H. + destr (map.get st1 a); [ | reflexivity ]. + eapply IHrets in H0. + rewrite H0. + reflexivity. + Qed. + + + Lemma subset_diff : + forall (s1 s2 s3: set string), + subset s1 s2 -> + subset (diff s1 s3) (diff s2 s3). + Proof. + intros. + unfold subset, diff. + intros. + assert (x \in s1 /\ ~ (x \in s3)). + { assert ((fun x : string => x \in s1 /\ ~ x \in s3) x) by exact H0. + simpl in H1. + assumption. + } + assert ((x \in s2) /\ (~x \in s3) -> x \in (fun x0 : string => x0 \in s2 /\ ~ x0 \in s3)). + { auto. } + eapply H2. + destr H1. split; eauto. + Qed. + + Lemma sameset_diff : + forall (s1 s2 s3: set string), + sameset s1 s2 -> + sameset (diff s1 s3) (diff s2 s3). + Proof. + intros. + unfold sameset in *. + destr H. + split; eauto using subset_diff. + Qed. + + Lemma sameset_diff_not_in: + forall (s: list string) x, + existsb (eqb x) s = false -> + sameset (diff (of_list s) (singleton_set x)) + (of_list s). + Proof. + intros. + unfold sameset; split. + * unfold subset; simpl. + intros. + unfold diff in H. + assert (x0 \in of_list s /\ ~ x0 \in singleton_set x) by auto. + destr H0; assumption. + * unfold subset; simpl. + intros. + unfold diff. + cut (x0 \in of_list s /\ ~ x0 \in singleton_set x); [ auto | ]. + split; [ assumption | ]. + eapply existsb_of_list in H0. + assert (x = x0 -> False). + { intros; subst. rewrite H0 in H. discriminate. } + auto. + Qed. + + + Lemma diff_subset: + forall s1 s2: set string, + subset (diff s1 s2) s1. + Proof. + intros. + unfold subset. + intros. + unfold diff in H. + assert (s1 x /\ ~ (s2 x)) by auto. + cut (s1 x). + { auto. } + destr H0; auto. + Qed. + + Lemma existsb_removeb_None: + forall (s: string) l, + existsb (eqb s) l = false -> + List.removeb eqb s l = l. + Proof. + intros. induction l. + - simpl; reflexivity. + - simpl in H. + apply Bool.orb_false_elim in H. + destr H. + eapply IHl in H0. + simpl. + rewrite H. simpl. + rewrite H0. + reflexivity. + Qed. + Lemma in_singleton : + forall (x: string) (s: list string), + In x s -> + subset (singleton_set x) (of_list s). + Proof. + intros. + unfold subset, singleton_set. + intros. + assert (eq x x0) by auto. + subst. + propositional idtac. + Qed. +End WithArguments. From 20a3581f571f4178d6fda8828843e16bf815f1a9 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Thu, 18 May 2023 10:35:44 -0400 Subject: [PATCH 07/14] in progress dead assignment lemmas --- compiler/src/compiler/DeadAssignment.v | 377 +++++++++++++++++++ compiler/src/compiler/DeadAssignmentHelper.v | 11 + 2 files changed, 388 insertions(+) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index 79ed645e..d5f94d6d 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -353,6 +353,383 @@ Section WithArguments. apply eqb_eq in H1. symmetry in H1. subst. + destr (find (eqb i) (List.removeb eqb x used_after')). + * repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + * rewrite of_list_cons. + unfold add. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff, subset_union_rr. + + rewrite of_list_cons. + unfold add. + apply subset_union_l. + * destr (find (eqb i) (List.removeb eqb x used_after')). + -- apply find_some in E0. + destr E0. + eapply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + -- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + * destr (find (eqb i) (List.removeb eqb x used_after')). + -- repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + -- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SStackalloc *) + simpl. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SLit *) + simpl. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SOp *) + simpl. destr z. + + simpl. + destr (find (eqb v) (List.removeb eqb x used_after)). + * simpl. + apply find_some in E. + destr E. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb y) (List.removeb eqb x used_after)). + -- simpl. + apply find_some in E. + destr E. + apply eqb_eq in H2. + symmetry in H2. + subst. + destr (find (eqb v) (List.removeb eqb x used_after')). + ++ apply find_some in E. + destr E. + eapply eqb_eq in H3. + symmetry in H3. + subst. + destr (find (eqb y) (List.removeb eqb x used_after')). + ** apply find_some in E. + destr E. + eapply eqb_eq in H4. + symmetry in H4. + subst. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ++ destr (find (eqb y) (v :: List.removeb eqb x used_after')). + ** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + auto using subset_diff. + -- rewrite of_list_cons. + unfold add. + eapply subset_union_l. + ++ destr (find (eqb v) (List.removeb eqb x used_after')). + ** destr (find (eqb y) (List.removeb eqb x used_after')). + --- apply find_some in E1. + destr E1. + apply eqb_eq in H2. + symmetry in H2. + subst. + auto using in_singleton. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ** destr (find (eqb y) (v :: List.removeb eqb x used_after')). + --- apply find_some in E1. + destr E1. + apply eqb_eq in H2. + symmetry in H2. + subst. + eauto using in_singleton. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ++ destr (find (eqb v) (List.removeb eqb x used_after')). + ** destr (find (eqb y) (List.removeb eqb x used_after')). + --- repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ** destr (find (eqb y) (v :: List.removeb eqb x used_after')). + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + auto using subset_diff. + * destr (find (eqb y) (v :: List.removeb eqb x used_after)). + ++ rewrite of_list_cons. + unfold add. + eapply subset_union_l. + ** destr (find (eqb v) (List.removeb eqb x used_after')). + --- eapply find_some in E1. + destr E1. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb y) (List.removeb eqb x used_after')). + +++ eauto using in_singleton. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + eauto using in_singleton. + --- destr (find (eqb y) (v :: List.removeb eqb x used_after')). + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ** destr (find (eqb v) (List.removeb eqb x used_after')). + --- eapply find_some in E1. + destr E1. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb y) (List.removeb eqb x used_after')). + +++ repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + --- destr (find (eqb y) (v :: List.removeb eqb x used_after')). + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ++ rewrite of_list_cons. + unfold add. + eapply subset_union_l. + ** destr (find (eqb v) (List.removeb eqb x used_after')). + --- destr (find (eqb y) (List.removeb eqb x used_after')). + +++ apply find_some in E2. + destr E2. + apply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + --- destr (find (eqb y) (v :: List.removeb eqb x used_after')). + +++ apply find_some in E2. + destr E2. + apply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ** destr (find (eqb v) (List.removeb eqb x used_after')). + --- apply find_some in E1. + destr E1. + apply eqb_eq in H1. + symmetry in H1. + subst. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + +++ destr (find (eqb y) (List.removeb eqb x used_after')). + *** eauto using in_singleton. + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + eauto using in_singleton. + +++ destr (find (eqb y) (List.removeb eqb x used_after')). + *** repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + --- rewrite of_list_cons. + unfold add. + apply subset_union_l. + +++ destr (find (eqb y) (v :: List.removeb eqb x used_after')). + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + apply subset_ref. + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + apply subset_ref. + +++ destr (find (eqb y) (v :: List.removeb eqb x used_after')). + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + + simpl. + destr (find (eqb y) (List.removeb eqb x used_after)). + * apply find_some in E. + destr E. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb y) (List.removeb eqb x used_after')). + -- repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + -- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + * rewrite of_list_cons. + unfold add. + apply subset_union_l. + -- destr (find (eqb y) (List.removeb eqb x used_after')). + ++ apply find_some in E0. + destr E0. + apply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + -- destr (find (eqb y) (List.removeb eqb x used_after')). + ++ repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SSet *) + simpl. + destr (find (eqb y) (List.removeb eqb x used_after)). + + destr (find (eqb y) (List.removeb eqb x used_after')). + * repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + * rewrite of_list_cons. + unfold add. + apply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + + rewrite of_list_cons. + unfold add. + apply subset_union_l. + * destr (find (eqb y) (List.removeb eqb x used_after')). + -- apply find_some in E0. + destr E0. + apply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + -- rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + * destr (find (eqb y) (List.removeb eqb x used_after')). + -- repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + -- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SIf *) + simpl. + repeat rewrite ListSet.of_list_list_union. + repeat apply subset_union_l. + + apply subset_union_rl. + apply subset_union_rl. + eauto. + + apply subset_union_rl. + apply subset_union_rr. + eauto. + + apply subset_union_rr. + eapply subset_ref. + - (* SLoop *) + simpl. eapply IHs1. + repeat rewrite ListSet.of_list_list_union. + repeat apply subset_union_l. + + apply subset_union_rl. + eapply subset_ref. + + apply subset_union_rr. + apply subset_union_rl. + eauto. + + apply subset_union_rr. + apply subset_union_rr. + apply subset_ref. + - (* SSeq *) + simpl. + eauto. + - (* SSkip *) + simpl. + auto. + - (* SCall *) + simpl. + repeat rewrite ListSet.of_list_list_union. + apply subset_union_l. + + apply subset_union_rl. + apply subset_ref. + + apply subset_union_rr. all: admit. Admitted. diff --git a/compiler/src/compiler/DeadAssignmentHelper.v b/compiler/src/compiler/DeadAssignmentHelper.v index 5ee73f8b..7d0c4c80 100644 --- a/compiler/src/compiler/DeadAssignmentHelper.v +++ b/compiler/src/compiler/DeadAssignmentHelper.v @@ -286,4 +286,15 @@ Section WithArguments. subst. propositional idtac. Qed. + + Lemma of_list_list_diff: + forall l1 l2 : list string, + of_list (ListSet.list_diff eqb l1 l2) = + diff (of_list l1) (of_list l2). + Proof. + intros. + induction l2. + - simpl. + Admitted. + End WithArguments. From 8f98d7ddd3bfa023ad39a9f1028cfed03b3442a7 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Thu, 18 May 2023 11:00:06 -0400 Subject: [PATCH 08/14] more progress on possible correctness lemma --- compiler/src/compiler/DeadAssignment.v | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index d5f94d6d..7e5a44ba 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -890,8 +890,19 @@ Section WithArguments. } { simpl. intros. eapply @exec.loop; eauto. - (* exec.loop *) - all: admit. + - eapply @exec.weaken. + + eapply IHexec. + admit. + + admit. + - intros. eapply H2 in H8. + 2: eassumption. + repeat eexists. + eapply H8. + - intros. eapply H4 in H8. + 2: eassumption. + + eapply H8. + + admit. + - admit. } { simpl. intros. From 0c406a2ad3bda8010f6d71417716cd4f8ad0b54d Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Sun, 21 May 2023 02:49:42 -0400 Subject: [PATCH 09/14] temp commit, redefined helper lemma --- compiler/src/compiler/DeadAssignment.v | 55 ++++++++++++++++++++------ 1 file changed, 44 insertions(+), 11 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index 7e5a44ba..b4ad3af6 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -21,7 +21,11 @@ Section WithArguments. Context {ext_spec : Semantics.ExtSpec} {ext_spec_ok: Semantics.ext_spec.ok ext_spec}. Local Hint Constructors exec: core. - + Create HintDb set_hints. + Hint Resolve + subset_diff + in_singleton + subset_union_rr : set_hints. Lemma live_monotone : forall s used_after used_after', subset (of_list used_after) (of_list used_after') -> @@ -58,7 +62,8 @@ Section WithArguments. destr E0. eapply eqb_eq in H1. subst. - eauto using in_singleton. + eauto with set_hints. + -- rewrite of_list_cons. unfold add. eapply subset_union_rl. eapply subset_ref. @@ -72,6 +77,15 @@ Section WithArguments. eauto using subset_diff. - (* SStore *) simpl. + (* destruct_one_match *) + repeat match goal with + | |- context[if ?c then _ else _] => + lazymatch c with + | context[if ?c' then _ else _] => fail + | _ => destr c + end + end. + destruct_one_match. destr (find (eqb v) used_after). + eapply find_some in E. destr E. @@ -775,23 +789,37 @@ Section WithArguments. all: admit. Admitted. + Definition compile_post used_after (postH : Semantics.trace -> mem -> locals -> MetricLog -> Prop) : (Semantics.trace -> mem -> locals -> MetricLog -> Prop) := + (fun t' m' lL' mcL' => + exists lH' mcH', + map.agree_on (PropSet.of_list used_after) lH' lL' + /\ postH t' m' lH' mcH' ). Lemma deadassignment_correct_aux: forall eH eL, deadassignment_functions eH = Success eL -> forall sH t m mcH lH postH, exec eH sH t m lH mcH postH -> - forall used_after lL, + forall used_after lL mcL, map.agree_on (of_list (live (deadAssignment used_after sH) used_after)) lH lL - -> exec eL (deadAssignment used_after sH) t m lH mcH - (fun t' m' lL' mcL' => - exists lH' mcH', - map.agree_on (PropSet.of_list used_after) lH' lL' - /\ postH t' m' lH' mcH' ). + -> exec eL (deadAssignment used_after sH) t m lL mcL (compile_post used_after postH). Proof. induction 2. + 13: { + intros. + simpl. + eapply @exec.seq with (mid := compile_post (live (deadAssignment used_after s2) used_after) mid). + - eapply IHexec. simpl in H3. eapply H3. + - intros. unfold compile_post in H4. fwd. + eapply H2. + + eapply H4p1. + + eapply H4p0. + } + Proof. + induction 2; unfold compile_post in *; simpl. { simpl. intros. eapply @exec.interact; eauto. + eauto. intros. apply H3 in H5. destruct H5. destruct H5. eexists. split. @@ -906,15 +934,17 @@ Section WithArguments. } { simpl. intros. - eapply @exec.seq. + eapply @exec.seq with (mid := compile_post (live (deadAssignment used_after s2) used_after) mid). - (* specialize (IHexec (live s2 used_after)). specialize IHexec with (1 := H3). apply IHexec in H3. eapply IHexec. *) eapply IHexec. - eapply agree_on_subset. + eapply H3. + (* eapply agree_on_subset. + + eapply H3. *) + (* + admit. (* eapply live_monotone. *) (* replace (live sH used_after) with (live sH used_after') where subset used_after used_after' @@ -926,9 +956,12 @@ Section WithArguments. forall s1 u u', subset u u' -> subset (of_list (live s1 u)) (of_list live s1 u') *) - +*) - simpl. intros. + unfold compile_post in H4. + fwd. eapply H2. + (* context has that there exists some lH' and mcH', but goal has that a specific lH and mcH that satisfy mid eexists. eexists. From a326f090100e27e6d36d6f8fae757a28aedcb002 Mon Sep 17 00:00:00 2001 From: Arthur De Belen <55215987+0adb@users.noreply.github.com> Date: Mon, 22 May 2023 01:17:19 -0400 Subject: [PATCH 10/14] Comment out large section of possibly unnecessary proof --- compiler/src/compiler/DeadAssignment.v | 384 +++++++++++++------------ 1 file changed, 195 insertions(+), 189 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index b4ad3af6..30fed792 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -26,7 +26,201 @@ Section WithArguments. subset_diff in_singleton subset_union_rr : set_hints. - Lemma live_monotone : + + Definition compile_post used_after (postH : Semantics.trace -> mem -> locals -> MetricLog -> Prop) : (Semantics.trace -> mem -> locals -> MetricLog -> Prop) := + (fun t' m' lL' mcL' => + exists lH' mcH', + map.agree_on (PropSet.of_list used_after) lH' lL' + /\ postH t' m' lH' mcH' ). + Lemma deadassignment_correct_aux: + forall eH eL, + deadassignment_functions eH = Success eL -> + forall sH t m mcH lH postH, + exec eH sH t m lH mcH postH -> + forall used_after lL mcL, + map.agree_on (of_list (live (deadAssignment used_after sH) used_after)) lH lL + -> exec eL (deadAssignment used_after sH) t m lL mcL (compile_post used_after postH). + Proof. + induction 2. + 13: { + intros. + simpl. + eapply @exec.seq with (mid := compile_post (live (deadAssignment used_after s2) used_after) mid). + - eapply IHexec. simpl in H3. eapply H3. + - intros. unfold compile_post in H4. fwd. + eapply H2. + + eapply H4p1. + + eapply H4p0. + } + Proof. + induction 2; unfold compile_post in *; simpl. + { simpl. + intros. + eapply @exec.interact; eauto. + eauto. + intros. apply H3 in H5. + destruct H5. destruct H5. + eexists. split. + all: eauto using agree_on_refl. + } + { simpl. intros. + eapply @exec.call. + * unfold deadassignment_functions in H. + unfold deadassignment_function in H. + simpl in H. + eapply map.try_map_values_fw in H. + 2: { eapply H0. } + destruct H. + destruct H. + inversion H. + rewrite <- H8 in H6. + apply H6. + * eassumption. + * eassumption. + * eapply IHexec. apply agree_on_refl. + * intros. destruct H6. destruct H6. + destruct H6. eapply H4 in H7. + destruct H7. destruct H7. + destruct H7. destruct H8. + eexists. eexists. + split. + -- eapply agree_on_getmany in H6. + rewrite <- H6. + eassumption. + -- split. + ++ eapply H8. + ++ eexists. eexists. + split. + 2: eapply H9. + eapply agree_on_refl. + + } + { simpl. intros. + eapply @exec.load; eauto. + destr (find (eqb a) (List.removeb eqb x used_after)). + all: eauto using agree_on_refl. + } + { simpl. intros. + destr (find (eqb v) used_after). + - destr (find (eqb a) used_after); eauto using agree_on_refl. + - destr (find (eqb a) (v :: used_after)); eauto using agree_on_refl. + } + { simpl. intros. + eauto using agree_on_refl. + } + { simpl. intros. + all: eauto using agree_on_refl. + apply @exec.stackalloc; auto. + simpl. intros. + eapply @exec.weaken. + -- eauto using agree_on_refl. + -- simpl. intros. + propositional idtac. + } + { simpl. intros. + destr (existsb (eqb x) used_after). + all: eauto 6 using agree_on_refl, agree_on_not_in. + } + { simpl. intros. + destr (existsb (eqb x) used_after). + all: eauto 6 using agree_on_refl, agree_on_not_in. + } + { simpl; eauto. + intros. destr (existsb (eqb x) used_after). + all: eauto 6 using agree_on_refl, agree_on_not_in. + } + { simpl. intros. + eapply @exec.if_true; eauto. + eapply IHexec. + eapply agree_on_subset. + -- eapply H2. + -- unfold subset. intros. + rewrite ListSet.of_list_list_union. + apply in_union_l. + rewrite ListSet.of_list_list_union. + apply in_union_l. + assumption. + } + { simpl. intros. + eapply @exec.if_false; eauto. + eapply IHexec. + all: eauto. + eapply agree_on_subset. + -- eapply H2. + -- unfold subset. intros. + rewrite ListSet.of_list_list_union. + apply in_union_l. + rewrite ListSet.of_list_list_union. + apply in_union_r. + assumption. + } + { simpl. intros. + eapply @exec.loop; eauto. + - eapply @exec.weaken. + + eapply IHexec. + admit. + + admit. + - intros. eapply H2 in H8. + 2: eassumption. + repeat eexists. + eapply H8. + - intros. eapply H4 in H8. + 2: eassumption. + + eapply H8. + + admit. + - admit. + } + { simpl. + intros. + eapply @exec.seq with (mid := compile_post (live (deadAssignment used_after s2) used_after) mid). + - (* specialize (IHexec (live s2 used_after)). + specialize IHexec with (1 := H3). + apply IHexec in H3. + eapply IHexec. *) + + eapply IHexec. + + eapply H3. + (* eapply agree_on_subset. + + eapply H3. *) + (* + + admit. (* eapply live_monotone. *) + (* replace (live sH used_after) with (live sH used_after') + where subset used_after used_after' + *) + + (* show that + of_list (live (deadAss used_after s2) used_after) + is subset of (live s2 used_after), and that + forall s1 u u', + subset u u' -> + subset (of_list (live s1 u)) (of_list live s1 u') *) +*) + - simpl. intros. + unfold compile_post in H4. + fwd. + eapply H2. + + (* context has that there exists some lH' and mcH', + but goal has that a specific lH and mcH that satisfy mid + eexists. eexists. + all: eauto. + all: ad mit. + exec.seq *) + all: admit. + } + { simpl. + intros. + eapply @exec.skip; eauto. + eexists. eexists. + split. + 2: eassumption. + apply agree_on_refl. + } + Admitted. + +End WithArguments. +(* + Lemma live_monotone : forall s used_after used_after', subset (of_list used_after) (of_list used_after') -> subset (of_list (live s used_after)) (of_list (live s used_after')). @@ -789,194 +983,6 @@ Section WithArguments. all: admit. Admitted. - Definition compile_post used_after (postH : Semantics.trace -> mem -> locals -> MetricLog -> Prop) : (Semantics.trace -> mem -> locals -> MetricLog -> Prop) := - (fun t' m' lL' mcL' => - exists lH' mcH', - map.agree_on (PropSet.of_list used_after) lH' lL' - /\ postH t' m' lH' mcH' ). - Lemma deadassignment_correct_aux: - forall eH eL, - deadassignment_functions eH = Success eL -> - forall sH t m mcH lH postH, - exec eH sH t m lH mcH postH -> - forall used_after lL mcL, - map.agree_on (of_list (live (deadAssignment used_after sH) used_after)) lH lL - -> exec eL (deadAssignment used_after sH) t m lL mcL (compile_post used_after postH). - Proof. - induction 2. - 13: { - intros. - simpl. - eapply @exec.seq with (mid := compile_post (live (deadAssignment used_after s2) used_after) mid). - - eapply IHexec. simpl in H3. eapply H3. - - intros. unfold compile_post in H4. fwd. - eapply H2. - + eapply H4p1. - + eapply H4p0. - } - Proof. - induction 2; unfold compile_post in *; simpl. - { simpl. - intros. - eapply @exec.interact; eauto. - eauto. - intros. apply H3 in H5. - destruct H5. destruct H5. - eexists. split. - all: eauto using agree_on_refl. - } - { simpl. intros. - eapply @exec.call. - * unfold deadassignment_functions in H. - unfold deadassignment_function in H. - simpl in H. - eapply map.try_map_values_fw in H. - 2: { eapply H0. } - destruct H. - destruct H. - inversion H. - rewrite <- H8 in H6. - apply H6. - * eassumption. - * eassumption. - * eapply IHexec. apply agree_on_refl. - * intros. destruct H6. destruct H6. - destruct H6. eapply H4 in H7. - destruct H7. destruct H7. - destruct H7. destruct H8. - eexists. eexists. - split. - -- eapply agree_on_getmany in H6. - rewrite <- H6. - eassumption. - -- split. - ++ eapply H8. - ++ eexists. eexists. - split. - 2: eapply H9. - eapply agree_on_refl. - - } - { simpl. intros. - eapply @exec.load; eauto. - destr (find (eqb a) (List.removeb eqb x used_after)). - all: eauto using agree_on_refl. - } - { simpl. intros. - destr (find (eqb v) used_after). - - destr (find (eqb a) used_after); eauto using agree_on_refl. - - destr (find (eqb a) (v :: used_after)); eauto using agree_on_refl. - } - { simpl. intros. - eauto using agree_on_refl. - } - { simpl. intros. - all: eauto using agree_on_refl. - apply @exec.stackalloc; auto. - simpl. intros. - eapply @exec.weaken. - -- eauto using agree_on_refl. - -- simpl. intros. - propositional idtac. - } - { simpl. intros. - destr (existsb (eqb x) used_after). - all: eauto 6 using agree_on_refl, agree_on_not_in. - } - { simpl. intros. - destr (existsb (eqb x) used_after). - all: eauto 6 using agree_on_refl, agree_on_not_in. - } - { simpl; eauto. - intros. destr (existsb (eqb x) used_after). - all: eauto 6 using agree_on_refl, agree_on_not_in. - } - { simpl. intros. - eapply @exec.if_true; eauto. - eapply IHexec. - eapply agree_on_subset. - -- eapply H2. - -- unfold subset. intros. - rewrite ListSet.of_list_list_union. - apply in_union_l. - rewrite ListSet.of_list_list_union. - apply in_union_l. - assumption. - } - { simpl. intros. - eapply @exec.if_false; eauto. - eapply IHexec. - all: eauto. - eapply agree_on_subset. - -- eapply H2. - -- unfold subset. intros. - rewrite ListSet.of_list_list_union. - apply in_union_l. - rewrite ListSet.of_list_list_union. - apply in_union_r. - assumption. - } - { simpl. intros. - eapply @exec.loop; eauto. - - eapply @exec.weaken. - + eapply IHexec. - admit. - + admit. - - intros. eapply H2 in H8. - 2: eassumption. - repeat eexists. - eapply H8. - - intros. eapply H4 in H8. - 2: eassumption. - + eapply H8. - + admit. - - admit. - } - { simpl. - intros. - eapply @exec.seq with (mid := compile_post (live (deadAssignment used_after s2) used_after) mid). - - (* specialize (IHexec (live s2 used_after)). - specialize IHexec with (1 := H3). - apply IHexec in H3. - eapply IHexec. *) - eapply IHexec. - + eapply H3. - (* eapply agree_on_subset. - + eapply H3. *) - (* - + admit. (* eapply live_monotone. *) - (* replace (live sH used_after) with (live sH used_after') - where subset used_after used_after' - *) - (* show that - of_list (live (deadAss used_after s2) used_after) - is subset of (live s2 used_after), and that - forall s1 u u', - subset u u' -> - subset (of_list (live s1 u)) (of_list live s1 u') *) *) - - simpl. intros. - unfold compile_post in H4. - fwd. - eapply H2. - - (* context has that there exists some lH' and mcH', - but goal has that a specific lH and mcH that satisfy mid - eexists. eexists. - all: eauto. - all: ad mit. - exec.seq *) - all: admit. - } - { simpl. - intros. - eapply @exec.skip; eauto. - eexists. eexists. - split. - 2: eassumption. - apply agree_on_refl. - } - Admitted. -End WithArguments. From 961bdc7be4ae02b4d11d1eb6a7d8b34f7d7a5539 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Wed, 28 Jun 2023 15:07:52 -0400 Subject: [PATCH 11/14] progress update commit (automating deadassignment proof) --- compiler/src/compiler/DeadAssignment.v | 606 ++++++++++++++++++- compiler/src/compiler/DeadAssignmentHelper.v | 321 +++++++++- 2 files changed, 924 insertions(+), 3 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index 30fed792..e1ba5df2 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -26,7 +26,7 @@ Section WithArguments. subset_diff in_singleton subset_union_rr : set_hints. - + Definition compile_post used_after (postH : Semantics.trace -> mem -> locals -> MetricLog -> Prop) : (Semantics.trace -> mem -> locals -> MetricLog -> Prop) := (fun t' m' lL' mcL' => exists lH' mcH', @@ -42,6 +42,608 @@ Section WithArguments. -> exec eL (deadAssignment used_after sH) t m lL mcL (compile_post used_after postH). Proof. induction 2. + - simpl. + intros. + eapply @exec.interact; fwd. + + match goal with + | H: map.split ?m _ _ |- map.split m _ _ => eapply H + end. + + match goal with + | H1: map.getmany_of_list ?l ?argvars = Some ?argvals, + H2: map.agree_on _ ?l ?lL + |- map.getmany_of_list ?lL ?argvars = Some ?y => + cut (map.getmany_of_list l argvars = map.getmany_of_list lL argvars); + intros; + match goal with + | H: map.getmany_of_list l argvars + = map.getmany_of_list lL argvars + |- map.getmany_of_list lL argvars = Some _ => + rewrite <- H; eassumption + | |- map.getmany_of_list l argvars + = map.getmany_of_list lL argvars => + eapply agree_on_getmany; eapply agree_on_subset; + [ eapply H2 | ] + end + end. + repeat match goal with + | |- context[of_list (ListSet.list_union _ _ _)] => rewrite ListSet.of_list_list_union + | |- context[ListSet.list_diff] => rewrite of_list_list_diff + end. + match goal with + | |- subset ?x (union ?x ?y) => + eapply subset_union_rl; eapply subset_ref + end. + + match goal with + | |- ext_spec _ _ _ _ _ => eassumption + end. + + intros. + match goal with + | H: outcome ?mReceive ?resvals, + H1: forall mReceive resvals, + outcome mReceive resvals -> _ |- _ => + apply H1 in H; + repeat match goal with + | H: exists l, _ |- _ => destr H + | H: _ /\ _ |- _ => destr H + end + end. + match goal with + | H: map.putmany_of_list_zip ?resvars ?resvals _ = _ |- + exists l, + map.putmany_of_list_zip resvars resvals _ = Some _ /\ _ + => + let Heq := fresh in + pose proof H as Heq; eapply putmany_Some in H; destr H + end. + match goal with + | H: map.putmany_of_list_zip _ _ _ = Some ?x0 |- _ => eexists x0; split; [ eapply H | ] + end. + match goal with + | |- forall m', map.split m' mKeep mReceive -> _ + => intros + end. + match goal with + | H: map.split ?m ?mKeep ?mReceive, + H': forall m', + map.split m' mKeep mReceive -> _ + |- _ => eapply H' in H + end. + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m' ?x _ |- exists lH' mcH', + map.agree_on _ lH' _ /\ + (post _ _ lH' _) => + exists x; eexists; split; [ | eapply H ] + end. + (* miscellaneous set reasoning; + unclear how to automate this across cases *) + repeat match goal with + | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H + | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H + end. + match goal with + | H: map.agree_on (union _ _) _ _ |- _ => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on (diff (of_list ?l1) (of_list ?l2)) ?l ?lL + |- _ => + match goal with + | H': map.putmany_of_list_zip l2 ?v l = Some ?x |- _ => + match goal with + | H'': map.putmany_of_list_zip l2 v lL = Some ?x0 + |- map.agree_on (of_list l1) x x0 => + eapply agree_on_subset; + [ eauto using agree_on_putmany + | eapply subset_trans; + [ eapply subset_union_rl; eapply subset_ref + | eapply sameset_union_diff_oflist ] + ] + end + end + end. + - simpl. + intros. + eapply @exec.call; fwd. + + match goal with + | H: deadassignment_functions ?eH = Success ?eL, + H1: map.get eH ?fname = Some ?x |- + map.get eL fname = Some _ => + unfold deadassignment_functions in H; + unfold deadassignment_function in H; + eapply map.try_map_values_fw in H; [ | eapply H1 ]; + repeat (destr H; simpl in H) + end. + match goal with + | H: Success _ = Success ?x, + H1: map.get ?eL ?fname = Some x + |- map.get eL fname = Some _ + => inversion H; fwd; eapply H1 + end. + + match goal with + | H: map.getmany_of_list ?l ?args = Some ?argvs + |- map.getmany_of_list lL args = Some _ => + replace (map.getmany_of_list lL args) with (map.getmany_of_list l args); [ eapply H | ] + end. + match goal with + | H: map.agree_on ?s ?l ?lL + |- map.getmany_of_list l ?args + = map.getmany_of_list lL ?args + => eapply agree_on_getmany; + eapply agree_on_subset; [ eapply H | ] + end. + (* set reasoning *) + repeat match goal with + | |- context[of_list (ListSet.list_union _ _ _)] => rewrite ListSet.of_list_list_union + | |- context[ListSet.list_diff] => rewrite of_list_list_diff + end. + match goal with + | |- subset ?x (union ?x ?y) => + eapply subset_union_rl; eapply subset_ref + end. + + match goal with + | |- map.putmany_of_list_zip _ _ _ = Some _ => eassumption + end. + + match goal with + | |- exec _ _ _ _ _ _ _ => eauto using agree_on_refl + end. + + match goal with + | |- forall t' m' mc' st1, + compile_post ?rets ?outcome t' m' st1 mc' -> _ + => unfold compile_post; intros; fwd + end. + + match goal with + | H: outcome _ _ _ _, + H1: forall t' m' mc' st1, + outcome _ _ _ _ -> + exists retvs l', + map.getmany_of_list st1 ?rets = Some retvs /\ _ + |- _ => eapply H1 in H; fwd + end. + + match goal with + | H: map.putmany_of_list_zip ?binds ?x1 ?l = Some ?x2, + H1: map.agree_on _ l ?lL + |- context[map.putmany_of_list_zip ?binds _ ?lL] => + let Heq := fresh in + pose proof H as Heq; eapply putmany_Some in H; destr H; fwd + end. + + match goal with + | H: map.agree_on (of_list ?rets) ?lH' ?st1, + H1: map.getmany_of_list ?lH' ?rets = Some ?retvs, + H2: map.putmany_of_list_zip ?binds ?retvs _ = Some ?x |- + exists retvs0 l'0, + map.getmany_of_list st1 rets = Some retvs0 /\ _ + => exists retvs; exists x; repeat split; [ | eapply H2 | ] + end. + * match goal with + | H: map.agree_on (of_list ?rets) ?lH' ?st1, + H1: map.getmany_of_list ?lH' ?rets = Some ?retvs + |- map.getmany_of_list ?st1 ?rets = Some ?retvs + => apply agree_on_getmany in H; rewrite <- H; eapply H1 + end. + * match goal with + | H: post ?t' ?m' ?l' _ + |- exists lH'0 mcH'0, + map.agree_on (of_list ?used_after) lH'0 ?x /\ + post ?t' ?m' lH'0 mcH'0 + => exists l'; eexists; split; [ | eapply H ] + end. + repeat match goal with + | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H + | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H + end. + match goal with + | H: map.agree_on (union _ _) ?l ?lL + |- _ => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on (diff (of_list ?used_after) (of_list ?binds)) ?l ?lL, + H1: map.putmany_of_list_zip binds ?retvs l = Some ?l', + H2: map.putmany_of_list_zip binds retvs lL = Some ?x + |- map.agree_on (of_list used_after) l' x + => eapply agree_on_subset; + [ eauto using agree_on_putmany | + eapply subset_trans; + [ eapply subset_union_rl; eapply subset_ref | + eapply sameset_union_diff_oflist ] + ] + end. + - simpl. + intros. + match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ => + apply agree_on_find in H; destr H + end. + eapply @exec.load; fwd. + + match goal with + | H: map.agree_on (of_list [?a]) ?l ?lL, + H1: map.get ?l ?a = Some ?addr |- + map.get ?lL ?a = Some _ => rewrite <- H; [ eassumption | ] + end. + match goal with + | |- ?s \in of_list [?s] => cut (of_list [s] s); [ simpl; intro; auto | unfold of_list; simpl; auto ] + end. + + match goal with + | H: Memory.load _ _ _ = Some _ |- Memory.load _ _ _ = Some _ => eapply H + end. + + match goal with + | |- compile_post _ _ _ _ _ _ => unfold compile_post + end. + match goal with + | H: post ?t m (map.put ?l ?x ?v) _, + H1: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list used_after) lH' + (map.put lL x v) /\ + post t m lH' mcH' + => exists (map.put l x v); eexists; split; [ | ] ; + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) _ |- post t m (map.put l x v) _ => eapply H + | |- _ => idtac + end + end. + + match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list used_after) (map.put ?l ?x ?v) (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; + eapply agree_on_subset; + match goal with + | |- map.agree_on _ (map.put l x v) (map.put lL x v) + => eapply agree_on_put; + match goal with + | |- map.put _ _ _ = map.put _ _ _ => reflexivity + | |- _ => idtac + end; + match goal with + | |- map.agree_on _ l lL => eapply H + end + (* Note that order matters in execution of these two tactics, ^ which is why they aren't in the same match-goal *) + | |- _ => idtac + end + end. + + match goal with + | |- subset (of_list ?s) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + - simpl. intros. + repeat match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ + => apply agree_on_find in H; destr H + end. + eapply @exec.store; fwd. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | |- Memory.store _ _ (word.add _ _) _ = Some _ => eassumption + end. + + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: map.agree_on ?s ?l ?lL, + H1: post ?t ?m' ?l ?mcH' + |- exists lH' mcH', + map.agree_on ?s lH' ?lL /\ + post ?t ?m' lH' mcH' + => exists l; eexists; split; [ eapply H | eapply H1 ] + end. + - simpl. intros. + match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ => + apply agree_on_find in H; destr H + end. + eapply @exec.inlinetable. + + match goal with + | |- ?x <> ?i => assumption + end. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | |- Memory.load _ (OfListWord.map.of_list_word _) _ = Some _ => eassumption + end. + + (* Note for further automation: + this goal's proof is exactly lifted from + the exec.load case's corresponding goal. *) + + match goal with + | |- context[compile_post] => unfold compile_post + end. + + match goal with + | H: post ?t m (map.put ?l ?x ?v) _, + H1: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list used_after) lH' + (map.put lL x v) /\ + post t m lH' mcH' + => exists (map.put l x v); eexists; split; [ | ] ; + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) _ |- post t m (map.put l x v) _ => eapply H + | |- _ => idtac + end + end. + match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list used_after) (map.put ?l ?x ?v) (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; + eapply agree_on_subset; + match goal with + | |- map.agree_on _ (map.put l x v) (map.put lL x v) + => eapply agree_on_put; + match goal with + | |- map.put _ _ _ = map.put _ _ _ => reflexivity + | |- _ => idtac + end; + match goal with + | |- map.agree_on _ l lL => eapply H + end + (* Note that order matters in execution of these two tactics, ^ which is why they aren't in the same match-goal *) + | |- _ => idtac + end + end. + + match goal with + | |- subset (of_list ?s) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + + - simpl. + intros. + eapply @exec.stackalloc. + + match goal with + | |- ?n mod Memory.bytes_per_word ?width = 0 => assumption + end. + + (* For complicated goals like this, + unsure how sound automation will be. *) + match goal with + | |- forall a mStack mCombined, + Memory.anybytes a ?n mStack -> + map.split mCombined ?mSmall mStack -> + exec _ _ _ mCombined _ _ _ + => intros + end. + match goal with + | H: context[exec _ (deadAssignment _ _) _ _ _ _ _], + H1: Memory.anybytes _ _ _, + H2: map.agree_on (of_list (List.removeb eqb ?x ?l')) ?l ?lL |- exec _ (deadAssignment _ _) _ _ (map.put ?lL ?x ?a) _ _ => + eapply H with (lL := map.put lL x a) in H1 + end. + all: try match goal with + | H: map.split _ ?mSmall ?mStack |- + map.split _ ?mSmall ?mStack => eapply H + end. + all: try match goal with + | |- map.agree_on + _ (map.put ?l ?x ?a) (map.put ?lL ?x ?a) + => eapply agree_on_subset; + match goal with + | |- map.agree_on _ (map.put ?l ?x ?a) + (map.put ?lL ?x ?a) => + eapply agree_on_put; + match goal with + | |- map.put _ _ _ = map.put _ _ _ + => reflexivity + | |- map.agree_on _ ?l ?lL => eassumption + end + | |- subset _ _ => idtac + end + end. + all: try match goal with + | |- subset _ (union (of_list (List.removeb eqb ?x ?l)) (singleton_set ?x)) => rewrite ListSet.of_list_removeb + end. + (* Copy pasted from earlier, + but this time the left argument to subset is unspecified + *) + all: try match goal with + | |- subset (of_list _) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + match goal with + | H: exec ?eL ?s ?t ?m ?l _ ?post |- exec ?eL ?s ?t ?m ?l _ ?post' => eapply exec.weaken; [ eapply H | simpl ] + end. + match goal with + | |- context[compile_post] => + unfold compile_post; simpl; intros; fwd + end. + match goal with + | H: Memory.anybytes ?a ?n ?mStack', + H1: map.split ?m' ?mSmall' ?mStack', + H2: post ?t' ?mSmall' ?lH' ?mcH', + H3: map.agree_on (of_list ?used_after) ?lH' ?l' + |- exists mSmall'1 mStack'1, + Memory.anybytes ?a ?n mStack'1 /\ + map.split ?m' mSmall'1 mStack'1 /\ + (exists lH'0 mcH'0, + map.agree_on (of_list ?used_after) lH'0 ?l' /\ + post ?t' mSmall'1 lH'0 mcH'0) => + exists mSmall'; exists mStack'; propositional idtac + end. + - simpl. intros. + destr (existsb (eqb x) used_after). + + eapply @exec.lit. + unfold compile_post. + exists (map.put l x (word.of_Z v)). + eexists. + propositional idtac. + * simpl in *. + eapply agree_on_subset. + -- eapply agree_on_put. + 2-3: reflexivity. + eapply H1. + -- rewrite ListSet.of_list_removeb. + try match goal with + | |- subset (of_list _) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + * eapply H0. + + eapply @exec.skip. + unfold compile_post. + simpl in *. + eexists (map.put l x (word.of_Z v)). + eexists. + split. + + repeat eexists. + eapply H0. + + exists mSmall'. + exists mStack'. + propositional idtac. + fwd. + eapply exec.weaken. + * eapply H4. + * unfold compile_post. + simpl. intros. + fwd. + exists mSmall'. + exists mStack'. + propositional idtac. + - + Search @exec.exec. + + + + + 2: { eapply agree_on_put. + + eapply H2 in H4. + 2: eassumption. + * eapply H4. + eaply H2. + match goal with + | H: _ -> exec ?eL (deadAssignment ?used_After + + + * eassumption. + * eapply agree_on_getmany. + eapply agree_on_subset; [ eapply H4 | ]. + rewrite ListSet.of_list_list_union. + eapply subset_union_rl. + eapply subset_ref. + + eassumption. + + unfold compile_post. + intros. + eapply H3 in H5. + destr H5. + destr H5. + pose proof H5 as H5'. + eapply putmany_Some in H5'. + destr H5'. + eexists x0. + split; [ eapply H7 | ]. + intros. + eapply H6 in H8. + exists x. + eexists. + split. + 2: eapply H8. + rewrite ListSet.of_list_list_union in H4. + rewrite of_list_list_diff in H4. + apply agree_on_union in H4. + destr H4. + eapply agree_on_subset; + [ eauto using agree_on_putmany | ]. + eapply subset_trans. + 2: eapply sameset_union_diff. + eapply subset_union_rl. + eapply subset_ref. 13: { intros. simpl. @@ -219,7 +821,7 @@ Section WithArguments. Admitted. End WithArguments. -(* +(* Lemma live_monotone : forall s used_after used_after', subset (of_list used_after) (of_list used_after') -> diff --git a/compiler/src/compiler/DeadAssignmentHelper.v b/compiler/src/compiler/DeadAssignmentHelper.v index 7d0c4c80..cd1400e2 100644 --- a/compiler/src/compiler/DeadAssignmentHelper.v +++ b/compiler/src/compiler/DeadAssignmentHelper.v @@ -16,6 +16,66 @@ Section WithArguments. Context {word : word width } {word_ok : word.ok word}. Context {locals : map.map string word } {locals_ok: map.ok locals}. + Lemma putmany_Some' : + forall (lk: list string) lv (m: locals), + (exists m', map.putmany_of_list_zip lk lv m = Some m') + <-> Datatypes.length lk = Datatypes.length lv. + Proof. + induction lk. + - simpl. intros. destr lv. + + simpl. + unfold iff; split. + * intros. reflexivity. + * intros. eauto. + + simpl. + unfold iff; split. + * intros. destr H. discriminate. + * intros. discriminate. + - intros. destr lv. + + simpl. + unfold iff; split. + * intros. destr H. discriminate. + * intros. discriminate. + + simpl. + unfold iff; split. + * intros. apply eq_S. + eapply IHlk. + eapply H. + * intros. apply eq_add_S in H. + eapply IHlk in H. + eapply H. + Qed. + + Lemma putmany_Some: + forall (lk: list string) lv (m0: locals) m1, + map.putmany_of_list_zip lk lv m0 = Some m1 + -> (forall (m: locals), + (exists m', map.putmany_of_list_zip lk lv m = Some m')). + Proof. + intros. + eapply putmany_Some'. + eapply putmany_Some'. + eexists. + eapply H. + Qed. + + Lemma agree_on_union: + forall (s0 s1: set string) (m0 m1: locals), + map.agree_on (union s0 s1) m0 m1 + <-> map.agree_on s0 m0 m1 /\ map.agree_on s1 m0 m1. + Proof. + intros. + unfold iff; split. + - unfold map.agree_on in *. + split; intros; cut (s0 k \/ s1 k); auto. + - unfold map.agree_on in *. + intros. + destr H. + cut (s0 k \/ s1 k). + + intros. destr H2; auto. + + auto. + Qed. + Lemma agree_on_refl : forall keySet (m : locals), map.agree_on keySet m m. @@ -294,7 +354,266 @@ Section WithArguments. Proof. intros. induction l2. - - simpl. + (* PR for this lemma being proved in coqutil exists; + unsure how to prove it without the assumptions + in the file that ListSet.of_list_list_union + is proven in *) + Admitted. + + + Lemma agree_on_put: + forall a r s (mH mL: locals) mH' mL', + map.agree_on s mH mL -> + map.put mH a r = mH' -> + map.put mL a r = mL' -> + map.agree_on (union s (singleton_set a)) mH' mL'. + Proof. + intros. + apply agree_on_union. + split. + - unfold map.agree_on in *. + intros. + eapply H in H2. + subst. + destr (eqb a k). + + repeat rewrite map.get_put_same; reflexivity. + + repeat rewrite map.get_put_diff; eauto. + - unfold map.agree_on. + intros. + cut (a = k). + + intros. subst. + repeat rewrite map.get_put_same; reflexivity. + + assert (singleton_set a k) by auto. + unfold singleton_set in *; assumption. + Qed. + + Lemma union_sameset: + forall (s1 s2 s1' s2': set string), + sameset s1 s1' -> + sameset s2 s2' -> + sameset (union s1 s2) (union s1' s2'). + Proof. + intros. + unfold sameset, union. + split. + - unfold sameset, subset in *. + propositional idtac. + assert (x \in s1 \/ x \in s2) by auto. + cut (x \in s1' \/ x \in s2'); [ auto | ]. + destr H. + + left; eauto. + + right; eauto. + - unfold sameset, subset in *. + propositional idtac. + assert (x \in s1' \/ x \in s2') by auto. + cut (x \in s1 \/ x \in s2); [ auto | ]. + destr H. + + left; eauto. + + right; eauto. + Qed. + + Lemma agree_on_putmany: + forall (lk0: list string) lv s (mH mL: locals) mH' mL', + map.agree_on s mH mL -> + map.putmany_of_list_zip lk0 lv mH = Some mH' -> + map.putmany_of_list_zip lk0 lv mL = Some mL' -> + map.agree_on (union s (of_list lk0)) mH' mL'. + Proof. + induction lk0. + - intros. simpl in *. + destr lv; [ | discriminate ]. + apply agree_on_union. + split. + + inversion H0. + inversion H1. + subst; eauto. + + unfold map.agree_on. + intros. + cut (of_list [] k). + * unfold of_list. + intros. + exfalso. + eauto using in_nil. + * auto. + - intros. destr lv; [ discriminate | ]. + simpl in *. + cut (map.agree_on (union s (singleton_set a)) + (map.put mH a r) (map.put mL a r)). + + intros. + eapply IHlk0 in H2. + 2-3: eassumption. + eapply agree_on_sameset. + * eassumption. + * eapply sameset_trans. + 2: { eapply union_assoc. } + apply union_sameset; + [ eapply sameset_ref | eapply of_list_cons ]. + + eapply agree_on_put. + 2-3: reflexivity. + eassumption. + Qed. + + + Lemma sameset_union_diff_oflist: + forall (l1 l2: list string), + sameset (union (of_list l1) (of_list l2)) (union (diff (of_list l1) (of_list l2) ) (of_list l2)). + Proof. + intros. + unfold sameset, of_list, subset, union, diff. + + assert (forall x, In x l2 \/ ~ (In x l2)). + { intro. eapply ListDec.In_decidable. unfold ListDec.decidable_eq. + intros. destr (eqb x0 y). + - unfold Decidable.decidable. left. reflexivity. + - unfold Decidable.decidable. right. eassumption. + } + + split. + - intros. + cut ((fun x : string => + x \in (fun e : string => In e l1) \/ + x \in (fun e : string => In e l2)) x); [ simpl; intro | auto ]. + cut ((In x l1) \/ (In x l2)); [ simpl; intro | auto ]. + cut ((fun x0 : string => + x0 \in + (fun x1 : string => + x1 \in (fun e : string => In e l1) /\ + ~ x1 \in (fun e : string => In e l2)) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + assert (In x l2 \/ ~ In x l2) by eapply H. + destr H3. + + right. auto. + + propositional idtac. left. + cut ((fun x1 : string => + x1 \in (fun e : string => In e l1) /\ + ~ x1 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + split; auto. + - intros. + cut ((fun x : string => + x \in + (fun x0 : string => + x0 \in (fun e : string => In e l1) /\ + ~ x0 \in (fun e : string => In e l2)) \/ + x \in (fun e : string => In e l2)) x); [ | auto ]. + simpl. intro. + destr H1. + + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) /\ + ~ x0 \in (fun e : string => In e l2)) x); [ simpl; intro | auto ]. + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + destr H2. left. assumption. + + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + right. assumption. + Qed. + + Lemma sameset_diff_singleton: + forall (l: list string) x, + sameset (diff (of_list l) (of_list [x])) (diff (of_list l) (singleton_set x)). + Proof. + intros. + unfold diff. + unfold sameset. + split; unfold subset; intros. + - cut ((fun x0 : string => + x0 \in of_list l /\ ~ x0 \in of_list [x]) x0); [ | auto ]. + simpl. + intros. + cut ((fun x1 : string => + x1 \in of_list l /\ ~ x1 \in singleton_set x) x0); [ auto | ]. + simpl. + destr H0. + split. + + assumption. + + unfold singleton_set, of_list in *. + destr (eqb x x0). + * assert (~ (In x0 [x0])) by auto. + assert (In x0 [x0]) by eapply in_eq. + eapply H2 in H3. + exfalso; auto. + * eauto. + - cut ((fun x0 : string => + x0 \in of_list l /\ ~ x0 \in of_list [x]) x0); [ auto | ]. + simpl. + cut ((fun x1 : string => + x1 \in of_list l /\ ~ x1 \in singleton_set x) x0); [ | auto ]. + simpl. + intro. + destr H0. + split. + + assumption. + + unfold singleton_set, of_list in *. + cut ((fun e : string => In e [x]) x0 -> False); [ auto | ]. + simpl. + intros. + destr H2; [ | assumption ]. + subst. + assert (eq x0 x0) by auto. + assert (eq x0 x0 -> False) by auto. + auto. + Qed. + + Lemma agree_on_find: + forall s l (m1 m2: locals), + map.agree_on (of_list (if (find (eqb s) l) + then l + else s :: l)) m1 m2 + -> map.agree_on (of_list [s]) m1 m2 /\ + map.agree_on (of_list l) m1 m2. + Proof. + intros. + destr (find (eqb s) l). + - split. + + unfold map.agree_on. + intros. + assert (k = s). + { cut (of_list [s] k); auto. + intros. destr H1; auto. + inversion H1. + } + rewrite H1 in *; clear H1. + apply find_some in E. + destr E. + apply eqb_eq in H2. + rewrite H2 in *. + eauto. + + assumption. + - eapply agree_on_sameset in H. + 2: eapply sameset_sym; eapply of_list_cons. + unfold add in H. + apply agree_on_union in H. + propositional idtac. + unfold map.agree_on in H_l. + assert (map.get m1 s = map.get m2 s). { + apply H_l. + unfold singleton_set. + cut (eq s s); auto. + } + unfold map.agree_on. + intros. + assert (k = s). + { cut (of_list [s] k); auto. + intros. destr H1; auto. + inversion H1. + } + rewrite H1. + assumption. + Qed. + + Lemma agree_on_put_notin : + forall x l m1 m2, + map.agree_on (of_list l) m1 m2 + -> existsb (eqb x) l = false + -> forall v, + map.agree_on (of_list l) (map.put m1 x v) m2. + Proof. Admitted. End WithArguments. From 1559a977e8673d110089f34de55d713c30fb6057 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Wed, 28 Jun 2023 15:07:52 -0400 Subject: [PATCH 12/14] progress update commit (automating deadassignment proof) --- compiler/src/compiler/DeadAssignment.v | 606 ++++++++++++++++++- compiler/src/compiler/DeadAssignmentHelper.v | 330 +++++++++- 2 files changed, 933 insertions(+), 3 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index 30fed792..e1ba5df2 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -26,7 +26,7 @@ Section WithArguments. subset_diff in_singleton subset_union_rr : set_hints. - + Definition compile_post used_after (postH : Semantics.trace -> mem -> locals -> MetricLog -> Prop) : (Semantics.trace -> mem -> locals -> MetricLog -> Prop) := (fun t' m' lL' mcL' => exists lH' mcH', @@ -42,6 +42,608 @@ Section WithArguments. -> exec eL (deadAssignment used_after sH) t m lL mcL (compile_post used_after postH). Proof. induction 2. + - simpl. + intros. + eapply @exec.interact; fwd. + + match goal with + | H: map.split ?m _ _ |- map.split m _ _ => eapply H + end. + + match goal with + | H1: map.getmany_of_list ?l ?argvars = Some ?argvals, + H2: map.agree_on _ ?l ?lL + |- map.getmany_of_list ?lL ?argvars = Some ?y => + cut (map.getmany_of_list l argvars = map.getmany_of_list lL argvars); + intros; + match goal with + | H: map.getmany_of_list l argvars + = map.getmany_of_list lL argvars + |- map.getmany_of_list lL argvars = Some _ => + rewrite <- H; eassumption + | |- map.getmany_of_list l argvars + = map.getmany_of_list lL argvars => + eapply agree_on_getmany; eapply agree_on_subset; + [ eapply H2 | ] + end + end. + repeat match goal with + | |- context[of_list (ListSet.list_union _ _ _)] => rewrite ListSet.of_list_list_union + | |- context[ListSet.list_diff] => rewrite of_list_list_diff + end. + match goal with + | |- subset ?x (union ?x ?y) => + eapply subset_union_rl; eapply subset_ref + end. + + match goal with + | |- ext_spec _ _ _ _ _ => eassumption + end. + + intros. + match goal with + | H: outcome ?mReceive ?resvals, + H1: forall mReceive resvals, + outcome mReceive resvals -> _ |- _ => + apply H1 in H; + repeat match goal with + | H: exists l, _ |- _ => destr H + | H: _ /\ _ |- _ => destr H + end + end. + match goal with + | H: map.putmany_of_list_zip ?resvars ?resvals _ = _ |- + exists l, + map.putmany_of_list_zip resvars resvals _ = Some _ /\ _ + => + let Heq := fresh in + pose proof H as Heq; eapply putmany_Some in H; destr H + end. + match goal with + | H: map.putmany_of_list_zip _ _ _ = Some ?x0 |- _ => eexists x0; split; [ eapply H | ] + end. + match goal with + | |- forall m', map.split m' mKeep mReceive -> _ + => intros + end. + match goal with + | H: map.split ?m ?mKeep ?mReceive, + H': forall m', + map.split m' mKeep mReceive -> _ + |- _ => eapply H' in H + end. + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m' ?x _ |- exists lH' mcH', + map.agree_on _ lH' _ /\ + (post _ _ lH' _) => + exists x; eexists; split; [ | eapply H ] + end. + (* miscellaneous set reasoning; + unclear how to automate this across cases *) + repeat match goal with + | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H + | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H + end. + match goal with + | H: map.agree_on (union _ _) _ _ |- _ => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on (diff (of_list ?l1) (of_list ?l2)) ?l ?lL + |- _ => + match goal with + | H': map.putmany_of_list_zip l2 ?v l = Some ?x |- _ => + match goal with + | H'': map.putmany_of_list_zip l2 v lL = Some ?x0 + |- map.agree_on (of_list l1) x x0 => + eapply agree_on_subset; + [ eauto using agree_on_putmany + | eapply subset_trans; + [ eapply subset_union_rl; eapply subset_ref + | eapply sameset_union_diff_oflist ] + ] + end + end + end. + - simpl. + intros. + eapply @exec.call; fwd. + + match goal with + | H: deadassignment_functions ?eH = Success ?eL, + H1: map.get eH ?fname = Some ?x |- + map.get eL fname = Some _ => + unfold deadassignment_functions in H; + unfold deadassignment_function in H; + eapply map.try_map_values_fw in H; [ | eapply H1 ]; + repeat (destr H; simpl in H) + end. + match goal with + | H: Success _ = Success ?x, + H1: map.get ?eL ?fname = Some x + |- map.get eL fname = Some _ + => inversion H; fwd; eapply H1 + end. + + match goal with + | H: map.getmany_of_list ?l ?args = Some ?argvs + |- map.getmany_of_list lL args = Some _ => + replace (map.getmany_of_list lL args) with (map.getmany_of_list l args); [ eapply H | ] + end. + match goal with + | H: map.agree_on ?s ?l ?lL + |- map.getmany_of_list l ?args + = map.getmany_of_list lL ?args + => eapply agree_on_getmany; + eapply agree_on_subset; [ eapply H | ] + end. + (* set reasoning *) + repeat match goal with + | |- context[of_list (ListSet.list_union _ _ _)] => rewrite ListSet.of_list_list_union + | |- context[ListSet.list_diff] => rewrite of_list_list_diff + end. + match goal with + | |- subset ?x (union ?x ?y) => + eapply subset_union_rl; eapply subset_ref + end. + + match goal with + | |- map.putmany_of_list_zip _ _ _ = Some _ => eassumption + end. + + match goal with + | |- exec _ _ _ _ _ _ _ => eauto using agree_on_refl + end. + + match goal with + | |- forall t' m' mc' st1, + compile_post ?rets ?outcome t' m' st1 mc' -> _ + => unfold compile_post; intros; fwd + end. + + match goal with + | H: outcome _ _ _ _, + H1: forall t' m' mc' st1, + outcome _ _ _ _ -> + exists retvs l', + map.getmany_of_list st1 ?rets = Some retvs /\ _ + |- _ => eapply H1 in H; fwd + end. + + match goal with + | H: map.putmany_of_list_zip ?binds ?x1 ?l = Some ?x2, + H1: map.agree_on _ l ?lL + |- context[map.putmany_of_list_zip ?binds _ ?lL] => + let Heq := fresh in + pose proof H as Heq; eapply putmany_Some in H; destr H; fwd + end. + + match goal with + | H: map.agree_on (of_list ?rets) ?lH' ?st1, + H1: map.getmany_of_list ?lH' ?rets = Some ?retvs, + H2: map.putmany_of_list_zip ?binds ?retvs _ = Some ?x |- + exists retvs0 l'0, + map.getmany_of_list st1 rets = Some retvs0 /\ _ + => exists retvs; exists x; repeat split; [ | eapply H2 | ] + end. + * match goal with + | H: map.agree_on (of_list ?rets) ?lH' ?st1, + H1: map.getmany_of_list ?lH' ?rets = Some ?retvs + |- map.getmany_of_list ?st1 ?rets = Some ?retvs + => apply agree_on_getmany in H; rewrite <- H; eapply H1 + end. + * match goal with + | H: post ?t' ?m' ?l' _ + |- exists lH'0 mcH'0, + map.agree_on (of_list ?used_after) lH'0 ?x /\ + post ?t' ?m' lH'0 mcH'0 + => exists l'; eexists; split; [ | eapply H ] + end. + repeat match goal with + | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H + | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H + end. + match goal with + | H: map.agree_on (union _ _) ?l ?lL + |- _ => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on (diff (of_list ?used_after) (of_list ?binds)) ?l ?lL, + H1: map.putmany_of_list_zip binds ?retvs l = Some ?l', + H2: map.putmany_of_list_zip binds retvs lL = Some ?x + |- map.agree_on (of_list used_after) l' x + => eapply agree_on_subset; + [ eauto using agree_on_putmany | + eapply subset_trans; + [ eapply subset_union_rl; eapply subset_ref | + eapply sameset_union_diff_oflist ] + ] + end. + - simpl. + intros. + match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ => + apply agree_on_find in H; destr H + end. + eapply @exec.load; fwd. + + match goal with + | H: map.agree_on (of_list [?a]) ?l ?lL, + H1: map.get ?l ?a = Some ?addr |- + map.get ?lL ?a = Some _ => rewrite <- H; [ eassumption | ] + end. + match goal with + | |- ?s \in of_list [?s] => cut (of_list [s] s); [ simpl; intro; auto | unfold of_list; simpl; auto ] + end. + + match goal with + | H: Memory.load _ _ _ = Some _ |- Memory.load _ _ _ = Some _ => eapply H + end. + + match goal with + | |- compile_post _ _ _ _ _ _ => unfold compile_post + end. + match goal with + | H: post ?t m (map.put ?l ?x ?v) _, + H1: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list used_after) lH' + (map.put lL x v) /\ + post t m lH' mcH' + => exists (map.put l x v); eexists; split; [ | ] ; + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) _ |- post t m (map.put l x v) _ => eapply H + | |- _ => idtac + end + end. + + match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list used_after) (map.put ?l ?x ?v) (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; + eapply agree_on_subset; + match goal with + | |- map.agree_on _ (map.put l x v) (map.put lL x v) + => eapply agree_on_put; + match goal with + | |- map.put _ _ _ = map.put _ _ _ => reflexivity + | |- _ => idtac + end; + match goal with + | |- map.agree_on _ l lL => eapply H + end + (* Note that order matters in execution of these two tactics, ^ which is why they aren't in the same match-goal *) + | |- _ => idtac + end + end. + + match goal with + | |- subset (of_list ?s) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + - simpl. intros. + repeat match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ + => apply agree_on_find in H; destr H + end. + eapply @exec.store; fwd. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | |- Memory.store _ _ (word.add _ _) _ = Some _ => eassumption + end. + + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: map.agree_on ?s ?l ?lL, + H1: post ?t ?m' ?l ?mcH' + |- exists lH' mcH', + map.agree_on ?s lH' ?lL /\ + post ?t ?m' lH' mcH' + => exists l; eexists; split; [ eapply H | eapply H1 ] + end. + - simpl. intros. + match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ => + apply agree_on_find in H; destr H + end. + eapply @exec.inlinetable. + + match goal with + | |- ?x <> ?i => assumption + end. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | |- Memory.load _ (OfListWord.map.of_list_word _) _ = Some _ => eassumption + end. + + (* Note for further automation: + this goal's proof is exactly lifted from + the exec.load case's corresponding goal. *) + + match goal with + | |- context[compile_post] => unfold compile_post + end. + + match goal with + | H: post ?t m (map.put ?l ?x ?v) _, + H1: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list used_after) lH' + (map.put lL x v) /\ + post t m lH' mcH' + => exists (map.put l x v); eexists; split; [ | ] ; + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) _ |- post t m (map.put l x v) _ => eapply H + | |- _ => idtac + end + end. + match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list used_after) (map.put ?l ?x ?v) (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; + eapply agree_on_subset; + match goal with + | |- map.agree_on _ (map.put l x v) (map.put lL x v) + => eapply agree_on_put; + match goal with + | |- map.put _ _ _ = map.put _ _ _ => reflexivity + | |- _ => idtac + end; + match goal with + | |- map.agree_on _ l lL => eapply H + end + (* Note that order matters in execution of these two tactics, ^ which is why they aren't in the same match-goal *) + | |- _ => idtac + end + end. + + match goal with + | |- subset (of_list ?s) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + + - simpl. + intros. + eapply @exec.stackalloc. + + match goal with + | |- ?n mod Memory.bytes_per_word ?width = 0 => assumption + end. + + (* For complicated goals like this, + unsure how sound automation will be. *) + match goal with + | |- forall a mStack mCombined, + Memory.anybytes a ?n mStack -> + map.split mCombined ?mSmall mStack -> + exec _ _ _ mCombined _ _ _ + => intros + end. + match goal with + | H: context[exec _ (deadAssignment _ _) _ _ _ _ _], + H1: Memory.anybytes _ _ _, + H2: map.agree_on (of_list (List.removeb eqb ?x ?l')) ?l ?lL |- exec _ (deadAssignment _ _) _ _ (map.put ?lL ?x ?a) _ _ => + eapply H with (lL := map.put lL x a) in H1 + end. + all: try match goal with + | H: map.split _ ?mSmall ?mStack |- + map.split _ ?mSmall ?mStack => eapply H + end. + all: try match goal with + | |- map.agree_on + _ (map.put ?l ?x ?a) (map.put ?lL ?x ?a) + => eapply agree_on_subset; + match goal with + | |- map.agree_on _ (map.put ?l ?x ?a) + (map.put ?lL ?x ?a) => + eapply agree_on_put; + match goal with + | |- map.put _ _ _ = map.put _ _ _ + => reflexivity + | |- map.agree_on _ ?l ?lL => eassumption + end + | |- subset _ _ => idtac + end + end. + all: try match goal with + | |- subset _ (union (of_list (List.removeb eqb ?x ?l)) (singleton_set ?x)) => rewrite ListSet.of_list_removeb + end. + (* Copy pasted from earlier, + but this time the left argument to subset is unspecified + *) + all: try match goal with + | |- subset (of_list _) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + match goal with + | H: exec ?eL ?s ?t ?m ?l _ ?post |- exec ?eL ?s ?t ?m ?l _ ?post' => eapply exec.weaken; [ eapply H | simpl ] + end. + match goal with + | |- context[compile_post] => + unfold compile_post; simpl; intros; fwd + end. + match goal with + | H: Memory.anybytes ?a ?n ?mStack', + H1: map.split ?m' ?mSmall' ?mStack', + H2: post ?t' ?mSmall' ?lH' ?mcH', + H3: map.agree_on (of_list ?used_after) ?lH' ?l' + |- exists mSmall'1 mStack'1, + Memory.anybytes ?a ?n mStack'1 /\ + map.split ?m' mSmall'1 mStack'1 /\ + (exists lH'0 mcH'0, + map.agree_on (of_list ?used_after) lH'0 ?l' /\ + post ?t' mSmall'1 lH'0 mcH'0) => + exists mSmall'; exists mStack'; propositional idtac + end. + - simpl. intros. + destr (existsb (eqb x) used_after). + + eapply @exec.lit. + unfold compile_post. + exists (map.put l x (word.of_Z v)). + eexists. + propositional idtac. + * simpl in *. + eapply agree_on_subset. + -- eapply agree_on_put. + 2-3: reflexivity. + eapply H1. + -- rewrite ListSet.of_list_removeb. + try match goal with + | |- subset (of_list _) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + * eapply H0. + + eapply @exec.skip. + unfold compile_post. + simpl in *. + eexists (map.put l x (word.of_Z v)). + eexists. + split. + + repeat eexists. + eapply H0. + + exists mSmall'. + exists mStack'. + propositional idtac. + fwd. + eapply exec.weaken. + * eapply H4. + * unfold compile_post. + simpl. intros. + fwd. + exists mSmall'. + exists mStack'. + propositional idtac. + - + Search @exec.exec. + + + + + 2: { eapply agree_on_put. + + eapply H2 in H4. + 2: eassumption. + * eapply H4. + eaply H2. + match goal with + | H: _ -> exec ?eL (deadAssignment ?used_After + + + * eassumption. + * eapply agree_on_getmany. + eapply agree_on_subset; [ eapply H4 | ]. + rewrite ListSet.of_list_list_union. + eapply subset_union_rl. + eapply subset_ref. + + eassumption. + + unfold compile_post. + intros. + eapply H3 in H5. + destr H5. + destr H5. + pose proof H5 as H5'. + eapply putmany_Some in H5'. + destr H5'. + eexists x0. + split; [ eapply H7 | ]. + intros. + eapply H6 in H8. + exists x. + eexists. + split. + 2: eapply H8. + rewrite ListSet.of_list_list_union in H4. + rewrite of_list_list_diff in H4. + apply agree_on_union in H4. + destr H4. + eapply agree_on_subset; + [ eauto using agree_on_putmany | ]. + eapply subset_trans. + 2: eapply sameset_union_diff. + eapply subset_union_rl. + eapply subset_ref. 13: { intros. simpl. @@ -219,7 +821,7 @@ Section WithArguments. Admitted. End WithArguments. -(* +(* Lemma live_monotone : forall s used_after used_after', subset (of_list used_after) (of_list used_after') -> diff --git a/compiler/src/compiler/DeadAssignmentHelper.v b/compiler/src/compiler/DeadAssignmentHelper.v index 7d0c4c80..764f0fb3 100644 --- a/compiler/src/compiler/DeadAssignmentHelper.v +++ b/compiler/src/compiler/DeadAssignmentHelper.v @@ -16,6 +16,66 @@ Section WithArguments. Context {word : word width } {word_ok : word.ok word}. Context {locals : map.map string word } {locals_ok: map.ok locals}. + Lemma putmany_Some' : + forall (lk: list string) lv (m: locals), + (exists m', map.putmany_of_list_zip lk lv m = Some m') + <-> Datatypes.length lk = Datatypes.length lv. + Proof. + induction lk. + - simpl. intros. destr lv. + + simpl. + unfold iff; split. + * intros. reflexivity. + * intros. eauto. + + simpl. + unfold iff; split. + * intros. destr H. discriminate. + * intros. discriminate. + - intros. destr lv. + + simpl. + unfold iff; split. + * intros. destr H. discriminate. + * intros. discriminate. + + simpl. + unfold iff; split. + * intros. apply eq_S. + eapply IHlk. + eapply H. + * intros. apply eq_add_S in H. + eapply IHlk in H. + eapply H. + Qed. + + Lemma putmany_Some: + forall (lk: list string) lv (m0: locals) m1, + map.putmany_of_list_zip lk lv m0 = Some m1 + -> (forall (m: locals), + (exists m', map.putmany_of_list_zip lk lv m = Some m')). + Proof. + intros. + eapply putmany_Some'. + eapply putmany_Some'. + eexists. + eapply H. + Qed. + + Lemma agree_on_union: + forall (s0 s1: set string) (m0 m1: locals), + map.agree_on (union s0 s1) m0 m1 + <-> map.agree_on s0 m0 m1 /\ map.agree_on s1 m0 m1. + Proof. + intros. + unfold iff; split. + - unfold map.agree_on in *. + split; intros; cut (s0 k \/ s1 k); auto. + - unfold map.agree_on in *. + intros. + destr H. + cut (s0 k \/ s1 k). + + intros. destr H2; auto. + + auto. + Qed. + Lemma agree_on_refl : forall keySet (m : locals), map.agree_on keySet m m. @@ -294,7 +354,275 @@ Section WithArguments. Proof. intros. induction l2. - - simpl. + (* PR for this lemma being proved in coqutil exists; + unsure how to prove it without the assumptions + in the file that ListSet.of_list_list_union + is proven in *) Admitted. + + Lemma agree_on_put: + forall a r s (mH mL: locals) mH' mL', + map.agree_on s mH mL -> + map.put mH a r = mH' -> + map.put mL a r = mL' -> + map.agree_on (union s (singleton_set a)) mH' mL'. + Proof. + intros. + apply agree_on_union. + split. + - unfold map.agree_on in *. + intros. + eapply H in H2. + subst. + destr (eqb a k). + + repeat rewrite map.get_put_same; reflexivity. + + repeat rewrite map.get_put_diff; eauto. + - unfold map.agree_on. + intros. + cut (a = k). + + intros. subst. + repeat rewrite map.get_put_same; reflexivity. + + assert (singleton_set a k) by auto. + unfold singleton_set in *; assumption. + Qed. + + Lemma union_sameset: + forall (s1 s2 s1' s2': set string), + sameset s1 s1' -> + sameset s2 s2' -> + sameset (union s1 s2) (union s1' s2'). + Proof. + intros. + unfold sameset, union. + split. + - unfold sameset, subset in *. + propositional idtac. + assert (x \in s1 \/ x \in s2) by auto. + cut (x \in s1' \/ x \in s2'); [ auto | ]. + destr H. + + left; eauto. + + right; eauto. + - unfold sameset, subset in *. + propositional idtac. + assert (x \in s1' \/ x \in s2') by auto. + cut (x \in s1 \/ x \in s2); [ auto | ]. + destr H. + + left; eauto. + + right; eauto. + Qed. + + Lemma agree_on_putmany: + forall (lk0: list string) lv s (mH mL: locals) mH' mL', + map.agree_on s mH mL -> + map.putmany_of_list_zip lk0 lv mH = Some mH' -> + map.putmany_of_list_zip lk0 lv mL = Some mL' -> + map.agree_on (union s (of_list lk0)) mH' mL'. + Proof. + induction lk0. + - intros. simpl in *. + destr lv; [ | discriminate ]. + apply agree_on_union. + split. + + inversion H0. + inversion H1. + subst; eauto. + + unfold map.agree_on. + intros. + cut (of_list [] k). + * unfold of_list. + intros. + exfalso. + eauto using in_nil. + * auto. + - intros. destr lv; [ discriminate | ]. + simpl in *. + cut (map.agree_on (union s (singleton_set a)) + (map.put mH a r) (map.put mL a r)). + + intros. + eapply IHlk0 in H2. + 2-3: eassumption. + eapply agree_on_sameset. + * eassumption. + * eapply sameset_trans. + 2: { eapply union_assoc. } + apply union_sameset; + [ eapply sameset_ref | eapply of_list_cons ]. + + eapply agree_on_put. + 2-3: reflexivity. + eassumption. + Qed. + + + Lemma sameset_union_diff_oflist: + forall (l1 l2: list string), + sameset (union (of_list l1) (of_list l2)) (union (diff (of_list l1) (of_list l2) ) (of_list l2)). + Proof. + intros. + unfold sameset, of_list, subset, union, diff. + + assert (forall x, In x l2 \/ ~ (In x l2)). + { intro. eapply ListDec.In_decidable. unfold ListDec.decidable_eq. + intros. destr (eqb x0 y). + - unfold Decidable.decidable. left. reflexivity. + - unfold Decidable.decidable. right. eassumption. + } + + split. + - intros. + cut ((fun x : string => + x \in (fun e : string => In e l1) \/ + x \in (fun e : string => In e l2)) x); [ simpl; intro | auto ]. + cut ((In x l1) \/ (In x l2)); [ simpl; intro | auto ]. + cut ((fun x0 : string => + x0 \in + (fun x1 : string => + x1 \in (fun e : string => In e l1) /\ + ~ x1 \in (fun e : string => In e l2)) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + assert (In x l2 \/ ~ In x l2) by eapply H. + destr H3. + + right. auto. + + propositional idtac. left. + cut ((fun x1 : string => + x1 \in (fun e : string => In e l1) /\ + ~ x1 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + split; auto. + - intros. + cut ((fun x : string => + x \in + (fun x0 : string => + x0 \in (fun e : string => In e l1) /\ + ~ x0 \in (fun e : string => In e l2)) \/ + x \in (fun e : string => In e l2)) x); [ | auto ]. + simpl. intro. + destr H1. + + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) /\ + ~ x0 \in (fun e : string => In e l2)) x); [ simpl; intro | auto ]. + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + destr H2. left. assumption. + + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + right. assumption. + Qed. + + Lemma sameset_diff_singleton: + forall (l: list string) x, + sameset (diff (of_list l) (of_list [x])) (diff (of_list l) (singleton_set x)). + Proof. + intros. + unfold diff. + unfold sameset. + split; unfold subset; intros. + - cut ((fun x0 : string => + x0 \in of_list l /\ ~ x0 \in of_list [x]) x0); [ | auto ]. + simpl. + intros. + cut ((fun x1 : string => + x1 \in of_list l /\ ~ x1 \in singleton_set x) x0); [ auto | ]. + simpl. + destr H0. + split. + + assumption. + + unfold singleton_set, of_list in *. + destr (eqb x x0). + * assert (~ (In x0 [x0])) by auto. + assert (In x0 [x0]) by eapply in_eq. + eapply H2 in H3. + exfalso; auto. + * eauto. + - cut ((fun x0 : string => + x0 \in of_list l /\ ~ x0 \in of_list [x]) x0); [ auto | ]. + simpl. + cut ((fun x1 : string => + x1 \in of_list l /\ ~ x1 \in singleton_set x) x0); [ | auto ]. + simpl. + intro. + destr H0. + split. + + assumption. + + unfold singleton_set, of_list in *. + cut ((fun e : string => In e [x]) x0 -> False); [ auto | ]. + simpl. + intros. + destr H2; [ | assumption ]. + subst. + assert (eq x0 x0) by auto. + assert (eq x0 x0 -> False) by auto. + auto. + Qed. + + Lemma agree_on_find: + forall s l (m1 m2: locals), + map.agree_on (of_list (if (find (eqb s) l) + then l + else s :: l)) m1 m2 + -> map.agree_on (of_list [s]) m1 m2 /\ + map.agree_on (of_list l) m1 m2. + Proof. + intros. + destr (find (eqb s) l). + - split. + + unfold map.agree_on. + intros. + assert (k = s). + { cut (of_list [s] k); auto. + intros. destr H1; auto. + inversion H1. + } + rewrite H1 in *; clear H1. + apply find_some in E. + destr E. + apply eqb_eq in H2. + rewrite H2 in *. + eauto. + + assumption. + - eapply agree_on_sameset in H. + 2: eapply sameset_sym; eapply of_list_cons. + unfold add in H. + apply agree_on_union in H. + propositional idtac. + unfold map.agree_on in H_l. + assert (map.get m1 s = map.get m2 s). { + apply H_l. + unfold singleton_set. + cut (eq s s); auto. + } + unfold map.agree_on. + intros. + assert (k = s). + { cut (of_list [s] k); auto. + intros. destr H1; auto. + inversion H1. + } + rewrite H1. + assumption. + Qed. + + Lemma agree_on_put_not_in : + forall x l (m1 m2: locals), + map.agree_on (of_list l) m1 m2 + -> existsb (eqb x) l = false + -> forall v, + map.agree_on (of_list l) (map.put m1 x v) m2. + Proof. + intros. + unfold map.agree_on. + intros. + rewrite <- H. + 2: eassumption. + erewrite agree_on_not_in. + 3: eassumption. + 2: eassumption. + reflexivity. + Qed. + End WithArguments. From 3e5c98a636de7ffce3d3ebb76c5a205ca0c20e66 Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Thu, 13 Jul 2023 09:54:03 -0400 Subject: [PATCH 13/14] progress on dead assignment proof --- compiler/src/compiler/DeadAssignment.v | 699 +++++++++++++------ compiler/src/compiler/DeadAssignmentHelper.v | 205 ++++++ 2 files changed, 688 insertions(+), 216 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index e1ba5df2..54103f59 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -291,46 +291,10 @@ Section WithArguments. | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL |- map.agree_on (of_list used_after) (map.put ?l ?x ?v) (map.put ?lL ?x ?v) => rewrite ListSet.of_list_removeb in H; - eapply agree_on_subset; - match goal with - | |- map.agree_on _ (map.put l x v) (map.put lL x v) - => eapply agree_on_put; - match goal with - | |- map.put _ _ _ = map.put _ _ _ => reflexivity - | |- _ => idtac - end; - match goal with - | |- map.agree_on _ l lL => eapply H - end - (* Note that order matters in execution of these two tactics, ^ which is why they aren't in the same match-goal *) - | |- _ => idtac - end + apply agree_on_diff_of_list_singleton; + assumption end. - match goal with - | |- subset (of_list ?s) - (union (diff (of_list ?s) (singleton_set ?x)) - (singleton_set ?x)) => - eapply subset_trans; - match goal with - | |- subset (of_list _) _ => idtac - | |- subset _ (union _ _) => - eapply union_sameset; - match goal with - | |- sameset (diff _ _) _ => - eapply sameset_sym; eapply sameset_diff_singleton - | |- sameset (singleton_set _) _ => - eapply sameset_sym; eapply of_list_singleton - end - end; - eapply subset_trans; - match goal with - | |- subset (of_list _) _ => idtac - | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist - end; - eapply subset_union_rl; - eapply subset_ref - end. - simpl. intros. repeat match goal with | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ @@ -404,46 +368,9 @@ Section WithArguments. |- map.agree_on (of_list used_after) (map.put ?l ?x ?v) (map.put ?lL ?x ?v) => rewrite ListSet.of_list_removeb in H; eapply agree_on_subset; - match goal with - | |- map.agree_on _ (map.put l x v) (map.put lL x v) - => eapply agree_on_put; - match goal with - | |- map.put _ _ _ = map.put _ _ _ => reflexivity - | |- _ => idtac - end; - match goal with - | |- map.agree_on _ l lL => eapply H - end - (* Note that order matters in execution of these two tactics, ^ which is why they aren't in the same match-goal *) - | |- _ => idtac - end + [ eapply agree_on_diff_of_list_singleton; eassumption + | eapply sameset_ref ] end. - - match goal with - | |- subset (of_list ?s) - (union (diff (of_list ?s) (singleton_set ?x)) - (singleton_set ?x)) => - eapply subset_trans; - match goal with - | |- subset (of_list _) _ => idtac - | |- subset _ (union _ _) => - eapply union_sameset; - match goal with - | |- sameset (diff _ _) _ => - eapply sameset_sym; eapply sameset_diff_singleton - | |- sameset (singleton_set _) _ => - eapply sameset_sym; eapply of_list_singleton - end - end; - eapply subset_trans; - match goal with - | |- subset (of_list _) _ => idtac - | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist - end; - eapply subset_union_rl; - eapply subset_ref - end. - - simpl. intros. eapply @exec.stackalloc. @@ -470,51 +397,13 @@ Section WithArguments. map.split _ ?mSmall ?mStack => eapply H end. all: try match goal with - | |- map.agree_on - _ (map.put ?l ?x ?a) (map.put ?lL ?x ?a) - => eapply agree_on_subset; - match goal with - | |- map.agree_on _ (map.put ?l ?x ?a) - (map.put ?lL ?x ?a) => - eapply agree_on_put; - match goal with - | |- map.put _ _ _ = map.put _ _ _ - => reflexivity - | |- map.agree_on _ ?l ?lL => eassumption - end - | |- subset _ _ => idtac - end - end. - all: try match goal with - | |- subset _ (union (of_list (List.removeb eqb ?x ?l)) (singleton_set ?x)) => rewrite ListSet.of_list_removeb - end. - (* Copy pasted from earlier, - but this time the left argument to subset is unspecified - *) - all: try match goal with - | |- subset (of_list _) - (union (diff (of_list ?s) (singleton_set ?x)) - (singleton_set ?x)) => - eapply subset_trans; - match goal with - | |- subset (of_list _) _ => idtac - | |- subset _ (union _ _) => - eapply union_sameset; - match goal with - | |- sameset (diff _ _) _ => - eapply sameset_sym; eapply sameset_diff_singleton - | |- sameset (singleton_set _) _ => - eapply sameset_sym; eapply of_list_singleton - end - end; - eapply subset_trans; - match goal with - | |- subset (of_list _) _ => idtac - | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist - end; - eapply subset_union_rl; - eapply subset_ref - end. + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list _) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; eapply agree_on_diff_of_list_singleton; eassumption + end. + match goal with | H: exec ?eL ?s ?t ?m ?l _ ?post |- exec ?eL ?s ?t ?m ?l _ ?post' => eapply exec.weaken; [ eapply H | simpl ] end. @@ -536,114 +425,492 @@ Section WithArguments. exists mSmall'; exists mStack'; propositional idtac end. - simpl. intros. - destr (existsb (eqb x) used_after). + match goal with + | H: context[existsb (eqb ?x) ?used_after] |- + context[existsb (eqb ?x) ?used_after] => + destr (existsb (eqb x) used_after) + end; + match goal with + | H: map.agree_on (of_list (live _ _)) ?l ?lL |- _ => + simpl in H + end. + eapply @exec.lit. unfold compile_post. - exists (map.put l x (word.of_Z v)). - eexists. - propositional idtac. - * simpl in *. - eapply agree_on_subset. - -- eapply agree_on_put. - 2-3: reflexivity. - eapply H1. - -- rewrite ListSet.of_list_removeb. - try match goal with - | |- subset (of_list _) - (union (diff (of_list ?s) (singleton_set ?x)) - (singleton_set ?x)) => - eapply subset_trans; - match goal with - | |- subset (of_list _) _ => idtac - | |- subset _ (union _ _) => - eapply union_sameset; - match goal with - | |- sameset (diff _ _) _ => - eapply sameset_sym; eapply sameset_diff_singleton - | |- sameset (singleton_set _) _ => - eapply sameset_sym; eapply of_list_singleton - end - end; - eapply subset_trans; - match goal with - | |- subset (of_list _) _ => idtac - | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist - end; - eapply subset_union_rl; - eapply subset_ref - end. - * eapply H0. + match goal with + | H: existsb (eqb ?x) ?used_after = true, + H1: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL, + H2: post ?t ?m (map.put ?l ?x (word.of_Z ?v)) ?mcH + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' + (map.put ?lL ?x (word.of_Z ?v)) /\ + post ?t ?m lH' mcH' => simpl in H1; exists (map.put l x (word.of_Z v)); eexists; propositional idtac + end. + * match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; eapply agree_on_diff_of_list_singleton; eassumption + end. + * match goal with + | H: post ?t ?m ?l ?mc |- + post ?t ?m ?l _ => eapply H + end. + eapply @exec.skip. unfold compile_post. - simpl in *. - eexists (map.put l x (word.of_Z v)). - eexists. - split. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: map.agree_on (of_list ?used_after) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' ?lL + /\ post ?t ?m lH' mcH' => + exists (map.put l x v); + exists mcH; propositional idtac; + apply agree_on_put_not_in; eauto + end. + - simpl. intros. + match goal with + | H: context[existsb (eqb ?x) ?used_after] |- + context[existsb (eqb ?x) ?used_after] => + destr (existsb (eqb x) used_after) + end; + match goal with + | H: map.agree_on (of_list (live _ _)) ?l ?lL |- _ => + simpl in H + end. + all: try repeat match goal with + | H: context[match ?z with _ => _ end] |- _ => destr z + end; simpl. + all: try match goal with + | H: find (eqb ?y) ?l = Some ?y' |- _ => + apply find_some in H; destr H; + match goal with + | H: (?a = ?b)%string |- _ => + apply eqb_eq in H; rewrite H in * + end; + match goal with + | H: In ?x (ListSet.list_union _ _ _) |- _ => + apply in_of_list in H4 + end + end. - repeat eexists. - eapply H0. + all: try repeat rewrite ListSet.of_list_list_union, ListSet.of_list_removeb in *. + + eapply @exec.op. + * match goal with + | H: map.get ?l ?s = Some ?y', + H1: ?s \in ?s', + H2: map.agree_on ?s' ?l ?lL + |- map.get ?lL ?s = _ => rewrite H2 in H; [ eapply H | eapply H1 ] + end. + * match goal with + | H: exec.lookup_op_locals ?l (Var ?v) = Some ?z', + H1: map.agree_on (union (of_list [?v]) _) ?l ?lL |- exec.lookup_op_locals ?lL (Var ?v) = Some _ => unfold exec.lookup_op_locals in *; simpl; rewrite H1 in H; [ eapply H | ] + end. - exists mSmall'. - exists mStack'. - propositional idtac. - fwd. - eapply exec.weaken. - * eapply H4. - * unfold compile_post. - simpl. intros. - fwd. - exists mSmall'. - exists mStack'. - propositional idtac. - - - Search @exec.exec. + match goal with + | |- ?v \in union (of_list [?v]) _ => + apply in_union_l; constructor; reflexivity + end. + * match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: map.agree_on + (union _ + (diff (of_list ?used_after) (singleton_set ?x))) + ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' + (map.put ?lL ?x ?v) /\ post ?t ?m lH' mcH' + => exists (map.put l x v); exists mcH; split + end. + -- match goal with + | H: map.agree_on + (union _ (diff (of_list ?used_after) (singleton_set ?x))) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on + (diff (of_list ?used_after) (singleton_set ?x)) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => eapply agree_on_diff_of_list_singleton; eassumption + end. + -- match goal with + | H: post ?t ?m ?l ?mc |- post ?t ?m ?l ?mc + => eapply H + end. + + (* Note: duplicated from previous '+' case, + with change from Var v -> Const c *) + eapply @exec.op. + * match goal with + | H: map.get ?l ?s = Some ?y', + H1: ?s \in ?s', + H2: map.agree_on ?s' ?l ?lL + |- map.get ?lL ?s = _ => rewrite H2 in H; [ eapply H | eapply H1 ] + end. + * match goal with + | |- exec.lookup_op_locals ?lL (Const ?v) = Some _ => unfold exec.lookup_op_locals in *; simpl; reflexivity + end. + * match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: exec.lookup_op_locals _ (Const ?c) = Some ?z' |- _ => + simpl in H; inversion H; fwd + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: map.agree_on + (union _ + (diff (of_list ?used_after) (singleton_set ?x))) ?l ?lL + + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' + (map.put ?lL ?x ?v) /\ post ?t ?m lH' mcH' + => exists (map.put l x v); exists mcH; split; + [ | eapply H ] + end. + match goal with + | H: map.agree_on + (union _ (diff (of_list ?used_after) (singleton_set ?x))) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on + (diff (of_list ?used_after) (singleton_set ?x)) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => eapply agree_on_diff_of_list_singleton; eassumption + end. + + eapply @exec.op. + * match goal with + | H: map.agree_on (of_list (?y :: ?c)) ?l ?lL + |- _ => eapply agree_on_cons in H; destr H + end. + match goal with + | H: map.get ?l ?y = Some ?y', + H1: map.get ?l ?y = map.get ?lL ?y + |- map.get ?lL ?y = Some _ => rewrite <- H1; eapply H + end. + * match goal with + | H: map.agree_on (of_list (?y :: ?c)) ?l ?lL + |- _ => eapply agree_on_cons in H; destr H + end. + + match goal with + | H: exec.lookup_op_locals ?l (Var ?v) = Some ?z' |- exec.lookup_op_locals ?lL (Var ?v) = Some _ => unfold exec.lookup_op_locals in *; simpl + end. + + match goal with + | H: map.agree_on + (of_list + (ListSet.list_union eqb [?v] + _)) ?l ?lL, + H1: map.get ?l ?v = Some ?z' |- map.get ?lL ?v = Some _ => rewrite H in H1; [ apply H1 | rewrite ListSet.of_list_list_union; apply in_union_l ] + end. + match goal with + | |- ?v \in of_list [?v] => constructor; reflexivity + end. + * match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: map.agree_on (of_list (?y :: ?c)) ?l ?lL + |- _ => eapply agree_on_cons in H; destr H + end. + match goal with + | H: map.agree_on + (of_list + (ListSet.list_union eqb _ _)) ?l ?lL + |- _ => rewrite ListSet.of_list_list_union in H; + apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on + (of_list (List.removeb eqb _ _)) ?l ?lL + |- _ => rewrite ListSet.of_list_removeb in H + end. + match goal with + | H: context[exec.lookup_op_locals] |- _ => simpl in H + end. + match goal with + | H: map.agree_on + (diff (of_list ?used_after) + (singleton_set ?x)) + ?l ?lL, + H1: post ?t ?m (map.put ?l ?x (?f ?op ?y' ?z')) ?mcH + |- exists lH' mcH', + map.agree_on (of_list ?used_after) + lH' + (map.put ?lL ?x (?f ?op ?y' ?z')) /\ + post ?t ?m lH' mcH' + => exists (map.put l x (f op y' z')); exists mcH; split; + [ | eapply H1 ] + end. + match goal with + | H: map.agree_on + (diff (of_list ?used_after) (singleton_set ?x)) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => eapply agree_on_diff_of_list_singleton; eassumption + end. + + match goal with + | H: map.agree_on (of_list (?y :: ?c)) ?l ?lL + |- _ => eapply agree_on_cons in H; destr H + end. + match goal with + | H: map.agree_on + (of_list + (ListSet.list_union eqb _ _)) ?l ?lL + |- _ => rewrite ListSet.of_list_list_union in H; + apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on + (of_list (List.removeb eqb _ _)) ?l ?lL + |- _ => rewrite ListSet.of_list_removeb in H + end. + match goal with + | H: context[exec.lookup_op_locals] |- _ => + simpl in H; fwd + end. + eapply @exec.op. + * match goal with + | H: map.get ?l ?y = Some ?y', + H1: map.get ?l ?y = map.get ?lL ?y + |- map.get ?lL ?y = Some _ => + rewrite H1 in H; eapply H + end. + * match goal with + | |- context[exec.lookup_op_locals] => + simpl; auto + end. + * match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m + (map.put ?l ?x (?f ?op ?y' ?z')) + ?mcH, + H1: map.agree_on (diff (of_list ?used_after) + (singleton_set ?x)) + ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' + (map.put ?lL ?x (?f ?op ?y' ?z')) /\ + post ?t ?m lH' mcH' + => exists (map.put l x (f op y' z')); exists mcH; split + end. + -- match goal with + | H: map.agree_on + (diff (of_list ?used_after) (singleton_set ?x)) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => eapply agree_on_diff_of_list_singleton; + eassumption + end. + -- match goal with + | H: post ?t ?m ?l ?mcH |- post ?t ?m ?l ?mcH + => eapply H + end. + + eapply @exec.skip. + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: existsb (eqb ?x) ?used_after = false, + H2: map.agree_on (of_list ?used_after) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' ?lL /\ + post ?t ?m lH' mcH' + => exists (map.put l x v); exists mcH; split; [ | eapply H ] + end. + match goal with + | H: existsb (eqb ?x) ?used_after = false, + H1: map.agree_on (of_list ?used_after) ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) ?lL => + eapply agree_on_put_not_in; [ eapply H1 | eapply H ] + end. + - simpl. intros. + match goal with + | H: context[existsb (eqb ?x) ?used_after] |- + context[existsb (eqb ?x) ?used_after] => + destr (existsb (eqb x) used_after) + end; + match goal with + | H: map.agree_on (of_list (live _ _)) ?l ?lL |- _ => + simpl in H + end. + all: try repeat match goal with + | H: context[match ?z with _ => _ end] |- _ => destr z + end; simpl. + all: try match goal with + | H: find (eqb ?y) ?l = Some ?y' |- _ => + apply find_some in H; destr H; + match goal with + | H: (?a = ?b)%string |- _ => + apply eqb_eq in H; rewrite H in * + end; + match goal with + | H: In ?s _ |- _ => + apply in_of_list in H + end + end. + + eapply @exec.set. + * match goal with + | H: map.get ?l ?s = Some ?y' + , H1: map.agree_on (of_list ?l') ?l ?lL + , H2: ?s \in of_list ?l' |- _ => + rewrite H1 in H; [ eapply H | eapply H2 ] + end. + * match goal with + | |- context[compile_post] => unfold compile_post; simpl + end. + repeat match goal with + | H: context[of_list (List.removeb eqb _ _)] |- _ => + rewrite ListSet.of_list_removeb in H + end. - 2: { eapply agree_on_put. + match goal with + | H: map.agree_on (diff (of_list ?used_after) (singleton_set ?x)) ?l ?lL, + H1: post ?t ?m (map.put ?l ?x ?y') ?mcH, + H2: ?s \in (diff (of_list ?used_after) (singleton_set ?x)) + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' (map.put ?lL ?x ?y) /\ post ?t ?m lH' mcH' => + exists (map.put l x y); exists mcH; split; [ | eapply H1 ] + end. + match goal with + | H: map.agree_on (diff (of_list ?used_after) (singleton_set ?x)) ?l ?lL |- + map.agree_on (of_list ?used_after) (map.put ?l ?x ?y') (map.put ?lL ?x ?y') => + eapply agree_on_diff_of_list_singleton; + eapply H + end. + + match goal with + | H: map.agree_on (of_list (_ :: _)) _ _ |- _ => + eapply agree_on_cons in H; destr H + end. + eapply @exec.set. + * match goal with + | H: map.get ?l ?y = Some ?y', + H1: map.get ?l ?y = map.get ?lL ?y + |- map.get ?lL ?y = Some _ => + rewrite H1 in H; eapply H + end. + * match goal with | |- context[compile_post] => unfold compile_post end. - eapply H2 in H4. - 2: eassumption. - * eapply H4. - eaply H2. + repeat match goal with + | H: context[of_list (List.removeb eqb _ _)] |- _ => + rewrite ListSet.of_list_removeb in H + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?y') ?mcH, + H1: map.agree_on (diff (of_list ?used_after) (singleton_set ?x)) ?l ?lL |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' (map.put ?lL ?x ?y') /\ post ?t ?m lH' mcH' => exists (map.put l x y'); exists mcH; split; [ | eapply H ] + end. + match goal with + | H: map.agree_on (diff (of_list ?used_after) (singleton_set ?x)) ?l ?lL |- map.agree_on (of_list ?used_after) (map.put ?l ?x ?y') (map.put ?lL ?x ?y') => + eapply agree_on_diff_of_list_singleton; eapply H + end. + + eapply @exec.skip. + match goal with + | |- context[compile_post] => unfold compile_post + end. match goal with - | H: _ -> exec ?eL (deadAssignment ?used_After + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: existsb (eqb ?x) ?used_after = false, + H2: map.agree_on (of_list ?used_after) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' ?lL /\ + post ?t ?m lH' mcH' + => exists (map.put l x v); exists mcH; split; [ | eapply H ] + end. + match goal with + | H: existsb (eqb ?x) ?used_after = false, + H1: map.agree_on (of_list ?used_after) ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) ?lL => + eapply agree_on_put_not_in; [ eapply H1 | eapply H ] + end. + - simpl. intros. + repeat match goal with + | H: map.agree_on (of_list (ListSet.list_union _ _ _)) ?l ?lL |- _ => rewrite ListSet.of_list_list_union in H; eapply agree_on_union in H; destr H + end. + eapply @exec.if_true. + + eauto 2 using accessed_vars_bcond_eval. + + eauto 2 using IHexec. + - simpl. intros. + repeat match goal with + | H: map.agree_on (of_list (ListSet.list_union _ _ _)) ?l ?lL |- _ => rewrite ListSet.of_list_list_union in H; eapply agree_on_union in H; destr H + end. + eapply @exec.if_false. + + eauto 2 using accessed_vars_bcond_eval. + + eauto 2 using IHexec. + - intros. + simpl in *. + eapply @exec.loop. + (* All the unsure goals are + about map.agree_on and live *) + + eapply IHexec. + eapply agree_on_subset. + * eapply H7. + * (* The goal here isn't true; see the helper file for attempts. *) + admit. + + intros. + unfold compile_post in H8. + repeat destr H8. + apply H1 in H9. + admit. (* easier; apply eval_bcond equality *) + + intros. + unfold compile_post in *. + inversion H9. + repeat destr H8. + eapply H2 in H10. + 2: admit. (* followes from accessed_vars_bcond *) + exists x. eexists. + split; admit. (* follows from assumptions *) + + intros. + unfold compile_post in H8. + repeat destr H8. + eapply H4 in H10. + 2: admit. (* follows from accessed_vars_bcond *) + * eapply H10. + * admit. (* goal here also might be untrue *) + + intros. + unfold compile_post in * . + repeat destr H8. + eapply H6 in H9. + * eapply H9. + * admit. (* unsure *) + - - * eassumption. - * eapply agree_on_getmany. - eapply agree_on_subset; [ eapply H4 | ]. - rewrite ListSet.of_list_list_union. - eapply subset_union_rl. - eapply subset_ref. - + eassumption. - + unfold compile_post. - intros. - eapply H3 in H5. - destr H5. - destr H5. - pose proof H5 as H5'. - eapply putmany_Some in H5'. - destr H5'. - eexists x0. - split; [ eapply H7 | ]. - intros. - eapply H6 in H8. - exists x. - eexists. - split. - 2: eapply H8. - rewrite ListSet.of_list_list_union in H4. - rewrite of_list_list_diff in H4. - apply agree_on_union in H4. - destr H4. - eapply agree_on_subset; - [ eauto using agree_on_putmany | ]. - eapply subset_trans. - 2: eapply sameset_union_diff. - eapply subset_union_rl. - eapply subset_ref. + eexists. split. + * admit. + * + 13: { intros. simpl. diff --git a/compiler/src/compiler/DeadAssignmentHelper.v b/compiler/src/compiler/DeadAssignmentHelper.v index 13cf03d7..7e6f960c 100644 --- a/compiler/src/compiler/DeadAssignmentHelper.v +++ b/compiler/src/compiler/DeadAssignmentHelper.v @@ -624,4 +624,209 @@ Section WithArguments. reflexivity. Qed. + Lemma subset_of_list_union_diff_singleton: + forall (l: list string) x, + subset (of_list l) + (union (diff (of_list l) (singleton_set x)) + (singleton_set x)). + Proof. + intros. + match goal with + | |- subset (of_list _) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + Qed. + + Lemma agree_on_diff_of_list_singleton: + forall (l: list string) x (m1 m2: locals), + map.agree_on (diff (of_list l) (singleton_set x)) m1 m2 -> + forall v, + map.agree_on (of_list l) (map.put m1 x v) (map.put m2 x v). + Proof. + intros. + eapply agree_on_subset. + - eapply agree_on_put. + 2-3: reflexivity. + eapply H. + - eapply subset_of_list_union_diff_singleton. + Qed. + + Lemma accessed_vars_bcond_eval : + forall (l lL: locals) cond val, + map.agree_on (of_list (accessed_vars_bcond cond)) l lL -> + eval_bcond l cond = Some val -> + eval_bcond lL cond = Some val. + Proof. + intros. + induction cond. + - simpl in *. + repeat (match goal with + | H: match ?c with _ => _ end = Some _ |- _ => + destr c + end; try match goal with + | H: None = Some _ |- _ + => inversion H + end). + repeat match goal with + | H: context[if ?c then _ else _] |- _ => destr c; fwd + end. + + match goal with + | H: map.get ?l ?s = Some ?r, + H1: map.get ?l ?s = Some ?r0 |- _ => + rewrite H in H1; fwd + end. + match goal with + | H: map.agree_on (of_list [?s]) ?l ?lL, + H1: map.get ?l ?s = Some ?r0 |- _ => + rewrite H in H1; [ | constructor; reflexivity ]; + repeat rewrite H1 + end. + reflexivity. + + repeat match goal with + | H: map.agree_on (of_list _) ?l ?lL |- _ => + apply agree_on_cons in H; destr H + end. + repeat match goal with + | H: map.get ?l ?s = map.get ?lL ?s, + H1: map.get ?l ?s = Some ?r0 |- _ => + rewrite H in H1; fwd + end. + reflexivity. + - simpl in *. + repeat (match goal with + | H: match ?c with _ => _ end = Some _ |- _ => + destr c + end; try match goal with + | H: None = Some _ |- _ + => inversion H + end); fwd. + repeat match goal with + | H: map.agree_on (of_list _) ?l ?lL |- _ => + apply agree_on_cons in H; destr H + end; fwd. + repeat match goal with + | H: map.get ?l ?s = map.get ?lL ?s, + H1: map.get ?l ?s = Some ?r0 |- _ => + rewrite H in H1; fwd + end. + reflexivity. + Qed. + + Lemma live_deadassignment': + forall body, + subset + (of_list (live (deadAssignment [] body) [])) + (of_list (live body [])). + Proof. + induction body. + all: try solve [simpl; eapply subset_ref]. + - (* SStackalloc *) + simpl. + repeat rewrite ListSet.of_list_removeb. + eapply subset_diff. + assumption. + - (* SOp *) + simpl. + repeat match goal with + | |- context[match ?c with _ => _ end] => destr c + end. + all: unfold subset; intros. + all: match goal with + | H: ?c \in of_list [] |- _ => inversion H + end. + - simpl. + repeat match goal with + | |- context[match ?c with _ => _ end] => destr c + end. + all: unfold subset; intros. + all: match goal with + | H: ?c \in of_list [] |- _ => inversion H + end. + - simpl. + repeat match goal with + | |- context[match ?c with _ => _ end] => destr c + | |- context[of_list (ListSet.list_union _ _ _)] => + rewrite ListSet.of_list_list_union + end. + eapply subset_union_l. + + eapply subset_union_l. + * eapply subset_union_rl. + eapply subset_union_rl. + eapply IHbody1. + * + Search union subset. + rewrite L + all: unfold subset; intros. + all: match goal with + | H: ?c \in of_list [] |- _ => inversion H + end. + + Search subset diff. + Lemma live_deadassignment: + forall s body, + subset (of_list (live body [])) + (of_list (live (deadAssignment s body) [])). + Proof. + induction s. + - + + Lemma deadassignment_subset: + forall used_after used_after', + subset (of_list used_after) (of_list used_after') -> + forall s, + subset (of_list (live s used_after)) + (of_list (live s used_after')). + Proof. + intros. + induction s; induction used_after. + - (* SLoad, empty used_after *) + simpl. + match goal with + | |- context[if ?c then _ else _] => destr c + end. + + subset + (of_list + (live + (deadAssignment + (ListSet.list_union eqb (accessed_vars_bcond cond) + (ListSet.list_union eqb used_after (live body2 []))) + body1) + (ListSet.list_union eqb (accessed_vars_bcond cond) + (ListSet.list_union eqb used_after (live body2 []))))) + (of_list + (live + (deadAssignment + (ListSet.list_union eqb (accessed_vars_bcond cond) + (ListSet.list_union eqb used_after (live body2 []))) + body1) + (ListSet.list_union eqb (accessed_vars_bcond cond) + (ListSet.list_union eqb used_after + (live + (deadAssignment + (live body1 + (ListSet.list_union eqb + (accessed_vars_bcond cond) + (ListSet.list_union eqb used_after + (live body2 [])))) body2) []))))) End WithArguments. From a1c0de899f519aa1b8e9643e46bb717d2a1e3a6c Mon Sep 17 00:00:00 2001 From: Arthur De Belen Date: Mon, 24 Jul 2023 16:10:54 -0400 Subject: [PATCH 14/14] temp progress commit on DeadAssignment --- compiler/src/compiler/DeadAssignment.v | 58 +++++++++--- compiler/src/compiler/DeadAssignmentDef.v | 5 +- compiler/src/compiler/DeadAssignmentHelper.v | 99 +------------------- 3 files changed, 49 insertions(+), 113 deletions(-) diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v index 54103f59..f1cc861e 100644 --- a/compiler/src/compiler/DeadAssignment.v +++ b/compiler/src/compiler/DeadAssignment.v @@ -21,17 +21,53 @@ Section WithArguments. Context {ext_spec : Semantics.ExtSpec} {ext_spec_ok: Semantics.ext_spec.ok ext_spec}. Local Hint Constructors exec: core. - Create HintDb set_hints. - Hint Resolve + Local Create HintDb set_hints. + Local Hint Resolve subset_diff in_singleton - subset_union_rr : set_hints. + subset_union_rr + subset_union_rl + subset_ref : set_hints. + Local Hint Rewrite ListSet.of_list_list_union : set_hints. + Local Hint Rewrite of_list_list_diff: set_hints. + Local Create HintDb agree_on_hints. + Hint Resolve + agree_on_getmany + agree_on_subset : agree_on_hints. + + (* Ideally `autorewrite* with set_hints` + should be able to replace + + repeat match goal with + | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H + | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H + end. + + But currently it doesn't. *) + + (* + Currently this tactic + match goal with + | |- subset ?x (union ?x ?y) => + eauto with set_hints + end. + doesn't solve it, although this tactic clears the goal: + + match goal with + | |- subset ?x (union ?x ?y) => + eapply subset_union_rl; eapply subset_ref + end. + *) + + Definition compile_post used_after (postH : Semantics.trace -> mem -> locals -> MetricLog -> Prop) : (Semantics.trace -> mem -> locals -> MetricLog -> Prop) := (fun t' m' lL' mcL' => exists lH' mcH', map.agree_on (PropSet.of_list used_after) lH' lL' /\ postH t' m' lH' mcH' ). + + Lemma deadassignment_correct_aux: forall eH eL, deadassignment_functions eH = Success eL -> @@ -65,6 +101,7 @@ Section WithArguments. [ eapply H2 | ] end end. + repeat match goal with | |- context[of_list (ListSet.list_union _ _ _)] => rewrite ListSet.of_list_list_union | |- context[ListSet.list_diff] => rewrite of_list_list_diff @@ -117,8 +154,6 @@ Section WithArguments. (post _ _ lH' _) => exists x; eexists; split; [ | eapply H ] end. - (* miscellaneous set reasoning; - unclear how to automate this across cases *) repeat match goal with | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H @@ -173,7 +208,6 @@ Section WithArguments. => eapply agree_on_getmany; eapply agree_on_subset; [ eapply H | ] end. - (* set reasoning *) repeat match goal with | |- context[of_list (ListSet.list_union _ _ _)] => rewrite ListSet.of_list_list_union | |- context[ListSet.list_diff] => rewrite of_list_list_diff @@ -870,13 +904,13 @@ Section WithArguments. + eauto 2 using IHexec. - intros. simpl in *. + rename IHexec into IH1. + rename H4 into IH2. + rename H6 into IH12. eapply @exec.loop. - (* All the unsure goals are - about map.agree_on and live *) - + eapply IHexec. - eapply agree_on_subset. - * eapply H7. - * (* The goal here isn't true; see the helper file for attempts. *) + + + (* The goal here isn't true; see the helper file for attempts. *) admit. + intros. unfold compile_post in H8. diff --git a/compiler/src/compiler/DeadAssignmentDef.v b/compiler/src/compiler/DeadAssignmentDef.v index 0c447d52..fe2af8ee 100644 --- a/compiler/src/compiler/DeadAssignmentDef.v +++ b/compiler/src/compiler/DeadAssignmentDef.v @@ -50,10 +50,7 @@ Section WithArgs. let deadAssignment' := deadAssignment used_after in match s with | SIf c s1 s2 => SIf c (deadAssignment' s1) (deadAssignment' s2) - | SLoop s1 c s2 => - let used_after_s1 := (list_union String.eqb (accessed_vars_bcond c) (list_union String.eqb used_after (live s2 []))) in - let used_after_s2 := (live s1 used_after_s1) in - SLoop (deadAssignment used_after_s1 s1) c (deadAssignment used_after_s2 s2) + | SLoop _ _ _ => s | SStackalloc v1 sz1 s => SStackalloc v1 sz1 (deadAssignment' s) | SSeq s1 s2 => let s2' := deadAssignment' s2 in diff --git a/compiler/src/compiler/DeadAssignmentHelper.v b/compiler/src/compiler/DeadAssignmentHelper.v index 7e6f960c..aef05540 100644 --- a/compiler/src/compiler/DeadAssignmentHelper.v +++ b/compiler/src/compiler/DeadAssignmentHelper.v @@ -732,101 +732,6 @@ Section WithArguments. reflexivity. Qed. - Lemma live_deadassignment': - forall body, - subset - (of_list (live (deadAssignment [] body) [])) - (of_list (live body [])). - Proof. - induction body. - all: try solve [simpl; eapply subset_ref]. - - (* SStackalloc *) - simpl. - repeat rewrite ListSet.of_list_removeb. - eapply subset_diff. - assumption. - - (* SOp *) - simpl. - repeat match goal with - | |- context[match ?c with _ => _ end] => destr c - end. - all: unfold subset; intros. - all: match goal with - | H: ?c \in of_list [] |- _ => inversion H - end. - - simpl. - repeat match goal with - | |- context[match ?c with _ => _ end] => destr c - end. - all: unfold subset; intros. - all: match goal with - | H: ?c \in of_list [] |- _ => inversion H - end. - - simpl. - repeat match goal with - | |- context[match ?c with _ => _ end] => destr c - | |- context[of_list (ListSet.list_union _ _ _)] => - rewrite ListSet.of_list_list_union - end. - eapply subset_union_l. - + eapply subset_union_l. - * eapply subset_union_rl. - eapply subset_union_rl. - eapply IHbody1. - * - Search union subset. - rewrite L - all: unfold subset; intros. - all: match goal with - | H: ?c \in of_list [] |- _ => inversion H - end. - - Search subset diff. - Lemma live_deadassignment: - forall s body, - subset (of_list (live body [])) - (of_list (live (deadAssignment s body) [])). - Proof. - induction s. - - - - Lemma deadassignment_subset: - forall used_after used_after', - subset (of_list used_after) (of_list used_after') -> - forall s, - subset (of_list (live s used_after)) - (of_list (live s used_after')). - Proof. - intros. - induction s; induction used_after. - - (* SLoad, empty used_after *) - simpl. - match goal with - | |- context[if ?c then _ else _] => destr c - end. - - subset - (of_list - (live - (deadAssignment - (ListSet.list_union eqb (accessed_vars_bcond cond) - (ListSet.list_union eqb used_after (live body2 []))) - body1) - (ListSet.list_union eqb (accessed_vars_bcond cond) - (ListSet.list_union eqb used_after (live body2 []))))) - (of_list - (live - (deadAssignment - (ListSet.list_union eqb (accessed_vars_bcond cond) - (ListSet.list_union eqb used_after (live body2 []))) - body1) - (ListSet.list_union eqb (accessed_vars_bcond cond) - (ListSet.list_union eqb used_after - (live - (deadAssignment - (live body1 - (ListSet.list_union eqb - (accessed_vars_bcond cond) - (ListSet.list_union eqb used_after - (live body2 [])))) body2) []))))) + + End WithArguments.