diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backend/CSE2.v | 115 | ||||
| -rw-r--r-- | backend/CSE3.v | 94 | ||||
| -rw-r--r-- | backend/CSE3analysis.v | 318 | ||||
| -rw-r--r-- | backend/CSE3analysisaux.ml | 94 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 625 | ||||
| -rw-r--r-- | backend/CSE3proof.v | 138 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Compiler.v | 25 | ||||
| -rw-r--r-- | driver/Compopts.v | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 4 | ||||
| -rw-r--r-- | extraction/extraction.v | 12 | ||||
| -rw-r--r-- | lib/HashedSet.v | 1402 | ||||
| -rw-r--r-- | lib/HashedSetaux.ml | 55 | ||||
| -rw-r--r-- | lib/HashedSetaux.mli | 6 | ||||
| -rw-r--r-- | lib/Lattice.v | 110 |
16 files changed, 2876 insertions, 128 deletions
@@ -57,6 +57,7 @@ FLOCQ=\ # General-purpose libraries (in lib/) VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ + HashedSet.v \ Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v @@ -88,6 +89,7 @@ BACKEND=\ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ + CSE3analysis.v CSE3analysisproof.v CSE3.v CSE3proof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ diff --git a/backend/CSE2.v b/backend/CSE2.v index d5444e3b..efa70b40 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -29,7 +29,7 @@ Proof. decide equality. Defined. -Module RELATION. +Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Definition t := (PTree.t sym_val). Definition eq (r1 r2 : t) := @@ -138,119 +138,6 @@ Qed. End RELATION. -Module Type SEMILATTICE_WITHOUT_BOTTOM. - - Parameter t: Type. - Parameter eq: t -> t -> Prop. - Axiom eq_refl: forall x, eq x x. - Axiom eq_sym: forall x y, eq x y -> eq y x. - Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Parameter beq: t -> t -> bool. - Axiom beq_correct: forall x y, beq x y = true -> eq x y. - Parameter ge: t -> t -> Prop. - Axiom ge_refl: forall x y, eq x y -> ge x y. - Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Parameter lub: t -> t -> t. - Axiom ge_lub_left: forall x y, ge (lub x y) x. - Axiom ge_lub_right: forall x y, ge (lub x y) y. - -End SEMILATTICE_WITHOUT_BOTTOM. - -Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). - Definition t := option L.t. - Definition eq (a b : t) := - match a, b with - | None, None => True - | Some x, Some y => L.eq x y - | Some _, None | None, Some _ => False - end. - - Lemma eq_refl: forall x, eq x x. - Proof. - unfold eq; destruct x; trivial. - apply L.eq_refl. - Qed. - - Lemma eq_sym: forall x y, eq x y -> eq y x. - Proof. - unfold eq; destruct x; destruct y; trivial. - apply L.eq_sym. - Qed. - - Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Proof. - unfold eq; destruct x; destruct y; destruct z; trivial. - - apply L.eq_trans. - - contradiction. - Qed. - - Definition beq (x y : t) := - match x, y with - | None, None => true - | Some x, Some y => L.beq x y - | Some _, None | None, Some _ => false - end. - - Lemma beq_correct: forall x y, beq x y = true -> eq x y. - Proof. - unfold beq, eq. - destruct x; destruct y; trivial; try congruence. - apply L.beq_correct. - Qed. - - Definition ge (x y : t) := - match x, y with - | None, Some _ => False - | _, None => True - | Some a, Some b => L.ge a b - end. - - Lemma ge_refl: forall x y, eq x y -> ge x y. - Proof. - unfold eq, ge. - destruct x; destruct y; trivial. - apply L.ge_refl. - Qed. - - Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Proof. - unfold ge. - destruct x; destruct y; destruct z; trivial; try contradiction. - apply L.ge_trans. - Qed. - - Definition bot: t := None. - Lemma ge_bot: forall x, ge x bot. - Proof. - unfold ge, bot. - destruct x; trivial. - Qed. - - Definition lub (a b : t) := - match a, b with - | None, _ => b - | _, None => a - | (Some x), (Some y) => Some (L.lub x y) - end. - - Lemma ge_lub_left: forall x y, ge (lub x y) x. - Proof. - unfold ge, lub. - destruct x; destruct y; trivial. - - apply L.ge_lub_left. - - apply L.ge_refl. - apply L.eq_refl. - Qed. - - Lemma ge_lub_right: forall x y, ge (lub x y) y. - Proof. - unfold ge, lub. - destruct x; destruct y; trivial. - - apply L.ge_lub_right. - - apply L.ge_refl. - apply L.eq_refl. - Qed. -End ADD_BOTTOM. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). diff --git a/backend/CSE3.v b/backend/CSE3.v new file mode 100644 index 00000000..d67a7a87 --- /dev/null +++ b/backend/CSE3.v @@ -0,0 +1,94 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps CSE2deps. +Require Import CSE3analysis HashedSet. + +Axiom preanalysis : RTL.function -> analysis_hints. + +Definition run f := preanalysis f. + +Section REWRITE. + Context {ctx : eq_context}. + +Definition find_op_in_fmap fmap pc op args := + match fmap with + | None => None + | Some map => + match PMap.get pc map with + | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel + | None => None + end + end. + +Definition find_load_in_fmap fmap pc chunk addr args := + match fmap with + | None => None + | Some map => + match PMap.get pc map with + | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel + | None => None + end + end. + +Definition forward_move_b (rb : RB.t) (x : reg) := + match rb with + | None => x + | Some rel => forward_move (ctx := ctx) rel x + end. + +Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := + match fmap with + | None => x + | Some inv => forward_move_b (PMap.get pc inv) x + end. + +Definition subst_args fmap pc := List.map (subst_arg fmap pc). + +Definition transf_instr (fmap : option (PMap.t RB.t)) + (pc: node) (instr: instruction) := + match instr with + | Iop op args dst s => + let args' := subst_args fmap pc args in + match find_op_in_fmap fmap pc op args' with + | None => Iop op args' dst s + | Some src => Iop Omove (src::nil) dst s + end + | Iload trap chunk addr args dst s => + let args' := subst_args fmap pc args in + match find_load_in_fmap fmap pc chunk addr args' with + | None => Iload trap chunk addr args' dst s + | Some src => Iop Omove (src::nil) dst s + end + | Istore chunk addr args src s => + Istore chunk addr (subst_args fmap pc args) src s + | Icall sig ros args dst s => + Icall sig ros (subst_args fmap pc args) dst s + | Itailcall sig ros args => + Itailcall sig ros (subst_args fmap pc args) + | Icond cond args s1 s2 => + Icond cond (subst_args fmap pc args) s1 s2 + | Ijumptable arg tbl => + Ijumptable (subst_arg fmap pc arg) tbl + | Ireturn (Some arg) => + Ireturn (Some (subst_arg fmap pc arg)) + | _ => instr + end. +End REWRITE. + +Definition transf_function (f: function) : function := + let ctx := context_from_hints (preanalysis f) in + let invariants := internal_analysis (ctx := ctx) f in + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.map (transf_instr (ctx := ctx) invariants) f.(fn_code); + fn_entrypoint := f.(fn_entrypoint) |}. + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v new file mode 100644 index 00000000..18aa33b1 --- /dev/null +++ b/backend/CSE3analysis.v @@ -0,0 +1,318 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps CSE2deps. +Require Import HashedSet. +Require List. + +Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. + Definition t := PSet.t. + Definition eq (x : t) (y : t) := x = y. + + Lemma eq_refl: forall x, eq x x. + Proof. + unfold eq. trivial. + Qed. + + Lemma eq_sym: forall x y, eq x y -> eq y x. + Proof. + unfold eq. congruence. + Qed. + + Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Proof. + unfold eq. congruence. + Qed. + + Definition beq (x y : t) := if PSet.eq x y then true else false. + + Lemma beq_correct: forall x y, beq x y = true -> eq x y. + Proof. + unfold beq. + intros. + destruct PSet.eq; congruence. + Qed. + + Definition ge (x y : t) := (PSet.is_subset x y) = true. + + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge. + intros. + subst y. + apply PSet.is_subset_spec. + trivial. + Qed. + + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge. + intros. + rewrite PSet.is_subset_spec in *. + intuition. + Qed. + + Definition lub := PSet.inter. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold ge, lub. + intros. + apply PSet.is_subset_spec. + intro. + rewrite PSet.ginter. + rewrite andb_true_iff. + intuition. + Qed. + + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold ge, lub. + intros. + apply PSet.is_subset_spec. + intro. + rewrite PSet.ginter. + rewrite andb_true_iff. + intuition. + Qed. + + Definition top := PSet.empty. +End RELATION. + +Module RB := ADD_BOTTOM(RELATION). +Module DS := Dataflow_Solver(RB)(NodeSetForward). + +Inductive sym_op : Type := +| SOp : operation -> sym_op +| SLoad : memory_chunk -> addressing -> sym_op. + +Definition eq_dec_sym_op : forall s s' : sym_op, {s = s'} + {s <> s'}. +Proof. + generalize eq_operation. + generalize eq_addressing. + generalize chunk_eq. + decide equality. +Defined. + +Definition eq_dec_args : forall l l' : list reg, { l = l' } + { l <> l' }. +Proof. + apply List.list_eq_dec. + exact peq. +Defined. + +Record equation := + mkequation + { eq_lhs : reg; + eq_op : sym_op; + eq_args : list reg }. + +Definition eq_dec_equation : + forall eq eq' : equation, {eq = eq'} + {eq <> eq'}. +Proof. + generalize peq. + generalize eq_dec_sym_op. + generalize eq_dec_args. + decide equality. +Defined. + +Definition eq_id := node. + +Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := + Regmap.set i (PSet.add j (Regmap.get i m)) m. + +Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) := + List.fold_left (fun already i => add_i_j i j already) ilist m. + +Definition get_reg_kills (eqs : PTree.t equation) : + Regmap.t PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation) => + add_i_j (eq_lhs eq) eqno + (add_ilist_j (eq_args eq) eqno already)) eqs + (PMap.init PSet.empty). + +Definition eq_depends_on_mem eq := + match eq_op eq with + | SLoad _ _ => true + | SOp op => op_depends_on_memory op + end. + +Definition get_mem_kills (eqs : PTree.t equation) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation) => + if eq_depends_on_mem eq + then PSet.add eqno already + else already) eqs PSet.empty. + +Definition is_move (op : operation) : + { op = Omove } + { op <> Omove }. +Proof. + destruct op; try (right ; congruence). + left; trivial. +Qed. + +Definition is_smove (sop : sym_op) : + { sop = SOp Omove } + { sop <> SOp Omove }. +Proof. + destruct sop; try (right ; congruence). + destruct (is_move o). + - left; congruence. + - right; congruence. +Qed. + +Definition get_moves (eqs : PTree.t equation) : + Regmap.t PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation) => + if is_smove (eq_op eq) + then add_i_j (eq_lhs eq) eqno already + else already) eqs (PMap.init PSet.empty). + +Record eq_context := mkeqcontext + { eq_catalog : eq_id -> option equation; + eq_find_oracle : node -> equation -> option eq_id; + eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; + eq_kill_reg : reg -> PSet.t; + eq_kill_mem : unit -> PSet.t; + eq_moves : reg -> PSet.t }. + +Section OPERATIONS. + Context {ctx : eq_context}. + + Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_reg ctx r). + + Definition kill_mem (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_mem ctx tt). + + Definition pick_source (l : list reg) := (* todo: take min? *) + match l with + | h::t => Some h + | nil => None + end. + + Definition forward_move (rel : RELATION.t) (x : reg) : reg := + match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with + | None => x + | Some eqno => + match eq_catalog ctx eqno with + | Some eq => + if is_smove (eq_op eq) && peq x (eq_lhs eq) + then + match eq_args eq with + | src::nil => src + | _ => x + end + else x + | _ => x + end + end. + + Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := + List.map (forward_move rel). + + Section PER_NODE. + Variable no : node. + + Definition eq_find (eq : equation) := + match eq_find_oracle ctx no eq with + | Some id => + match eq_catalog ctx id with + | Some eq' => if eq_dec_equation eq eq' then Some id else None + | None => None + end + | None => None + end. + + + Definition rhs_find (sop : sym_op) (args : list reg) (rel : RELATION.t) : option reg := + match pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel)) with + | None => None + | Some src => + match eq_catalog ctx src with + | None => None + | Some eq => + if eq_dec_sym_op sop (eq_op eq) && eq_dec_args args (eq_args eq) + then Some (eq_lhs eq) + else None + end + end. + + Definition oper2 (dst : reg) (op: sym_op)(args : list reg) + (rel : RELATION.t) : RELATION.t := + let rel' := kill_reg dst rel in + match eq_find {| eq_lhs := dst; + eq_op := op; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => rel' + end. + + Definition oper1 (dst : reg) (op: sym_op) (args : list reg) + (rel : RELATION.t) : RELATION.t := + if List.in_dec peq dst args + then kill_reg dst rel + else oper2 dst op args rel. + + + Definition move (src dst : reg) (rel : RELATION.t) : RELATION.t := + match eq_find {| eq_lhs := dst; + eq_op := SOp Omove; + eq_args:= src::nil |} with + | Some eq_id => PSet.add eq_id (kill_reg dst rel) + | None => kill_reg dst rel + end. + + 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 => move r dst rel + | None => oper1 dst op args rel + end. + + End PER_NODE. + +Definition apply_instr no instr (rel : RELATION.t) : RB.t := + match instr with + | Inop _ + | Icond _ _ _ _ + | Ijumptable _ _ => Some rel + | Istore chunk addr args _ _ => Some (kill_mem rel) + | Iop op args dst _ => Some (oper no dst (SOp op) args rel) + | Iload trap chunk addr args dst _ => Some (oper no dst (SLoad chunk addr) args rel) + | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) + | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) + | Itailcall _ _ _ | Ireturn _ => RB.bot + end. + +Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := + match ro with + | None => None + | Some x => + match code ! pc with + | None => RB.bot + | Some instr => apply_instr pc instr x + end + end. + +Definition internal_analysis (f : RTL.function) := DS.fixpoint + (RTL.fn_code f) RTL.successors_instr + (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). + +End OPERATIONS. + +Record analysis_hints := + mkanalysis_hints + { hint_eq_catalog : PTree.t equation; + hint_eq_find_oracle : node -> equation -> option eq_id; + hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }. + +Definition context_from_hints (hints : analysis_hints) := + let eqs := hint_eq_catalog hints in + let reg_kills := get_reg_kills eqs in + let mem_kills := get_mem_kills eqs in + let moves := get_moves eqs in + {| + eq_catalog := fun eq_id => PTree.get eq_id eqs; + eq_find_oracle := hint_eq_find_oracle hints ; + eq_rhs_oracle := hint_eq_rhs_oracle hints; + eq_kill_reg := fun reg => PMap.get reg reg_kills; + eq_kill_mem := fun _ => mem_kills; + eq_moves := fun reg => PMap.get reg moves + |}. diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml new file mode 100644 index 00000000..f3c7d9b9 --- /dev/null +++ b/backend/CSE3analysisaux.ml @@ -0,0 +1,94 @@ +open CSE3analysis +open Maps +open HashedSet +open Camlcoq + +let flatten_eq eq = + ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);; + +let imp_add_i_j s i j = + s := PMap.set i (PSet.add j (PMap.get i !s)) !s;; + +let string_of_chunk = function + | AST.Mint8signed -> "int8signed" + | AST.Mint8unsigned -> "int8unsigned" + | AST.Mint16signed -> "int16signed" + | AST.Mint16unsigned -> "int16unsigned" + | AST.Mint32 -> "int32" + | AST.Mint64 -> "int64" + | AST.Mfloat32 -> "float32" + | AST.Mfloat64 -> "float64" + | AST.Many32 -> "any32" + | AST.Many64 -> "any64";; + +let print_reg channel i = + Printf.fprintf channel "r%d" i;; + +let print_eq channel (lhs, sop, args) = + match sop with + | SOp op -> + Printf.printf "%a = %a\n" print_reg lhs (PrintOp.print_operation print_reg) (op, args) + | SLoad(chunk, addr) -> + 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 preanalysis (f : RTL.coq_function) = + let cur_eq_id = ref 0 + and cur_catalog = ref PTree.empty + and eq_table = Hashtbl.create 100 + and rhs_table = Hashtbl.create 100 + and cur_kill_reg = ref (PMap.init PSet.empty) + 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) + and rhs_find_oracle node sop args = + match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with + | None -> PSet.empty + | Some s -> s 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 + match Hashtbl.find_opt eq_table flat_eq with + | Some x -> + Some x + | None -> + (* TODO print_eq stderr flat_eq; *) + incr cur_eq_id; + let id = !cur_eq_id in + let coq_id = P.of_int id in + begin + Hashtbl.add eq_table flat_eq coq_id; + (cur_catalog := PTree.set coq_id eq !cur_catalog); + Hashtbl.add rhs_table (flat_eq_op, flat_eq_args) + (PSet.add coq_id + (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with + | None -> PSet.empty + | Some s -> s)); + List.iter + (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) + (eq.eq_lhs :: eq.eq_args); + (if eq_depends_on_mem eq + then cur_kill_mem := PSet.add coq_id !cur_kill_mem); + (match eq.eq_op, eq.eq_args with + | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id + | _, _ -> ()); + Some coq_id + end + in + ignore + (internal_analysis + { eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog); + eq_find_oracle = mutating_eq_find_oracle; + eq_rhs_oracle = rhs_find_oracle ; + eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); + eq_kill_mem = (fun () -> !cur_kill_mem); + eq_moves = (fun reg -> PMap.get reg !cur_moves) + } f); + { hint_eq_catalog = !cur_catalog; + hint_eq_find_oracle= eq_find_oracle; + hint_eq_rhs_oracle = rhs_find_oracle };; diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v new file mode 100644 index 00000000..f805d2b8 --- /dev/null +++ b/backend/CSE3analysisproof.v @@ -0,0 +1,625 @@ + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet. +Require Import Lia. + +Lemma subst_args_notin : + forall (rs : regset) dst v args, + ~ In dst args -> + (rs # dst <- v) ## args = rs ## args. +Proof. + induction args; simpl; trivial. + intro NOTIN. + destruct (peq a dst). + { + subst a. + intuition congruence. + } + rewrite Regmap.gso by congruence. + f_equal. + apply IHargs. + intuition congruence. +Qed. + +Lemma add_i_j_adds : forall i j m, + PSet.contains (Regmap.get i (add_i_j i j m)) j = true. +Proof. + intros. + unfold add_i_j. + rewrite Regmap.gss. + auto with pset. +Qed. +Hint Resolve add_i_j_adds: cse3. + +Lemma add_i_j_monotone : forall i j i' j' m, + PSet.contains (Regmap.get i' m) j' = true -> + PSet.contains (Regmap.get i' (add_i_j i j m)) j' = true. +Proof. + intros. + unfold add_i_j. + destruct (peq i i'). + - subst i'. + rewrite Regmap.gss. + destruct (peq j j'). + + subst j'. + apply PSet.gadds. + + eauto with pset. + - rewrite Regmap.gso. + assumption. + congruence. +Qed. + +Hint Resolve add_i_j_monotone: cse3. + +Lemma add_ilist_j_monotone : forall ilist j i' j' m, + PSet.contains (Regmap.get i' m) j' = true -> + PSet.contains (Regmap.get i' (add_ilist_j ilist j m)) j' = true. +Proof. + induction ilist; simpl; intros until m; intro CONTAINS; auto with cse3. +Qed. +Hint Resolve add_ilist_j_monotone: cse3. + +Lemma add_ilist_j_adds : forall ilist j m, + forall i, In i ilist -> + PSet.contains (Regmap.get i (add_ilist_j ilist j m)) j = true. +Proof. + induction ilist; simpl; intros until i; intro IN. + contradiction. + destruct IN as [HEAD | TAIL]; subst; auto with cse3. +Qed. +Hint Resolve add_ilist_j_adds: cse3. + +Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : + Regmap.t PSet.t := + List.fold_left (fun already (item : eq_id * equation) => + add_i_j (eq_lhs (snd item)) (fst item) + (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. + +Lemma xlget_kills_monotone : + forall eqs m i j, + PSet.contains (Regmap.get i m) j = true -> + PSet.contains (Regmap.get i (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + auto with cse3. +Qed. + +Hint Resolve xlget_kills_monotone : cse3. + +Lemma xlget_kills_has_lhs : + forall eqs m lhs sop args j, + In (j, {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |}) eqs -> + PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros until j. + intro HEAD_TAIL. + destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. + - auto with cse3. + - eapply IHeqs. eassumption. +Qed. +Hint Resolve xlget_kills_has_lhs : cse3. + +Lemma xlget_kills_has_arg : + forall eqs m lhs sop arg args j, + In (j, {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |}) eqs -> + In arg args -> + PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros until j. + intros HEAD_TAIL ARG. + destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. + - auto with cse3. + - eapply IHeqs; eassumption. +Qed. + +Hint Resolve xlget_kills_has_arg : cse3. + +Lemma get_kills_has_lhs : + forall eqs lhs sop args j, + PTree.get j eqs = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + PSet.contains (Regmap.get lhs (get_reg_kills eqs)) j = true. +Proof. + unfold get_reg_kills. + intros. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : Regmap.t PSet.t) (p : positive * equation) => + add_i_j (eq_lhs (snd p)) (fst p) + (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + eapply xlget_kills_has_lhs. + apply PTree.elements_correct. + eassumption. +Qed. + +Lemma get_kills_has_arg : + forall eqs lhs sop arg args j, + PTree.get j eqs = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + In arg args -> + PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true. +Proof. + unfold get_reg_kills. + intros. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : Regmap.t PSet.t) (p : positive * equation) => + add_i_j (eq_lhs (snd p)) (fst p) + (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + eapply xlget_kills_has_arg. + - apply PTree.elements_correct. + eassumption. + - assumption. +Qed. + +Hint Resolve get_kills_has_arg : cse3. + +Definition eq_involves (eq : equation) (i : reg) := + i = (eq_lhs eq) \/ In i (eq_args eq). + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + + Context {ctx : eq_context}. + + Definition sem_rhs (sop : sym_op) (args : list reg) + (rs : regset) (m : mem) (v' : val) := + match sop with + | SOp op => + match eval_operation genv sp op (rs ## args) m with + | Some v => v' = v + | None => False + end + | SLoad chunk addr => + match + match eval_addressing genv sp addr (rs ## args) with + | Some a => Mem.loadv chunk m a + | None => None + end + with + | Some dat => v' = dat + | None => v' = default_notrap_load_value chunk + end + end. + + Definition sem_eq (eq : equation) (rs : regset) (m : mem) := + sem_rhs (eq_op eq) (eq_args eq) rs m (rs # (eq_lhs eq)). + + Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) := + forall i eq, + PSet.contains rel i = true -> + eq_catalog ctx i = Some eq -> + sem_eq eq rs m. + + Hypothesis ctx_kill_reg_has_lhs : + forall lhs sop args j, + eq_catalog ctx j = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + PSet.contains (eq_kill_reg ctx lhs) j = true. + + Hypothesis ctx_kill_reg_has_arg : + forall lhs sop args j, + eq_catalog ctx j = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + forall arg, + In arg args -> + PSet.contains (eq_kill_reg ctx arg) j = true. + + Hypothesis ctx_kill_mem_has_depends_on_mem : + forall lhs op args j, + eq_catalog ctx j = Some {| eq_lhs := lhs; + eq_op := SOp op; + eq_args:= args |} -> + op_depends_on_memory op = true -> + PSet.contains (eq_kill_mem ctx tt) j = true. + + Hypothesis ctx_kill_mem_has_load : + forall lhs chunk addr args j, + eq_catalog ctx j = Some {| eq_lhs := lhs; + eq_op := SLoad chunk addr; + eq_args:= args |} -> + PSet.contains (eq_kill_mem ctx tt) j = true. + + Theorem kill_reg_sound : + forall rel rs m dst v, + (sem_rel rel rs m) -> + (sem_rel (kill_reg (ctx:=ctx) dst rel) (rs#dst <- v) m). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_reg. + intros until v. + intros REL i eq. + specialize REL with (i := i) (eq0 := eq). + destruct eq as [lhs sop args]; simpl. + specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + specialize ctx_kill_reg_has_arg with (lhs := lhs) (sop := sop) (args := args) (j := i) (arg := dst). + intuition. + rewrite PSet.gsubtract in H. + rewrite andb_true_iff in H. + rewrite negb_true_iff in H. + intuition. + simpl in *. + assert ({In dst args} + {~In dst args}) as IN_ARGS. + { + apply List.in_dec. + apply peq. + } + destruct IN_ARGS as [IN_ARGS | NOTIN_ARGS]. + { intuition. + congruence. + } + destruct (peq dst lhs). + { + congruence. + } + rewrite subst_args_notin by assumption. + destruct sop. + - destruct (eval_operation genv sp o rs ## args m) as [ev | ]; trivial. + rewrite Regmap.gso by congruence. + assumption. + - rewrite Regmap.gso by congruence. + assumption. + Qed. + + Hint Resolve kill_reg_sound : cse3. + + Theorem kill_reg_sound2 : + forall rel rs m dst, + (sem_rel rel rs m) -> + (sem_rel (kill_reg (ctx:=ctx) dst rel) rs m). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_reg. + intros until dst. + intros REL i eq. + specialize REL with (i := i) (eq0 := eq). + destruct eq as [lhs sop args]; simpl. + specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + specialize ctx_kill_reg_has_arg with (lhs := lhs) (sop := sop) (args := args) (j := i) (arg := dst). + intuition. + rewrite PSet.gsubtract in H. + rewrite andb_true_iff in H. + rewrite negb_true_iff in H. + intuition. + Qed. + + Lemma pick_source_sound : + forall (l : list reg), + match pick_source l with + | Some x => In x l + | None => True + end. + Proof. + unfold pick_source. + destruct l; simpl; trivial. + left; trivial. + Qed. + + Hint Resolve pick_source_sound : cse3. + + Theorem forward_move_sound : + forall rel rs m x, + (sem_rel rel rs m) -> + rs # (forward_move (ctx := ctx) rel x) = rs # x. + Proof. + unfold sem_rel, forward_move. + intros until x. + intro REL. + pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT. + destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))). + 2: reflexivity. + destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. + 2: reflexivity. + specialize REL with (i := r) (eq0 := eq). + destruct (is_smove (eq_op eq)) as [MOVE | ]. + 2: reflexivity. + destruct (peq x (eq_lhs eq)). + 2: reflexivity. + simpl. + subst x. + rewrite PSet.elements_spec in ELEMENT. + rewrite PSet.ginter in ELEMENT. + rewrite andb_true_iff in ELEMENT. + unfold sem_eq in REL. + rewrite MOVE in REL. + simpl in REL. + destruct (eq_args eq) as [ | h t]. + reflexivity. + destruct t. + 2: reflexivity. + simpl in REL. + intuition congruence. + Qed. + + Hint Resolve forward_move_sound : cse3. + + Theorem forward_move_l_sound : + forall rel rs m l, + (sem_rel rel rs m) -> + rs ## (forward_move_l (ctx := ctx) rel l) = rs ## l. + Proof. + induction l; simpl; intros; trivial. + erewrite forward_move_sound by eassumption. + intuition congruence. + Qed. + + Hint Resolve forward_move_l_sound : cse3. + + Theorem kill_mem_sound : + forall rel rs m m', + (sem_rel rel rs m) -> + (sem_rel (kill_mem (ctx:=ctx) rel) rs m'). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_mem. + intros until m'. + intros REL i eq. + specialize REL with (i := i) (eq0 := eq). + intros SUBTRACT CATALOG. + rewrite PSet.gsubtract in SUBTRACT. + rewrite andb_true_iff in SUBTRACT. + intuition. + destruct (eq_op eq) as [op | chunk addr] eqn:OP. + - specialize ctx_kill_mem_has_depends_on_mem with (lhs := eq_lhs eq) (op := op) (args := eq_args eq) (j := i). + rewrite (op_depends_on_memory_correct genv sp op) with (m2 := m). + assumption. + destruct (op_depends_on_memory op) in *; trivial. + rewrite ctx_kill_mem_has_depends_on_mem in H0; trivial. + discriminate H0. + rewrite <- OP. + rewrite CATALOG. + destruct eq; reflexivity. + - specialize ctx_kill_mem_has_load with (lhs := eq_lhs eq) (chunk := chunk) (addr := addr) (args := eq_args eq) (j := i). + destruct eq as [lhs op args]; simpl in *. + rewrite negb_true_iff in H0. + rewrite OP in CATALOG. + intuition. + congruence. + Qed. + + Hint Resolve kill_mem_sound : cse3. + + Theorem eq_find_sound: + forall no eq id, + eq_find (ctx := ctx) no eq = Some id -> + eq_catalog ctx id = Some eq. + Proof. + unfold eq_find. + intros. + destruct (eq_find_oracle ctx no eq) as [ id' | ]. + 2: discriminate. + destruct (eq_catalog ctx id') as [eq' |] eqn:CATALOG. + 2: discriminate. + destruct (eq_dec_equation eq eq'). + 2: discriminate. + congruence. + Qed. + + Hint Resolve eq_find_sound : cse3. + + Theorem rhs_find_sound: + forall no sop args rel src rs m, + sem_rel rel rs m -> + rhs_find (ctx := ctx) no sop args rel = Some src -> + sem_rhs sop args rs m (rs # src). + Proof. + unfold rhs_find, sem_rel, sem_eq. + intros until m. + intros REL FIND. + pose proof (pick_source_sound (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel))) as SOURCE. + destruct (pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel))) as [ src' | ]. + 2: discriminate. + rewrite PSet.elements_spec in SOURCE. + rewrite PSet.ginter in SOURCE. + rewrite andb_true_iff in SOURCE. + destruct (eq_catalog ctx src') as [eq | ] eqn:CATALOG. + 2: discriminate. + specialize REL with (i := src') (eq0 := eq). + destruct (eq_dec_sym_op sop (eq_op eq)). + 2: discriminate. + destruct (eq_dec_args args (eq_args eq)). + 2: discriminate. + simpl in FIND. + intuition congruence. + Qed. + + Hint Resolve rhs_find_sound : cse3. + + Theorem forward_move_rhs_sound : + forall sop args rel rs m v, + (sem_rel rel rs m) -> + (sem_rhs sop args rs m v) -> + (sem_rhs sop (forward_move_l (ctx := ctx) rel args) rs m v). + Proof. + intros until v. + intros REL RHS. + destruct sop; simpl in *. + all: erewrite forward_move_l_sound by eassumption; assumption. + Qed. + + Hint Resolve forward_move_rhs_sound : cse3. + + Lemma arg_not_replaced: + forall (rs : regset) dst v args, + ~ In dst args -> + (rs # dst <- v) ## args = rs ## args. + Proof. + induction args; simpl; trivial. + intuition. + f_equal; trivial. + apply Regmap.gso; congruence. + Qed. + + Lemma sem_rhs_depends_on_args_only: + forall sop args rs dst m v, + sem_rhs sop args rs m v -> + ~ In dst args -> + sem_rhs sop args (rs # dst <- v) m v. + Proof. + unfold sem_rhs. + intros. + rewrite arg_not_replaced by assumption. + assumption. + Qed. + + Lemma replace_sound: + forall no eqno dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + ~ In dst args -> + eq_find (ctx := ctx) no + {| eq_lhs := dst; + eq_op := sop; + eq_args:= args |} = Some eqno -> + sem_rel (PSet.add eqno (kill_reg (ctx := ctx) dst rel)) (rs # dst <- v) m. + Proof. + intros until v. + intros REL RHS NOTIN FIND i eq CONTAINS CATALOG. + destruct (peq i eqno). + - subst i. + rewrite eq_find_sound with (no := no) (eq0 := {| eq_lhs := dst; eq_op := sop; eq_args := args |}) in CATALOG by exact FIND. + clear FIND. + inv CATALOG. + unfold sem_eq. + simpl in *. + rewrite Regmap.gss. + apply sem_rhs_depends_on_args_only; auto. + - rewrite PSet.gaddo in CONTAINS by congruence. + eapply kill_reg_sound; eauto. + Qed. + + Lemma sem_rhs_det: + forall {sop} {args} {rs} {m} {v} {v'}, + sem_rhs sop args rs m v -> + sem_rhs sop args rs m v' -> + v = v'. + Proof. + intros until v'. intro SEMv. + destruct sop; simpl in *. + - destruct eval_operation. + congruence. + contradiction. + - destruct eval_addressing. + + destruct Mem.loadv; congruence. + + congruence. + Qed. + + Theorem oper2_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + not (In dst args) -> + sem_rhs sop args rs m v -> + sem_rel (oper2 (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + unfold oper2. + intros until v. + intros REL NOTIN RHS. + pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := sop; eq_args := args |}) as EQ_FIND_SOUND. + destruct eq_find. + 2: auto with cse3; fail. + specialize EQ_FIND_SOUND with (id := e). + intuition. + intros i eq CONTAINS. + destruct (peq i e). + { subst i. + rewrite H. + clear H. + intro Z. + inv Z. + unfold sem_eq. + simpl. + rewrite Regmap.gss. + apply sem_rhs_depends_on_args_only; auto. + } + rewrite PSet.gaddo in CONTAINS by congruence. + apply (kill_reg_sound rel rs m dst v REL i eq); auto. + Qed. + + Hint Resolve oper2_sound : cse3. + + Theorem oper1_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + sem_rel (oper1 (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + intros. + unfold oper1. + destruct in_dec; auto with cse3. + Qed. + + Hint Resolve oper1_sound : cse3. + + Lemma move_sound : + forall no : node, + forall rel : RELATION.t, + forall src dst : reg, + forall rs m, + sem_rel rel rs m -> + sem_rel (move (ctx:=ctx) no src dst rel) (rs # dst <- (rs # src)) m. + Proof. + unfold move. + intros until m. + intro REL. + pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND. + destruct eq_find. + - intros i eq CONTAINS. + destruct (peq i e). + + subst i. + rewrite (EQ_FIND_SOUND e) by trivial. + intro Z. + inv Z. + unfold sem_eq. + simpl. + destruct (peq src dst). + * subst dst. + reflexivity. + * rewrite Regmap.gss. + rewrite Regmap.gso by congruence. + reflexivity. + + intros. + rewrite PSet.gaddo in CONTAINS by congruence. + apply (kill_reg_sound rel rs m dst (rs # src) REL i); auto. + - apply kill_reg_sound; auto. + Qed. + + Hint Resolve move_sound : cse3. + + Theorem oper_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + sem_rel (oper (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + intros until v. + intros REL RHS. + unfold oper. + destruct rhs_find as [src |] eqn:RHS_FIND. + - 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. + - apply oper1_sound; auto. + Qed. + + Hint Resolve oper_sound : cse3. +End SOUNDNESS. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v new file mode 100644 index 00000000..408b3cee --- /dev/null +++ b/backend/CSE3proof.v @@ -0,0 +1,138 @@ +(* +Replace available expressions by the register containing their value. + +Proofs. + +David Monniaux, CNRS, VERIMAG + *) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE3 CSE3analysis CSE3analysisproof. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. +End SOUNDNESS. + + +Definition match_prog (p tp: RTL.program) := + match_program (fun cu f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. apply match_transform_program; auto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof (Genv.find_funct_transf TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (transf_fundef f). +Proof (Genv.find_funct_ptr_transf TRANSL). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_transf TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). + +Lemma sig_preserved: + forall f, funsig (transf_fundef f) = funsig f. +Proof. + destruct f; trivial. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + find_function tge ros rs = Some (transf_fundef fd). +Proof. + unfold find_function; intros. destruct ros as [r|id]. + eapply functions_translated; eauto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. +Qed. + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := +| match_frames_intro: forall res f sp pc rs, + (* (forall m : mem, + forall vres, (fmap_sem' sp m (forward_map f) pc rs # res <- vres)) -> *) + match_frames (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). + +Inductive match_states: RTL.state -> RTL.state -> Prop := + | match_regular_states: forall stk f sp pc rs m stk' + (STACKS: list_forall2 match_frames stk stk'), + (* (fmap_sem' sp m (forward_map f) pc rs) -> *) + match_states (State stk f sp pc rs m) + (State stk' (transf_function f) sp pc rs m) + | match_callstates: forall stk f args m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Callstate stk f args m) + (Callstate stk' (transf_fundef f) args m) + | match_returnstates: forall stk v m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Returnstate stk v m) + (Returnstate stk' v m). + + +Lemma step_simulation: + forall S1 t S2, RTL.step ge S1 t S2 -> + forall S1', match_states S1 S1' -> + exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. +Proof. +Admitted. +Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. +Proof. + intros. inv H. econstructor; split. + econstructor. + eapply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. + eapply function_ptr_translated; eauto. + rewrite <- H3; apply sig_preserved. + constructor. constructor. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_step. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 79c0bce0..7e3b23d8 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -27,6 +27,7 @@ let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fcse2 = ref true +let option_fcse3 = ref true let option_fredundancy = ref true let option_fduplicate = ref 0 let option_finvertcond = ref true diff --git a/driver/Compiler.v b/driver/Compiler.v index da19a0b9..c2428d94 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -43,6 +43,7 @@ Require Constprop. Require CSE. Require ForwardMoves. Require CSE2. +Require CSE3. Require Deadcode. Require Unusedglob. Require Allnontrap. @@ -68,6 +69,7 @@ Require Constpropproof. Require CSEproof. Require ForwardMovesproof. Require CSE2proof. +Require CSE3proof. Require Deadcodeproof. Require Unusedglobproof. Require Allnontrapproof. @@ -144,14 +146,16 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 7) @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 10) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 11) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 12) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 13) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -259,6 +263,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) @@ -306,8 +311,9 @@ Proof. 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. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p13ter := total_if optim_CSE3 CSE3.transf_program p13bis) in *. + 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. 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. @@ -331,7 +337,8 @@ Proof. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. + exists p13ter; split. apply total_if_match. apply CSE3proof.transf_program_match. + exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. @@ -392,7 +399,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -422,6 +429,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. + eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. diff --git a/driver/Compopts.v b/driver/Compopts.v index b4b9f30d..1f952164 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -43,6 +43,9 @@ Parameter optim_CSE: unit -> bool. (** Flag -fcse2. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE2: unit -> bool. +(** Flag -fcse3. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE3: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 43aedf50..12b61d86 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -196,6 +196,7 @@ Processing options: (<n>=0: none, <n>=1: limited, <n>=2: full; default is full) -fcse Perform common subexpression elimination [on] -fcse2 Perform inter-loop common subexpression elimination [on] + -fcse3 Perform inter-loop common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= <optim> Perform postpass scheduling with the specified optimization [list] @@ -265,7 +266,7 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; - option_fcse; option_fcse2; + option_fcse; option_fcse2; option_fcse3; option_fpostpass; option_fredundancy; option_finline; option_finline_functions_called_once; ] @@ -391,6 +392,7 @@ let cmdline_actions = @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse @ f_opt "cse2" option_fcse2 + @ f_opt "cse3" option_fcse3 @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] diff --git a/extraction/extraction.v b/extraction/extraction.v index ba6b080b..79393cf8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -36,6 +36,9 @@ Require Parser. Require Initializers. Require Asmaux. +Require CSE3. +Require CSE3analysis. + (* Standard lib *) Require Import ExtrOcamlBasic. Require Import ExtrOcamlString. @@ -111,6 +114,8 @@ Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". Extract Constant Compopts.optim_CSE2 => "fun _ -> !Clflags.option_fcse2". +Extract Constant Compopts.optim_CSE3 => + "fun _ -> !Clflags.option_fcse3". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => @@ -158,6 +163,12 @@ Extract Constant Cabs.loc => Extract Inlined Constant Cabs.string => "String.t". Extract Constant Cabs.char_code => "int64". +Extract Inlined Constant CSE3.preanalysis => "CSE3analysisaux.preanalysis". + +Extract Inductive HashedSet.PSet_internals.pset => "HashedSetaux.pset" [ "HashedSetaux.empty" "HashedSetaux.node" ] "HashedSetaux.pset_match". + +Extract Inlined Constant HashedSet.PSet_internals.pset_eq => "(==)" (* "HashedSetaux.eq" *). + (* Processor-specific extraction directives *) Load extractionMachdep. @@ -180,6 +191,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction + CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem CSE3.run Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env diff --git a/lib/HashedSet.v b/lib/HashedSet.v new file mode 100644 index 00000000..00e01612 --- /dev/null +++ b/lib/HashedSet.v @@ -0,0 +1,1402 @@ +Require Import ZArith. +Require Import Bool. +Require Import List. +Require Coq.Logic.Eqdep_dec. + +(* begin from Maps *) +Fixpoint prev_append (i j: positive) {struct i} : positive := + match i with + | xH => j + | xI i' => prev_append i' (xI j) + | xO i' => prev_append i' (xO j) + end. + +Definition prev (i: positive) : positive := + prev_append i xH. + +Lemma prev_append_prev i j: + prev (prev_append i j) = prev_append j i. +Proof. + revert j. unfold prev. + induction i as [i IH|i IH|]. 3: reflexivity. + intros j. simpl. rewrite IH. reflexivity. + intros j. simpl. rewrite IH. reflexivity. +Qed. + +Lemma prev_involutive i : + prev (prev i) = i. +Proof (prev_append_prev i xH). + +Lemma prev_append_inj i j j' : + prev_append i j = prev_append i j' -> j = j'. +Proof. + revert j j'. + induction i as [i Hi|i Hi|]; intros j j' H; auto; + specialize (Hi _ _ H); congruence. +Qed. + +(* end from Maps *) + +Lemma orb_idem: forall b, orb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_idem: forall b, andb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_negb_false: forall b, andb b (negb b) = false. +Proof. + destruct b; reflexivity. +Qed. + +Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pset. + +Module PSet_internals. +Inductive pset : Type := +| Empty : pset +| Node : pset -> bool -> pset -> pset. + +Definition empty := Empty. + +Definition is_empty x := + match x with + | Empty => true + | Node _ _ _ => false + end. + +Fixpoint wf x := + match x with + | Empty => true + | Node b0 f b1 => + (wf b0) && (wf b1) && + ((negb (is_empty b0)) || f || (negb (is_empty b1))) + end. + +Definition iswf x := (wf x)=true. + +Lemma empty_wf : iswf empty. +Proof. + reflexivity. +Qed. + +Definition pset_eq : + forall s s': pset, { s=s' } + { s <> s' }. +Proof. + induction s; destruct s'; repeat decide equality. +Qed. + +Fixpoint contains (s : pset) (i : positive) {struct i} : bool := + match s with + | Empty => false + | Node b0 f b1 => + match i with + | xH => f + | xO ii => contains b0 ii + | xI ii => contains b1 ii + end + end. + +Lemma gempty : + forall i : positive, + contains Empty i = false. +Proof. + destruct i; simpl; reflexivity. +Qed. + +Hint Resolve gempty : pset. +Hint Rewrite gempty : pset. + +Definition node (b0 : pset) (f : bool) (b1 : pset) : pset := + match b0, f, b1 with + | Empty, false, Empty => Empty + | _, _, _ => Node b0 f b1 + end. + +Lemma wf_node : + forall b0 f b1, + iswf b0 -> iswf b1 -> iswf (node b0 f b1). +Proof. + destruct b0; destruct f; destruct b1; simpl. + all: unfold iswf; simpl; intros; trivial. + all: autorewrite with pset; trivial. + all: rewrite H. + all: rewrite H0. + all: reflexivity. +Qed. + +Hint Resolve wf_node: pset. + +Lemma gnode : + forall b0 f b1 i, + contains (node b0 f b1) i = + contains (Node b0 f b1) i. +Proof. + destruct b0; simpl; trivial. + destruct f; simpl; trivial. + destruct b1; simpl; trivial. + intro. + rewrite gempty. + destruct i; simpl; trivial. + all: symmetry; apply gempty. +Qed. + +Hint Rewrite gnode : pset. + +Fixpoint add (i : positive) (s : pset) {struct i} : pset := + match s with + | Empty => + match i with + | xH => Node Empty true Empty + | xO ii => Node (add ii Empty) false Empty + | xI ii => Node Empty false (add ii Empty) + end + | Node b0 f b1 => + match i with + | xH => Node b0 true b1 + | xO ii => Node (add ii b0) f b1 + | xI ii => Node b0 f (add ii b1) + end + end. + +Lemma add_nonempty: + forall i s, is_empty (add i s) = false. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Hint Rewrite add_nonempty : pset. +Hint Resolve add_nonempty : pset. + +Lemma wf_add: + forall i s, (iswf s) -> (iswf (add i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: autorewrite with pset; simpl; trivial. + 1,3: auto with pset. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: intuition. +Qed. + +Hint Resolve wf_add : pset. + +Theorem gadds : + forall i : positive, + forall s : pset, + contains (add i s) i = true. +Proof. + induction i; destruct s; simpl; auto. +Qed. + +Hint Resolve gadds : pset. +Hint Rewrite gadds : pset. + +Theorem gaddo : + forall i j : positive, + forall s : pset, + i <> j -> + contains (add i s) j = contains s j. +Proof. + induction i; destruct j; destruct s; simpl; intro; auto with pset. + 5, 6: congruence. + all: rewrite IHi by congruence. + all: trivial. + all: apply gempty. +Qed. + +Hint Resolve gaddo : pset. + +Fixpoint remove (i : positive) (s : pset) { struct i } : pset := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 false b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => node (remove ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 f (remove ii b1) + end + end. + +Lemma wf_remove : + forall i s, (iswf s) -> (iswf (remove i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: apply wf_node. + all: intuition. + all: apply IHi. + all: assumption. +Qed. + + +Fixpoint remove_noncanon (i : positive) (s : pset) { struct i } : pset := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 false b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node (remove_noncanon ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 f (remove_noncanon ii b1) + end + end. + +Lemma remove_noncanon_same: + forall i j s, (contains (remove i s) j) = (contains (remove_noncanon i s) j). +Proof. + induction i; destruct s; simpl; trivial. + all: rewrite gnode. + 3: reflexivity. + all: destruct j; simpl; trivial. +Qed. + +Lemma remove_empty : + forall i, remove i Empty = Empty. +Proof. + induction i; simpl; trivial. +Qed. + +Hint Rewrite remove_empty : pset. +Hint Resolve remove_empty : pset. + +Lemma gremove_noncanon_s : + forall i : positive, + forall s : pset, + contains (remove_noncanon i s) i = false. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Theorem gremoves : + forall i : positive, + forall s : pset, + contains (remove i s) i = false. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_s. +Qed. + +Hint Resolve gremoves : pset. +Hint Rewrite gremoves : pset. + +Lemma gremove_noncanon_o : + forall i j : positive, + forall s : pset, + i<>j -> + contains (remove_noncanon i s) j = contains s j. +Proof. + induction i; destruct j; destruct s; simpl; intro; trivial. + 1, 2: rewrite IHi by congruence. + 1, 2: reflexivity. + congruence. +Qed. + +Theorem gremoveo : + forall i j : positive, + forall s : pset, + i<>j -> + contains (remove i s) j = contains s j. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_o. + assumption. +Qed. + +Hint Resolve gremoveo : pset. + +Fixpoint union_nonopt (s s' : pset) : pset := + match s, s' with + | Empty, _ => s' + | _, Empty => s + | (Node b0 f b1), (Node b0' f' b1') => + Node (union_nonopt b0 b0') (orb f f') (union_nonopt b1 b1') + end. + +Theorem gunion_nonopt: + forall s s' : pset, + forall j : positive, + (contains (union_nonopt s s')) j = orb (contains s j) (contains s' j). +Proof. + induction s; destruct s'; intro; simpl; autorewrite with pset; simpl; trivial. + destruct j; simpl; trivial. +Qed. + + +Fixpoint union (s s' : pset) : pset := + if pset_eq s s' then s else + match s, s' with + | Empty, _ => s' + | _, Empty => s + | (Node b0 f b1), (Node b0' f' b1') => + Node (union b0 b0') (orb f f') (union b1 b1') + end. + +Lemma union_nonempty1: + forall s s', + (is_empty s) = false -> is_empty (union s s')= false. +Proof. + induction s; destruct s'; simpl; try discriminate. + all: destruct pset_eq; simpl; trivial. +Qed. + +Lemma union_nonempty2: + forall s s', + (is_empty s') = false -> is_empty (union s s')= false. +Proof. + induction s; destruct s'; simpl; try discriminate. + all: destruct pset_eq; simpl; trivial; discriminate. +Qed. + +Hint Resolve union_nonempty1 union_nonempty2 : pset. + +Lemma wf_union : + forall s s', (iswf s) -> (iswf s') -> (iswf (union s s')). +Proof. + induction s; destruct s'; intros; simpl. + all: destruct pset_eq; trivial. + unfold iswf in *. simpl in *. + repeat rewrite andb_true_iff in H. + repeat rewrite andb_true_iff in H0. + rewrite IHs1. + rewrite IHs2. + simpl. + all: intuition. + repeat rewrite orb_true_iff in H2, H3. + repeat rewrite negb_true_iff in H2, H3. + repeat rewrite orb_true_iff. + repeat rewrite negb_true_iff. + intuition auto with pset. +Qed. + +Hint Resolve wf_union : pset. + +Theorem gunion: + forall s s' : pset, + forall j : positive, + (contains (union s s')) j = orb (contains s j) (contains s' j). +Proof. + induction s; destruct s'; intro; simpl. + all: destruct pset_eq as [EQ | NEQ]; try congruence. + all: autorewrite with pset; simpl; trivial. + - rewrite <- EQ. + symmetry. + apply orb_idem. + - destruct j; simpl; trivial. +Qed. + +Fixpoint inter_noncanon (s s' : pset) : pset := + if pset_eq s s' then s else + match s, s' with + | Empty, _ | _, Empty => Empty + | (Node b0 f b1), (Node b0' f' b1') => + Node (inter_noncanon b0 b0') (andb f f') (inter_noncanon b1 b1') + end. + +Lemma ginter_noncanon: + forall s s' : pset, + forall j : positive, + (contains (inter_noncanon s s')) j = andb (contains s j) (contains s' j). +Proof. + induction s; destruct s'; intro; simpl. + all: destruct pset_eq as [EQ | NEQ]; try congruence. + all: autorewrite with pset; simpl; trivial. + - rewrite <- EQ. + symmetry. + apply andb_idem. + - destruct j; simpl; trivial. +Qed. + +Fixpoint inter (s s' : pset) : pset := + if pset_eq s s' then s else + match s, s' with + | Empty, _ | _, Empty => Empty + | (Node b0 f b1), (Node b0' f' b1') => + node (inter b0 b0') (andb f f') (inter b1 b1') + end. + +Lemma wf_inter : + forall s s', (iswf s) -> (iswf s') -> (iswf (inter s s')). +Proof. + induction s; destruct s'; intros; simpl. + all: destruct pset_eq; trivial. + unfold iswf in H, H0. + simpl in H, H0. + repeat rewrite andb_true_iff in H. + repeat rewrite andb_true_iff in H0. + fold (iswf s1) in *. + fold (iswf s2) in *. + intuition. +Qed. + +Hint Resolve wf_inter : pset. + +Lemma inter_noncanon_same: + forall s s' j, (contains (inter s s') j) = (contains (inter_noncanon s s') j). +Proof. + induction s; destruct s'; simpl; trivial. + destruct pset_eq; trivial. + destruct j; rewrite gnode; simpl; auto. +Qed. + +Theorem ginter: + forall s s' : pset, + forall j : positive, + (contains (inter s s')) j = andb (contains s j) (contains s' j). +Proof. + intros. + rewrite inter_noncanon_same. + apply ginter_noncanon. +Qed. + +Hint Resolve ginter gunion : pset. +Hint Rewrite ginter gunion : pset. + +Fixpoint subtract_noncanon (s s' : pset) : pset := + if pset_eq s s' then Empty else + match s, s' with + | Empty, _ => Empty + | _, Empty => s + | (Node b0 f b1), (Node b0' f' b1') => + Node (subtract_noncanon b0 b0') (andb f (negb f')) (subtract_noncanon b1 b1') + end. + +Lemma gsubtract_noncanon: + forall s s' : pset, + forall j : positive, + (contains (subtract_noncanon s s')) j = andb (contains s j) (negb (contains s' j)). +Proof. + induction s; destruct s'; intro; simpl. + all: destruct pset_eq as [EQ | NEQ]; try congruence. + all: autorewrite with pset; simpl; trivial. + - rewrite <- EQ. + symmetry. + apply andb_negb_false. + - destruct j; simpl; trivial. +Qed. + +Fixpoint subtract (s s' : pset) : pset := + if pset_eq s s' then Empty else + match s, s' with + | Empty, _ => Empty + | _, Empty => s + | (Node b0 f b1), (Node b0' f' b1') => + node (subtract b0 b0') (andb f (negb f')) (subtract b1 b1') + end. + +Lemma wf_subtract : + forall s s', (iswf s) -> (iswf s') -> (iswf (subtract s s')). +Proof. + induction s; destruct s'; intros; simpl. + all: destruct pset_eq; trivial. + reflexivity. + + unfold iswf in H, H0. + simpl in H, H0. + + repeat rewrite andb_true_iff in H. + repeat rewrite andb_true_iff in H0. + fold (iswf s1) in *. + fold (iswf s2) in *. + intuition. +Qed. + +Hint Resolve wf_subtract : pset. + +Lemma subtract_noncanon_same: + forall s s' j, (contains (subtract s s') j) = (contains (subtract_noncanon s s') j). +Proof. + induction s; destruct s'; simpl; trivial. + destruct pset_eq; trivial. + destruct j; rewrite gnode; simpl; auto. +Qed. + +Theorem gsubtract: + forall s s' : pset, + forall j : positive, + (contains (subtract s s')) j = andb (contains s j) (negb (contains s' j)). +Proof. + intros. + rewrite subtract_noncanon_same. + apply gsubtract_noncanon. +Qed. + +Hint Resolve gsubtract : pset. +Hint Rewrite gsubtract : pset. + +Lemma wf_is_nonempty : + forall s, iswf s -> is_empty s = false -> exists i, contains s i = true. +Proof. + induction s; simpl; trivial. + discriminate. + intro WF. + unfold iswf in WF. + simpl in WF. + repeat rewrite andb_true_iff in WF. + repeat rewrite orb_true_iff in WF. + repeat rewrite negb_true_iff in WF. + fold (iswf s1) in WF. + fold (iswf s2) in WF. + intuition. + - destruct H5 as [i K]. + exists (xO i). + simpl. + assumption. + - exists xH. + simpl. + assumption. + - destruct H5 as [i K]. + exists (xI i). + simpl. + assumption. +Qed. + +Hint Resolve wf_is_nonempty : pset. + +Lemma wf_is_empty1 : + forall s, iswf s -> (forall i, (contains s i) = false) -> is_empty s = true. +Proof. + induction s; trivial. + intro WF. + unfold iswf in WF. + simpl in WF. + repeat rewrite andb_true_iff in WF. + fold (iswf s1) in WF. + fold (iswf s2) in WF. + intro ALL. + intuition. + exfalso. + repeat rewrite orb_true_iff in H0. + repeat rewrite negb_true_iff in H0. + intuition. + - rewrite H in H0. discriminate. + intro i. + specialize ALL with (xO i). + simpl in ALL. + assumption. + - specialize ALL with xH. + simpl in ALL. + congruence. + - rewrite H3 in H4. discriminate. + intro i. + specialize ALL with (xI i). + simpl in ALL. + assumption. +Qed. + +Hint Resolve wf_is_empty1 : pset. + +Lemma wf_eq : + forall s s', iswf s -> iswf s' -> s <> s' -> + exists i, (contains s i) <> (contains s' i). +Proof. + induction s; destruct s'; intros WF WF' DIFF; simpl. + - congruence. + - assert (exists i, (contains (Node s'1 b s'2) i)= true) as K by auto with pset. + destruct K as [i Z]. + exists i. + rewrite Z. + rewrite gempty. + discriminate. + - assert (exists i, (contains (Node s1 b s2) i)= true) as K by auto with pset. + destruct K as [i Z]. + exists i. + rewrite Z. + rewrite gempty. + discriminate. + - destruct (pset_eq s1 s'1). + + subst s'1. + destruct (pset_eq s2 s'2). + * subst s'2. + exists xH. + simpl. + congruence. + * specialize IHs2 with s'2. + unfold iswf in WF. + simpl in WF. + repeat rewrite andb_true_iff in WF. + fold (iswf s1) in WF. + fold (iswf s2) in WF. + unfold iswf in WF'. + simpl in WF'. + repeat rewrite andb_true_iff in WF'. + fold (iswf s'2) in WF'. + intuition. + destruct H1 as [i K]. + exists (xI i). + simpl. + assumption. + + specialize IHs1 with s'1. + unfold iswf in WF. + simpl in WF. + repeat rewrite andb_true_iff in WF. + fold (iswf s1) in WF. + fold (iswf s2) in WF. + unfold iswf in WF'. + simpl in WF'. + repeat rewrite andb_true_iff in WF'. + fold (iswf s'1) in WF'. + fold (iswf s'2) in WF'. + intuition. + destruct H1 as [i K]. + exists (xO i). + simpl. + assumption. +Qed. + +Theorem eq_correct: + forall s s', + (iswf s) -> (iswf s') -> + (forall i, (contains s i) = (contains s' i)) <-> s = s'. +Proof. + intros s s' WF WF'. + split. + { + intro ALL. + destruct (pset_eq s s') as [ | INEQ]; trivial. + exfalso. + destruct (wf_eq s s' WF WF' INEQ) as [i K]. + specialize ALL with i. + congruence. + } + intro EQ. + subst s'. + trivial. +Qed. + +Lemma wf_irrelevant: + forall s, + forall WF WF' : iswf s, WF = WF'. +Proof. + unfold iswf. + intros. + apply Coq.Logic.Eqdep_dec.eq_proofs_unicity_on. + decide equality. +Qed. + +Fixpoint xelements (s : pset) (i : positive) + (k: list positive) {struct s} + : list positive := + match s with + | Empty => k + | Node b0 false b1 => + xelements b0 (xO i) (xelements b1 (xI i) k) + | Node b0 true b1 => + xelements b0 (xO i) ((prev i) :: xelements b1 (xI i) k) + end. + +Definition elements (m : pset) := xelements m xH nil. + + Remark xelements_append: + forall (m: pset) i k1 k2, + xelements m i (k1 ++ k2) = xelements m i k1 ++ k2. + Proof. + induction m; intros; simpl. + - auto. + - destruct b; rewrite IHm2; rewrite <- IHm1; auto. + Qed. + + Remark xelements_empty: + forall i, xelements Empty i nil = nil. + Proof. + intros; reflexivity. + Qed. + + Remark xelements_node: + forall (m1: pset) o (m2: pset) i, + xelements (Node m1 o m2) i nil = + xelements m1 (xO i) nil + ++ (if o then (prev i) :: nil else nil) + ++ xelements m2 (xI i) nil. + Proof. + intros. simpl. destruct o; simpl; + rewrite <- xelements_append; trivial. + Qed. + + Lemma xelements_incl: + forall (m: pset) (i : positive) k x, + In x k -> In x (xelements m i k). + Proof. + induction m; intros; simpl. + auto. + destruct b. + apply IHm1. simpl; right; auto. + auto. + Qed. + + Lemma xelements_correct: + forall (m: pset) (i j : positive) k, + contains m i=true -> In (prev (prev_append i j)) (xelements m j k). + Proof. + induction m; intros; simpl. + - rewrite gempty in H. discriminate. + - destruct b; destruct i; simpl; simpl in H; auto. + + apply xelements_incl. simpl. + right. auto. + + apply xelements_incl. simpl. + left. trivial. + + apply xelements_incl. auto. + + discriminate. + Qed. + + Theorem elements_correct: + forall (m: pset) (i: positive), + contains m i = true -> In i (elements m). + Proof. + intros m i H. + generalize (xelements_correct m i xH nil H). rewrite prev_append_prev. exact id. + Qed. + + Lemma in_xelements: + forall (m: pset) (i k: positive), + In k (xelements m i nil) -> + exists j, k = prev (prev_append j i) /\ contains m j = true. + Proof. + induction m; intros. + - rewrite xelements_empty in H. contradiction. + - rewrite xelements_node in H. rewrite ! in_app_iff in H. destruct H as [P | [P | P]]. + + specialize IHm1 with (k := k) (i := xO i). + intuition. + destruct H as [j [Q R]]. + exists (xO j). + auto. + + destruct b; simpl in P; intuition auto. subst k. exists xH; auto. + + specialize IHm2 with (k := k) (i := xI i). + intuition. + destruct H as [j [Q R]]. + exists (xI j). + auto. + Qed. + + Theorem elements_complete: + forall (m: pset) (i: positive), + In i (elements m) -> contains m i = true. + Proof. + unfold elements. intros m i H. + destruct (in_xelements m 1 i H) as [j [P Q]]. + rewrite prev_append_prev in P. change i with (prev_append 1 i) in P. + replace j with i in * by (apply prev_append_inj; auto). + assumption. + Qed. + + + Fixpoint xfold {B: Type} (f: B -> positive -> B) + (i: positive) (m: pset) (v: B) {struct m} : B := + match m with + | Empty => v + | Node l false r => + let v1 := xfold f (xO i) l v in + xfold f (xI i) r v1 + | Node l true r => + let v1 := xfold f (xO i) l v in + let v2 := f v1 (prev i) in + xfold f (xI i) r v2 + end. + + Definition fold {B : Type} (f: B -> positive -> B) (m: pset) (v: B) := + xfold f xH m v. + + + Lemma xfold_xelements: + forall {B: Type} (f: B -> positive -> B) m i v l, + List.fold_left f l (xfold f i m v) = + List.fold_left f (xelements m i l) v. + Proof. + induction m; intros; simpl; trivial. + destruct b; simpl. + all: rewrite <- IHm1; simpl; rewrite <- IHm2; trivial. + Qed. + + Theorem fold_spec: + forall {B: Type} (f: B -> positive -> B) (v: B) (m: pset), + fold f m v = + List.fold_left f (elements m) v. + Proof. + intros. unfold fold, elements. rewrite <- xfold_xelements. auto. + Qed. + + Fixpoint is_subset (s s' : pset) {struct s} := + if pset_eq s s' then true else + match s, s' with + | Empty, _ => true + | _, Empty => false + | (Node b0 f b1), (Node b0' f' b1') => + ((negb f) || f') && + (is_subset b0 b0') && + (is_subset b1 b1') + end. + + Theorem is_subset_spec1: + forall s s', + is_subset s s' = true -> + (forall i, contains s i = true -> contains s' i = true). + Proof. + induction s; destruct s'; simpl; intros; trivial. + all: destruct pset_eq. + all: try discriminate. + all: try rewrite gempty in *. + all: try discriminate. + { congruence. + } + repeat rewrite andb_true_iff in H. + repeat rewrite orb_true_iff in H. + repeat rewrite negb_true_iff in H. + specialize IHs1 with (s' := s'1). + specialize IHs2 with (s' := s'2). + intuition. + - destruct i; simpl in *; auto. congruence. + - destruct i; simpl in *; auto. + Qed. + + Theorem is_subset_spec2: + forall s s', + iswf s -> + (forall i, contains s i = true -> contains s' i = true) -> + is_subset s s' = true. + Proof. + induction s; destruct s'; simpl. + all: intro WF. + all: unfold iswf in WF. + all: simpl in WF. + all: repeat rewrite andb_true_iff in WF. + all: destruct pset_eq; trivial. + all: fold (iswf s1) in WF. + all: fold (iswf s2) in WF. + - repeat rewrite orb_true_iff in WF. + repeat rewrite negb_true_iff in WF. + intuition. + + destruct (wf_is_nonempty s1 H2 H1) as [i K]. + specialize H with (xO i). + simpl in H. + auto. + + specialize H with xH. + simpl in H. + auto. + + destruct (wf_is_nonempty s2 H3 H0) as [i K]. + specialize H with (xI i). + simpl in H. + auto. + - intro CONTAINS. + repeat rewrite andb_true_iff. + specialize IHs1 with (s' := s'1). + specialize IHs2 with (s' := s'2). + intuition. + + specialize CONTAINS with xH. + simpl in CONTAINS. + destruct b; destruct b0; intuition congruence. + + apply H. + intros. + specialize CONTAINS with (xO i). + simpl in CONTAINS. + auto. + + apply H3. + intros. + specialize CONTAINS with (xI i). + simpl in CONTAINS. + auto. + Qed. + + Fixpoint xfilter (fn : positive -> bool) + (s : pset) (i : positive) {struct s} : pset := + match s with + | Empty => Empty + | Node b0 f b1 => + node (xfilter fn b0 (xO i)) + (f && (fn (prev i))) + (xfilter fn b1 (xI i)) + end. + + Lemma gxfilter: + forall fn s j i, + contains (xfilter fn s i) j = + contains s j && + (fn (prev (prev_append j i))). + Proof. + induction s; simpl; intros; trivial. + { + rewrite gempty. + trivial. + } + rewrite gnode. + destruct j; simpl; auto. + Qed. + + Definition filter (fn : positive -> bool) m := xfilter fn m xH. + + Lemma gfilter: + forall fn s j, + contains (filter fn s) j = + contains s j && (fn j). + Proof. + intros. + unfold filter. + rewrite gxfilter. + rewrite prev_append_prev. + reflexivity. + Qed. + + Lemma wf_xfilter: + forall fn s j, + iswf s -> iswf (xfilter fn s j). + Proof. + induction s; intros; trivial. + simpl. + unfold iswf in H. + simpl in H. + repeat rewrite andb_true_iff in H. + fold (iswf s1) in H. + fold (iswf s2) in H. + intuition. + Qed. + + Lemma wf_filter: + forall fn s, + iswf s -> iswf (filter fn s). + Proof. + intros. + apply wf_xfilter; auto. + Qed. +End PSet_internals. + +Module Type POSITIVE_SET. +Parameter t : Type. +Parameter empty : t. + +Parameter contains: t -> positive -> bool. + +Axiom gempty : + forall i : positive, + contains empty i = false. + +Parameter add : positive -> t -> t. + +Axiom gaddo : + forall i j : positive, + forall s : t, + i <> j -> + contains (add i s) j = contains s j. + +Axiom gadds : + forall i : positive, + forall s : t, + contains (add i s) i = true. + +Parameter remove : positive -> t -> t. + +Axiom gremoves : + forall i : positive, + forall s : t, + contains (remove i s) i = false. + +Axiom gremoveo : + forall i j : positive, + forall s : t, + i<>j -> + contains (remove i s) j = contains s j. + +Parameter union : t -> t -> t. + +Axiom gunion: + forall s s' : t, + forall j : positive, + (contains (union s s')) j = orb (contains s j) (contains s' j). + +Parameter inter : t -> t -> t. + +Axiom ginter: + forall s s' : t, + forall j : positive, + (contains (inter s s')) j = andb (contains s j) (contains s' j). + +Parameter subtract : t -> t -> t. + +Axiom gsubtract: + forall s s' : t, + forall j : positive, + (contains (subtract s s')) j = andb (contains s j) (negb (contains s' j)). + +Axiom uneq_exists : + forall s s', s <> s' -> + exists i, (contains s i) <> (contains s' i). + +Parameter eq: + forall s s' : t, {s = s'} + {s <> s'}. + +Axiom eq_spec : + forall s s', + (forall i, (contains s i) = (contains s' i)) <-> s = s'. + +Parameter elements : t -> list positive. + +Axiom elements_correct: + forall (m: t) (i: positive), + contains m i = true -> In i (elements m). + +Axiom elements_complete: + forall (m: t) (i: positive), + In i (elements m) -> contains m i = true. + +Axiom elements_spec: + forall (m: t) (i: positive), + In i (elements m) <-> contains m i = true. + +Parameter fold: + forall {B : Type}, + (B -> positive -> B) -> t -> B -> B. + +Axiom fold_spec: + forall {B: Type} (f: B -> positive -> B) (v: B) (m: t), + fold f m v = + List.fold_left f (elements m) v. + +Parameter is_subset : t -> t -> bool. + +Axiom is_subset_spec1: + forall s s', + is_subset s s' = true -> + (forall i, contains s i = true -> contains s' i = true). + +Axiom is_subset_spec2: + forall s s', + (forall i, contains s i = true -> contains s' i = true) -> + is_subset s s' = true. + +Axiom is_subset_spec: + forall s s', + is_subset s s' = true <-> + (forall i, contains s i = true -> contains s' i = true). + +Parameter filter: (positive -> bool) -> t -> t. + +Axiom gfilter: + forall fn s j, + contains (filter fn s) j = + contains s j && (fn j). + +End POSITIVE_SET. + +Module PSet : POSITIVE_SET. + +Record pset : Type := mkpset +{ + pset_x : PSet_internals.pset ; + pset_wf : PSet_internals.wf pset_x = true +}. + +Definition t := pset. + +Program Definition empty : t := mkpset PSet_internals.empty _. + +Definition contains (s : t) (i : positive) := + PSet_internals.contains (pset_x s) i. + +Theorem gempty : + forall i : positive, + contains empty i = false. +Proof. + intro. + unfold empty, contains. + simpl. + auto with pset. +Qed. + +Program Definition add (i : positive) (s : t) := + mkpset (PSet_internals.add i (pset_x s)) _. +Obligation 1. + destruct s. + apply PSet_internals.wf_add. + simpl. + assumption. +Qed. + +Theorem gaddo : + forall i j : positive, + forall s : t, + i <> j -> + contains (add i s) j = contains s j. +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Theorem gadds : + forall i : positive, + forall s : pset, + contains (add i s) i = true. +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Program Definition remove (i : positive) (s : t) := + mkpset (PSet_internals.remove i (pset_x s)) _. +Obligation 1. + destruct s. + apply PSet_internals.wf_remove. + simpl. + assumption. +Qed. + +Theorem gremoves : + forall i : positive, + forall s : pset, + contains (remove i s) i = false. +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Theorem gremoveo : + forall i j : positive, + forall s : pset, + i<>j -> + contains (remove i s) j = contains s j. +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Program Definition union (s s' : t) := + mkpset (PSet_internals.union (pset_x s) (pset_x s')) _. +Obligation 1. + destruct s; destruct s'. + apply PSet_internals.wf_union; simpl; assumption. +Qed. + +Theorem gunion: + forall s s' : pset, + forall j : positive, + (contains (union s s')) j = orb (contains s j) (contains s' j). +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Program Definition inter (s s' : t) := + mkpset (PSet_internals.inter (pset_x s) (pset_x s')) _. +Obligation 1. + destruct s; destruct s'. + apply PSet_internals.wf_inter; simpl; assumption. +Qed. + +Theorem ginter: + forall s s' : pset, + forall j : positive, + (contains (inter s s')) j = andb (contains s j) (contains s' j). +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Program Definition subtract (s s' : t) := + mkpset (PSet_internals.subtract (pset_x s) (pset_x s')) _. +Obligation 1. + destruct s; destruct s'. + apply PSet_internals.wf_subtract; simpl; assumption. +Qed. + +Theorem gsubtract: + forall s s' : pset, + forall j : positive, + (contains (subtract s s')) j = andb (contains s j) (negb (contains s' j)). +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Theorem uneq_exists : + forall s s', s <> s' -> + exists i, (contains s i) <> (contains s' i). +Proof. + destruct s as [s WF]; destruct s' as [s' WF']; simpl. + intro UNEQ. + destruct (PSet_internals.pset_eq s s'). + { subst s'. + pose proof (PSet_internals.wf_irrelevant s WF WF'). + subst WF'. + congruence. + } + unfold contains; simpl. + apply PSet_internals.wf_eq; trivial. +Qed. + +Definition eq: + forall s s' : t, {s = s'} + {s <> s'}. +Proof. + destruct s as [s WF]. + destruct s' as [s' WF']. + destruct (PSet_internals.pset_eq s s'); simpl. + { + subst s'. + left. + pose proof (PSet_internals.wf_irrelevant s WF WF'). + subst WF'. + reflexivity. + } + right. + congruence. +Qed. + +Theorem eq_spec : + forall s s', + (forall i, (contains s i) = (contains s' i)) <-> s = s'. +Proof. + intros. + split; intro K. + 2: subst s'; reflexivity. + destruct s as [s WF]. + destruct s' as [s' WF']. + unfold contains in K. + simpl in K. + fold (PSet_internals.iswf s) in WF. + fold (PSet_internals.iswf s') in WF'. + assert (s = s'). + { + apply PSet_internals.eq_correct; assumption. + } + subst s'. + pose proof (PSet_internals.wf_irrelevant s WF WF'). + subst WF'. + reflexivity. +Qed. + + +Definition elements (m : t) := PSet_internals.elements (pset_x m). + + +Theorem elements_correct: + forall (m: pset) (i: positive), + contains m i = true -> In i (elements m). +Proof. + destruct m; unfold elements, contains; simpl. + apply PSet_internals.elements_correct. +Qed. + +Theorem elements_complete: + forall (m: pset) (i: positive), + In i (elements m) -> contains m i = true. +Proof. + destruct m; unfold elements, contains; simpl. + apply PSet_internals.elements_complete. +Qed. + + +Theorem elements_spec: + forall (m: pset) (i: positive), + In i (elements m) <-> contains m i = true. +Proof. + intros. split. + - apply elements_complete. + - apply elements_correct. +Qed. + +Definition fold {B : Type} (f : B -> positive -> B) (m : t) (v : B) : B := + PSet_internals.fold f (pset_x m) v. + +Theorem fold_spec: + forall {B: Type} (f: B -> positive -> B) (v: B) (m: pset), + fold f m v = + List.fold_left f (elements m) v. +Proof. + destruct m; unfold fold, elements; simpl. + apply PSet_internals.fold_spec. +Qed. + +Definition is_subset (s s' : t) := PSet_internals.is_subset (pset_x s) (pset_x s'). + +Theorem is_subset_spec1: + forall s s', + is_subset s s' = true -> + (forall i, contains s i = true -> contains s' i = true). +Proof. + unfold is_subset, contains. + intros s s' H. + apply PSet_internals.is_subset_spec1. + assumption. +Qed. + +Theorem is_subset_spec2: + forall s s', + (forall i, contains s i = true -> contains s' i = true) -> + is_subset s s' = true. +Proof. + destruct s; destruct s'; + unfold is_subset, contains; + intros. + apply PSet_internals.is_subset_spec2. + all: simpl. + all: assumption. +Qed. + +Hint Resolve is_subset_spec1 is_subset_spec2 : pset. + +Theorem is_subset_spec: + forall s s', + is_subset s s' = true <-> + (forall i, contains s i = true -> contains s' i = true). +Proof. + intros. + split; + eauto with pset. +Qed. + +Program Definition filter (fn : positive -> bool) (m : t) : t := + (mkpset (PSet_internals.filter fn (pset_x m)) _). +Obligation 1. + apply PSet_internals.wf_filter. + unfold PSet_internals.iswf. + destruct m. + assumption. +Qed. + +Theorem gfilter: + forall fn s j, + contains (filter fn s) j = + contains s j && (fn j). +Proof. + unfold contains, filter. + simpl. + intros. + apply PSet_internals.gfilter. +Qed. +End PSet. + +Hint Resolve PSet.gaddo PSet.gadds PSet.gremoveo PSet.gremoves PSet.gunion PSet.ginter PSet.gsubtract PSet.gfilter PSet.is_subset_spec1 PSet.is_subset_spec2 : pset. + +Hint Rewrite PSet.gadds PSet.gremoves PSet.gunion PSet.ginter PSet.gsubtract PSet.gfilter : pset. diff --git a/lib/HashedSetaux.ml b/lib/HashedSetaux.ml new file mode 100644 index 00000000..8329c249 --- /dev/null +++ b/lib/HashedSetaux.ml @@ -0,0 +1,55 @@ +type uid = int + +let uid_base = min_int +let next_uid = ref (uid_base+1) + +let incr_uid () = + let r = !next_uid in + if r = max_int + then failwith "HashedSet: no more uid" + else next_uid := succ r;; + +let cur_uid () = !next_uid;; + +type pset = + | Empty + | Node of uid * pset * bool * pset;; + +let get_uid = function + | Empty -> uid_base + | Node(uid, _, _, _) -> uid;; + +module HashedPSet = + struct + type t = pset + + let hash = function + | Empty -> 0 + | Node(_, b0, f, b1) -> Hashtbl.hash (get_uid b0, f, get_uid b1);; + + let equal x x' = match x, x' with + | Empty, Empty -> true + | Node(_, b0, f, b1), Node(_, b0', f', b1') -> + b0 == b0' && f == f' && b1 == b1' + | _, _ -> false + end;; + +module PSetHash = Weak.Make(HashedPSet);; + +let htable = PSetHash.create 1000;; + +let qnode b0 f b1 = + let x = Node(cur_uid(), b0, f, b1) in + match PSetHash.find_opt htable x with + | None -> PSetHash.add htable x; incr_uid(); x + | Some y -> y;; + +let node (b0, f, b1) = qnode b0 f b1;; + +let empty = Empty;; + +let pset_match empty_case node_case = function + | Empty -> empty_case () + | Node(_, b0, f, b1) -> node_case b0 f b1;; + +let eq (x : pset) (y : pset) = (x==y);; diff --git a/lib/HashedSetaux.mli b/lib/HashedSetaux.mli new file mode 100644 index 00000000..14beac41 --- /dev/null +++ b/lib/HashedSetaux.mli @@ -0,0 +1,6 @@ +type pset +val qnode : pset -> bool -> pset -> pset +val node : pset * bool * pset -> pset +val empty : pset +val pset_match : (unit -> 'a) -> (pset -> bool -> pset -> 'a) -> pset -> 'a +val eq : pset -> pset -> bool diff --git a/lib/Lattice.v b/lib/Lattice.v index 85fc03f3..8ea736ad 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -30,7 +30,8 @@ Local Unset Case Analysis Schemes. [bot], and an upper bound operation [lub]. Note that we do not demand that [lub] computes the least upper bound. *) -Module Type SEMILATTICE. + +Module Type SEMILATTICE_WITHOUT_BOTTOM. Parameter t: Type. Parameter eq: t -> t -> Prop. @@ -42,25 +43,124 @@ Module Type SEMILATTICE. Parameter ge: t -> t -> Prop. Axiom ge_refl: forall x y, eq x y -> ge x y. Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Parameter bot: t. - Axiom ge_bot: forall x, ge x bot. Parameter lub: t -> t -> t. Axiom ge_lub_left: forall x y, ge (lub x y) x. Axiom ge_lub_right: forall x y, ge (lub x y) y. +End SEMILATTICE_WITHOUT_BOTTOM. + +Module Type SEMILATTICE. + Include SEMILATTICE_WITHOUT_BOTTOM. + Parameter bot: t. + Axiom ge_bot: forall x, ge x bot. End SEMILATTICE. (** A semi-lattice ``with top'' is similar, but also has a greatest element [top]. *) Module Type SEMILATTICE_WITH_TOP. - Include SEMILATTICE. Parameter top: t. Axiom ge_top: forall x, ge top x. - End SEMILATTICE_WITH_TOP. + +Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM) <: SEMILATTICE. + Definition t := option L.t. + Definition eq (a b : t) := + match a, b with + | None, None => True + | Some x, Some y => L.eq x y + | Some _, None | None, Some _ => False + end. + + Lemma eq_refl: forall x, eq x x. + Proof. + unfold eq; destruct x; trivial. + apply L.eq_refl. + Qed. + + Lemma eq_sym: forall x y, eq x y -> eq y x. + Proof. + unfold eq; destruct x; destruct y; trivial. + apply L.eq_sym. + Qed. + + Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Proof. + unfold eq; destruct x; destruct y; destruct z; trivial. + - apply L.eq_trans. + - contradiction. + Qed. + + Definition beq (x y : t) := + match x, y with + | None, None => true + | Some x, Some y => L.beq x y + | Some _, None | None, Some _ => false + end. + + Lemma beq_correct: forall x y, beq x y = true -> eq x y. + Proof. + unfold beq, eq. + destruct x; destruct y; trivial; try congruence. + apply L.beq_correct. + Qed. + + Definition ge (x y : t) := + match x, y with + | None, Some _ => False + | _, None => True + | Some a, Some b => L.ge a b + end. + + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge. + destruct x; destruct y; trivial. + apply L.ge_refl. + Qed. + + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge. + destruct x; destruct y; destruct z; trivial; try contradiction. + apply L.ge_trans. + Qed. + + Definition bot: t := None. + Lemma ge_bot: forall x, ge x bot. + Proof. + unfold ge, bot. + destruct x; trivial. + Qed. + + Definition lub (a b : t) := + match a, b with + | None, _ => b + | _, None => a + | (Some x), (Some y) => Some (L.lub x y) + end. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold ge, lub. + destruct x; destruct y; trivial. + - apply L.ge_lub_left. + - apply L.ge_refl. + apply L.eq_refl. + Qed. + + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold ge, lub. + destruct x; destruct y; trivial. + - apply L.ge_lub_right. + - apply L.ge_refl. + apply L.eq_refl. + Qed. +End ADD_BOTTOM. + (** * Semi-lattice over maps *) Set Implicit Arguments. |