aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/CSE3analysis.v19
-rw-r--r--backend/CSE3analysisaux.ml39
-rw-r--r--backend/CSE3analysisproof.v26
-rw-r--r--driver/Compiler.v40
4 files changed, 82 insertions, 42 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index b495371d..91064a5d 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -274,11 +274,20 @@ Section OPERATIONS.
Definition oper (dst : reg) (op: sym_op) (args : list reg)
(rel : RELATION.t) : RELATION.t :=
- match rhs_find op (forward_move_l rel args) rel with
- | Some r => RELATION.glb (move r dst rel)
- (oper1 dst op args rel)
- | None => oper1 dst op args rel
- end.
+ if is_smove op
+ then
+ match args with
+ | src::nil =>
+ move (forward_move rel src) dst rel
+ | _ => kill_reg dst rel
+ end
+ else
+ let args' := forward_move_l rel args in
+ match rhs_find op args' rel with
+ | Some r => (* FIXME RELATION.glb ( *) move r dst rel (* )
+ (oper1 dst op args' rel) *)
+ | None => oper1 dst op args' rel
+ end.
Definition clever_kill_store
(chunk : memory_chunk) (addr: addressing) (args : list reg)
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 0260f3b1..e8e608da 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -32,10 +32,10 @@ let print_eq channel (lhs, sop, args) =
Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk)
(PrintOp.print_addressing print_reg) (addr, args);;
-let print_set s =
- Printf.printf "{ ";
- List.iter (fun i -> Printf.printf "%d; " (P.to_int i)) (PSet.elements s);
- Printf.printf "}\n";;
+let pp_set oc s =
+ Printf.fprintf oc "{ ";
+ List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s);
+ Printf.fprintf oc "}";;
let pp_rhs oc (sop, args) =
match sop with
@@ -45,6 +45,16 @@ let pp_rhs oc (sop, args) =
(PrintAST.name_of_chunk chunk)
(PrintOp.print_addressing PrintRTL.reg) (addr, args);;
+let pp_eq oc eq =
+ Printf.fprintf oc "x%d = %a" (P.to_int eq.eq_lhs)
+ pp_rhs (eq.eq_op, eq.eq_args);;
+
+let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x)
+
+let pp_option pp oc = function
+ | None -> output_string oc "none"
+ | Some x -> pp oc x;;
+
let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
let cur_eq_id = ref 0
and cur_catalog = ref PTree.empty
@@ -54,14 +64,21 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
and cur_kill_mem = ref PSet.empty
and cur_moves = ref (PMap.init PSet.empty) in
let eq_find_oracle node eq =
- Hashtbl.find_opt eq_table (flatten_eq eq)
+ let o = Hashtbl.find_opt eq_table (flatten_eq eq) in
+ Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node)
+ pp_eq eq (pp_option pp_P) o;
+ o
and rhs_find_oracle node sop args =
- (* Printf.printf "query for %a\n" pp_rhs (sop, args); *)
- match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with
- | None -> PSet.empty
- | Some s -> s in
+ let o =
+ match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with
+ | None -> PSet.empty
+ | Some s -> s in
+ Printf.printf "@%d: rhs_find %a = %a\n" (P.to_int node) pp_rhs (sop, args)
+ pp_set o;
+ o in
let mutating_eq_find_oracle node eq : P.t option =
let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in
+ let o =
match Hashtbl.find_opt eq_table flat_eq with
| Some x ->
Some x
@@ -88,6 +105,10 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
| _, _ -> ());
Some coq_id
end
+ in
+ Printf.printf "@%d: mutating_eq_find %a -> %a\n" (P.to_int node)
+ pp_eq eq (pp_option pp_P) o;
+ o
in
match
internal_analysis
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 3ea5e078..116353fa 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -778,15 +778,25 @@ Section SOUNDNESS.
intros until v.
intros REL RHS.
unfold oper.
- destruct rhs_find as [src |] eqn:RHS_FIND.
- - apply sem_rel_glb; split.
- + pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
- eapply forward_move_rhs_sound in RHS.
- 2: eassumption.
- rewrite <- (sem_rhs_det SOUND RHS).
- apply move_sound; auto.
+ destruct (is_smove sop).
+ - subst.
+ simpl in RHS.
+ destruct args. contradiction.
+ destruct args. 2: contradiction.
+ cbn in *.
+ subst.
+ rewrite <- (forward_move_sound rel rs m r) by auto.
+ apply move_sound; auto.
+ - destruct rhs_find as [src |] eqn:RHS_FIND.
+ + (* FIXME apply sem_rel_glb; split. *)
+ * pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
+ eapply forward_move_rhs_sound in RHS.
+ 2: eassumption.
+ rewrite <- (sem_rhs_det SOUND RHS).
+ apply move_sound; auto.
+ (* FIXME * apply oper1_sound; auto. *)
+ apply oper1_sound; auto.
- - apply oper1_sound; auto.
+ apply forward_move_rhs_sound; auto.
Qed.
Hint Resolve oper_sound : cse3.
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 3dbd35ce..6a799bd7 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -293,35 +293,35 @@ Theorem transf_c_program_match:
match_prog p tp.
Proof.
intros p tp T.
- unfold transf_c_program, time in T. simpl in T.
- destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate.
- unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
- destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate.
- destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate.
- destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate.
- unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
- destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
- destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
- unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
+ unfold transf_c_program, time in T. cbn in T.
+ destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate.
+ unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T.
+ destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate.
+ destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate.
+ destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate.
+ unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T.
+ destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate.
+ destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate.
+ unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. cbn in T.
set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *.
- destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate.
+ destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; cbn in T; try discriminate.
set (p9 := Renumber.transf_program p8) in *.
- destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate.
+ destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; cbn in T; try discriminate.
set (p11 := total_if optim_constprop Constprop.transf_program p10) in *.
set (p12 := total_if optim_constprop Renumber.transf_program p11) in *.
- destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
+ destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; cbn in T; try discriminate.
set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *.
- destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate.
+ destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; cbn in T; try discriminate.
set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *.
- destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate.
+ destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; cbn in T; try discriminate.
set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *.
- destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate.
- destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate.
+ destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; cbn in T; try discriminate.
+ destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; cbn in T; try discriminate.
set (p17 := Tunneling.tunnel_program p16) in *.
- destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate.
+ destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; cbn in T; try discriminate.
set (p19 := CleanupLabels.transf_program p18) in *.
- destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate.
- destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate.
+ destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; cbn in T; try discriminate.
+ destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; cbn in T; try discriminate.
unfold match_prog; simpl.
exists p1; split. apply SimplExprproof.transf_program_match; auto.
exists p2; split. apply SimplLocalsproof.match_transf_program; auto.
generated by cgit (git 2.34.1) at 2024-06-12 12:57:08 +0000