diff options
48 files changed, 4497 insertions, 184 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,10 +89,12 @@ 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 \ ForwardMoves.v ForwardMovesproof.v \ + FirstNop.v \ Allnontrap.v Allnontrapproof.v \ Allocation.v Allocproof.v \ Tunneling.v Tunnelingproof.v \ diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index e54673dd..e7edcf0d 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -133,7 +133,9 @@ module Target : TARGET = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 03e06a65..54af7cd5 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -147,7 +147,9 @@ struct let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data(i) -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" diff --git a/backend/CSE2.v b/backend/CSE2.v index 900a7517..dc206c75 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..352cc895 --- /dev/null +++ b/backend/CSE3.v @@ -0,0 +1,93 @@ +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. +Require Import RTLtyping. + +Local Open Scope error_monad_scope. + +Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints. + +Section REWRITE. + Context {ctx : eq_context}. + +Definition find_op_in_fmap fmap pc op args := + match PMap.get pc fmap with + | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel + | None => None + end. + +Definition find_load_in_fmap fmap pc chunk addr args := + match PMap.get pc fmap with + | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel + | None => None + 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 : PMap.t RB.t) (pc : node) (x : reg) : reg := + forward_move_b (PMap.get pc fmap) x. + +Definition forward_move_l_b (rb : RB.t) (xl : list reg) := + match rb with + | None => xl + | Some rel => forward_move_l (ctx := ctx) rel xl + end. + +Definition subst_args fmap pc xl := + forward_move_l_b (PMap.get pc fmap) xl. + +Definition transf_instr (fmap : 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 (if is_trivial_op op then None else 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 expected => + Icond cond (subst_args fmap pc args) s1 s2 expected + | 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) : res function := + do tenv <- type_function f; + let (invariants, hints) := preanalysis tenv f in + let ctx := context_from_hints hints in + if check_inductiveness (ctx:=ctx) f tenv invariants + then + OK {| 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) |} + else Error (msg "cse3: not inductive"). + +Definition transf_fundef (fd: fundef) : res fundef := + AST.transf_partial_fundef transf_function fd. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v new file mode 100644 index 00000000..90ce4ce7 --- /dev/null +++ b/backend/CSE3analysis.v @@ -0,0 +1,403 @@ +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 Compopts. + +Definition typing_env := reg -> typ. + +Definition loadv_storev_compatible_type + (chunk : memory_chunk) (ty : typ) : bool := + match chunk, ty with + | Mint32, Tint + | Mint64, Tlong + | Mfloat32, Tsingle + | Mfloat64, Tfloat => true + | _, _ => false + end. + +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. + + Definition clever_kill_store + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := + PSet.subtract rel + (PSet.filter + (fun eqno => + match eq_catalog ctx eqno with + | None => false + | Some eq => + match eq_op eq with + | SOp op => true + | SLoad chunk' addr' => + may_overlap chunk addr args chunk' addr' (eq_args eq) + end + end) + (PSet.inter rel (eq_kill_mem ctx tt))). + + Definition store2 + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := + if Compopts.optim_CSE3_alias_analysis tt + then clever_kill_store chunk addr args src rel + else kill_mem rel. + + Definition store1 + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) (ty: typ) + (rel : RELATION.t) : RELATION.t := + let rel' := store2 chunk addr args src rel in + if loadv_storev_compatible_type chunk ty + then + match eq_find {| eq_lhs := src; + eq_op := SLoad chunk addr; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => rel' + end + else rel'. + + Definition store + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) (ty: typ) + (rel : RELATION.t) : RELATION.t := + store1 chunk addr (forward_move_l rel args) src ty rel. + + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := + match instr with + | Inop _ + | Icond _ _ _ _ _ + | Ijumptable _ _ => Some rel + | Istore chunk addr args src _ => + Some (store chunk addr args src (tenv src) rel) + | Iop op args dst _ => Some (oper dst (SOp op) args rel) + | Iload trap chunk addr args dst _ => Some (oper 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. + End PER_NODE. + +Definition apply_instr' (tenv : typing_env) 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 tenv instr x + end + end. + +Definition invariants := PMap.t RB.t. + +Definition rel_leb (x y : RELATION.t) : bool := (PSet.is_subset y x). + +Definition relb_leb (x y : RB.t) : bool := + match x, y with + | None, _ => true + | (Some _), None => false + | (Some x), (Some y) => rel_leb x y + end. + +Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: invariants) := + (RB.beq (Some RELATION.top) (PMap.get (fn_entrypoint fn) inv)) && + PTree_Properties.for_all (fn_code fn) + (fun pc instr => + match PMap.get pc inv with + | None => true + | Some rel => + let rel' := apply_instr pc tenv instr rel in + List.forallb + (fun pc' => relb_leb rel' (PMap.get pc' inv)) + (RTL.successors_instr instr) + end). + +Definition internal_analysis + (tenv : typing_env) + (f : RTL.function) : option invariants := DS.fixpoint + (RTL.fn_code f) RTL.successors_instr + (apply_instr' tenv (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..23e20ea8 --- /dev/null +++ b/backend/CSE3analysisaux.ml @@ -0,0 +1,97 @@ +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 (tenv : typing_env) (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 + match + 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) + } tenv f + with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3" + | Some invariants -> + invariants, + { 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..b87ec92c --- /dev/null +++ b/backend/CSE3analysisproof.v @@ -0,0 +1,926 @@ + +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 RTLtyping. +Require Import Lia. + +Lemma rel_leb_correct: + forall x x', + rel_leb x x' = true <-> RELATION.ge x' x. +Proof. + unfold rel_leb, RELATION.ge. + split; auto. +Qed. + +Hint Resolve rel_leb_correct : cse3. + +Lemma relb_leb_correct: + forall x x', + relb_leb x x' = true <-> RB.ge x' x. +Proof. + unfold relb_leb, RB.ge. + destruct x; destruct x'; split; trivial; try contradiction; discriminate. +Qed. + +Hint Resolve relb_leb_correct : cse3. + +Theorem loadv_storev_really_same: + forall chunk: memory_chunk, + forall m1: mem, + forall addr v: val, + forall m2: mem, + forall ty : typ, + forall TYPE: Val.has_type v ty, + forall STORE: Mem.storev chunk m1 addr v = Some m2, + forall COMPATIBLE: loadv_storev_compatible_type chunk ty = true, + Mem.loadv chunk m2 addr = Some v. +Proof. + intros. + rewrite Mem.loadv_storev_same with (m1:=m1) (v:=v) by assumption. + f_equal. + destruct chunk; destruct ty; try discriminate. + all: destruct v; trivial; try contradiction. + all: unfold Val.load_result, Val.has_type in *. + all: destruct Archi.ptr64; trivial; discriminate. +Qed. + +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. + + +Definition xlget_mem_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := +(fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) + 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_mem_kills_monotone : + forall eqs m j, + PSet.contains m j = true -> + PSet.contains (xlget_mem_kills eqs m) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + destruct eq_depends_on_mem. + - apply IHeqs. + destruct (peq (fst a) j). + + subst j. apply PSet.gadds. + + rewrite PSet.gaddo by congruence. + trivial. + - auto. +Qed. + +Hint Resolve xlget_mem_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. + +Hint Resolve get_kills_has_lhs : cse3. + +Lemma context_from_hints_get_kills_has_lhs : + forall hints lhs sop args j, + PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + PSet.contains (eq_kill_reg (context_from_hints hints) lhs) j = true. +Proof. + intros; simpl. + eapply get_kills_has_lhs. + eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_lhs : cse3. + +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. + +Lemma context_from_hints_get_kills_has_arg : + forall hints lhs sop arg args j, + PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + In arg args -> + PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_arg; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_arg : cse3. + +Lemma xlget_kills_has_eq_depends_on_mem : + forall eqs eq j m, + In (j, eq) eqs -> + eq_depends_on_mem eq = true -> + PSet.contains (xlget_mem_kills eqs m) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros. + destruct H. + { subst a. + simpl. + rewrite H0. + apply xlget_mem_kills_monotone. + apply PSet.gadds. + } + eauto. +Qed. + +Hint Resolve xlget_kills_has_eq_depends_on_mem : cse3. + +Lemma get_kills_has_eq_depends_on_mem : + forall eqs eq j, + PTree.get j eqs = Some eq -> + eq_depends_on_mem eq = true -> + PSet.contains (get_mem_kills eqs) j = true. +Proof. + intros. + unfold get_mem_kills. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) + (PTree.elements eqs) PSet.empty) + with (xlget_mem_kills (PTree.elements eqs) PSet.empty). + eapply xlget_kills_has_eq_depends_on_mem. + apply PTree.elements_correct. + eassumption. + trivial. +Qed. + +Lemma context_from_hints_get_kills_has_eq_depends_on_mem : + forall hints eq j, + PTree.get j (hint_eq_catalog hints) = Some eq -> + eq_depends_on_mem eq = true -> + PSet.contains (eq_kill_mem (context_from_hints hints) tt) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_eq_depends_on_mem; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3. + +Definition eq_involves (eq : equation) (i : reg) := + i = (eq_lhs eq) \/ In i (eq_args eq). + +Section SOUNDNESS. + Context {F V : Type}. + Context {genv: Genv.t F V}. + Context {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 eq j, + eq_catalog ctx j = Some eq -> + eq_depends_on_mem eq = true -> + 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 (eq0 := eq) (j := i). + unfold eq_depends_on_mem in ctx_kill_mem_has_depends_on_mem. + rewrite OP in ctx_kill_mem_has_depends_on_mem. + 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. + - specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i). + destruct eq as [lhs op args]; simpl in *. + rewrite OP in ctx_kill_mem_has_depends_on_mem. + 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. + + + Theorem clever_kill_store_sound: + forall chunk addr args a src rel rs m m', + sem_rel rel rs m -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs # src) = Some m' -> + sem_rel (clever_kill_store (ctx:=ctx) chunk addr args src rel) rs m'. + Proof. + unfold clever_kill_store. + intros until m'. intros REL ADDR STORE i eq CONTAINS CATALOG. + autorewrite with pset in CONTAINS. + destruct (PSet.contains rel i) eqn:RELi; simpl in CONTAINS. + 2: discriminate. + rewrite CATALOG in CONTAINS. + unfold sem_rel in REL. + specialize REL with (i := i) (eq0 := eq). + destruct eq; simpl in *. + unfold sem_eq in *. + simpl in *. + destruct eq_op as [op' | chunk' addr']; simpl. + - destruct (op_depends_on_memory op') eqn:DEPENDS. + + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + discriminate. + + rewrite op_depends_on_memory_correct with (m2:=m); trivial. + apply REL; auto. + - simpl in REL. + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + simpl in CONTAINS. + rewrite negb_true_iff in CONTAINS. + destruct (eval_addressing genv sp addr' rs ## eq_args) as [a'|] eqn:ADDR'. + + erewrite may_overlap_sound with (chunk:=chunk) (addr:=addr) (args:=args) (chunk':=chunk') (addr':=addr') (args':=eq_args); try eassumption. + apply REL; auto. + + apply REL; auto. + Qed. + + Hint Resolve clever_kill_store_sound : cse3. + + Theorem store2_sound: + forall chunk addr args a src rel rs m m', + sem_rel rel rs m -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs # src) = Some m' -> + sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m'. + Proof. + unfold store2. + intros. + destruct (Compopts.optim_CSE3_alias_analysis tt); eauto with cse3. + Qed. + + Hint Resolve store2_sound : cse3. + + Theorem store1_sound: + forall no chunk addr args a src rel tenv rs m m', + sem_rel rel rs m -> + wt_regset tenv rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs#src) = Some m' -> + sem_rel (store1 (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + Proof. + unfold store1. + intros until m'. + intros REL WT ADDR STORE. + assert (sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m') as REL' by eauto with cse3. + destruct loadv_storev_compatible_type eqn:COMPATIBLE. + 2: auto; fail. + destruct eq_find as [eq_id | ] eqn:FIND. + 2: auto; fail. + intros i eq CONTAINS CATALOG. + destruct (peq i eq_id). + { subst i. + rewrite eq_find_sound with (no:=no) (eq0:={| eq_lhs := src; eq_op := SLoad chunk addr; eq_args := args |}) in CATALOG; trivial. + inv CATALOG. + unfold sem_eq. + simpl. + rewrite ADDR. + rewrite loadv_storev_really_same with (m1:=m) (v:=rs#src) (ty:=(tenv src)); trivial. + } + unfold sem_rel in REL'. + rewrite PSet.gaddo in CONTAINS by congruence. + eauto. + Qed. + + Hint Resolve store1_sound : cse3. + + Theorem store_sound: + forall no chunk addr args a src rel tenv rs m m', + sem_rel rel rs m -> + wt_regset tenv rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs#src) = Some m' -> + sem_rel (store (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + Proof. + unfold store. + intros until m'. + intros REL WT ADDR STORE. + rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. + rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + apply store1_sound with (a := a) (m := m); trivial. + rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + assumption. + Qed. + + Hint Resolve store_sound : cse3. + + Section INDUCTIVENESS. + Variable fn : RTL.function. + Variable tenv : typing_env. + Variable inv: invariants. + + Definition is_inductive_step (pc pc' : node) := + forall instr, + PTree.get pc (fn_code fn) = Some instr -> + In pc' (successors_instr instr) -> + RB.ge (PMap.get pc' inv) + (apply_instr' (ctx:=ctx) tenv (fn_code fn) pc (PMap.get pc inv)). + + Definition is_inductive_allstep := + forall pc pc', is_inductive_step pc pc'. + + Lemma checked_is_inductive_allstep: + (check_inductiveness (ctx:=ctx) fn tenv inv) = true -> + is_inductive_allstep. + Proof. + unfold check_inductiveness, is_inductive_allstep, is_inductive_step. + rewrite andb_true_iff. + rewrite PTree_Properties.for_all_correct. + intros (ENTRYPOINT & ALL). + intros until instr. + intros INSTR IN_SUCC. + specialize ALL with (x := pc) (a := instr). + pose proof (ALL INSTR) as AT_PC. + destruct (inv # pc). + 2: apply RB.ge_bot. + rewrite List.forallb_forall in AT_PC. + unfold apply_instr'. + rewrite INSTR. + apply relb_leb_correct. + auto. + Qed. + + Lemma checked_is_inductive_entry: + (check_inductiveness (ctx:=ctx) fn tenv inv) = true -> + inv # (fn_entrypoint fn) = Some RELATION.top. + Proof. + unfold check_inductiveness, is_inductive_allstep, is_inductive_step. + rewrite andb_true_iff. + intros (ENTRYPOINT & ALL). + apply RB.beq_correct in ENTRYPOINT. + unfold RB.eq, RELATION.eq in ENTRYPOINT. + destruct (inv # (fn_entrypoint fn)) as [rel | ]. + 2: contradiction. + f_equal. + symmetry. + assumption. + Qed. + End INDUCTIVENESS. + + Hint Resolve checked_is_inductive_allstep checked_is_inductive_entry : cse3. +End SOUNDNESS. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v new file mode 100644 index 00000000..19fb20be --- /dev/null +++ b/backend/CSE3proof.v @@ -0,0 +1,875 @@ +(* +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. +Require Import RTLtyping. + + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Section SOUNDNESS. +Variable sp : val. +Variable ctx : eq_context. + +Definition sem_rel_b (rel : RB.t) (rs : regset) (m : mem) := + match rel with + | None => False + | Some rel => sem_rel (ctx:=ctx) (genv:=ge) (sp:=sp) rel rs m + end. + +Lemma forward_move_b_sound : + forall rel rs m x, + (sem_rel_b rel rs m) -> + rs # (forward_move_b (ctx := ctx) rel x) = rs # x. +Proof. + destruct rel as [rel | ]; simpl; intros. + 2: contradiction. + eapply forward_move_sound; eauto. + Qed. + + Lemma forward_move_l_b_sound : + forall rel rs m x, + (sem_rel_b rel rs m) -> + rs ## (forward_move_l_b (ctx := ctx) rel x) = rs ## x. + Proof. + destruct rel as [rel | ]; simpl; intros. + 2: contradiction. + eapply forward_move_l_sound; eauto. + Qed. + + Definition fmap_sem (fmap : PMap.t RB.t) (pc : node) (rs : regset) (m : mem) := + sem_rel_b (PMap.get pc fmap) rs m. + + Lemma subst_arg_ok: + forall invariants, + forall pc, + forall rs, + forall m, + forall arg, + forall (SEM : fmap_sem invariants pc rs m), + rs # (subst_arg (ctx:=ctx) invariants pc arg) = rs # arg. + Proof. + intros. + apply forward_move_b_sound with (m:=m). + assumption. + Qed. + + Lemma subst_args_ok: + forall invariants, + forall pc, + forall rs, + forall m, + forall args, + forall (SEM : fmap_sem invariants pc rs m), + rs ## (subst_args (ctx:=ctx) invariants pc args) = rs ## args. + Proof. + intros. + apply forward_move_l_b_sound with (m:=m). + assumption. + Qed. +End SOUNDNESS. + +Lemma functions_translated: + forall (v: val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. +Proof. + apply (Genv.find_funct_transf_partial TRANSF). +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: RTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof. + apply (Genv.find_funct_ptr_transf_partial TRANSF). +Qed. + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof. + apply (Genv.find_symbol_match TRANSF). +Qed. + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof. + apply (Genv.senv_match TRANSF). +Qed. + +Lemma sig_preserved: + forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. +Proof. + destruct f; simpl; intros. + - monadInv H. + monadInv EQ. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ1. + reflexivity. + - monadInv H. + reflexivity. +Qed. + +Lemma stacksize_preserved: + forall f tf, transf_function f = OK tf -> fn_stacksize tf = fn_stacksize f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma params_preserved: + forall f tf, transf_function f = OK tf -> fn_params tf = fn_params f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma entrypoint_preserved: + forall f tf, transf_function f = OK tf -> fn_entrypoint tf = fn_entrypoint f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma sig_preserved2: + forall f tf, transf_function f = OK tf -> fn_sig tf = fn_sig f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma transf_function_is_typable: + forall f tf, transf_function f = OK tf -> + exists tenv, type_function f = OK tenv. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + exists x. + assumption. +Qed. +Lemma transf_function_invariants_inductive: + forall f tf tenv, transf_function f = OK tf -> + type_function f = OK tenv -> + check_inductiveness (ctx:=(context_from_hints (snd (preanalysis tenv f)))) + f tenv (fst (preanalysis tenv f)) = true. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + replace x with tenv in * by congruence. + clear x. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness; trivial; discriminate. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + exists tfd, + find_function tge ros rs = Some tfd /\ transf_fundef fd = OK tfd. +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. + +Check sem_rel_b. +Inductive match_stackframes: list stackframe -> list stackframe -> signature -> Prop := + | match_stackframes_nil: forall sg, + sg.(sig_res) = Tint -> + match_stackframes nil nil sg + | match_stackframes_cons: + forall res f sp pc rs s tf ts sg tenv + (STACKS: match_stackframes s ts (fn_sig tf)) + (FUN: transf_function f = OK tf) + (WTF: type_function f = OK tenv) + (WTRS: wt_regset tenv rs) + (WTRES: tenv res = proj_sig_res sg) + (REL: forall m vres, + sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) + ((fst (preanalysis tenv f))#pc) (rs#res <- vres) m), + + match_stackframes + (Stackframe res f sp pc rs :: s) + (Stackframe res tf sp pc rs :: ts) + sg. + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s f sp pc rs m ts tf tenv + (STACKS: match_stackframes s ts (fn_sig tf)) + (FUN: transf_function f = OK tf) + (WTF: type_function f = OK tenv) + (WTRS: wt_regset tenv rs) + (REL: sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) ((fst (preanalysis tenv f))#pc) rs m), + match_states (State s f sp pc rs m) + (State ts tf sp pc rs m) + | match_states_call: + forall s f args m ts tf + (STACKS: match_stackframes s ts (funsig tf)) + (FUN: transf_fundef f = OK tf) + (WTARGS: Val.has_type_list args (sig_args (funsig tf))), + match_states (Callstate s f args m) + (Callstate ts tf args m) + | match_states_return: + forall s res m ts sg + (STACKS: match_stackframes s ts sg) + (WTRES: Val.has_type res (proj_sig_res sg)), + match_states (Returnstate s res m) + (Returnstate ts res m). + +Lemma match_stackframes_change_sig: + forall s ts sg sg', + match_stackframes s ts sg -> + sg'.(sig_res) = sg.(sig_res) -> + match_stackframes s ts sg'. +Proof. + intros. inv H. + constructor. congruence. + econstructor; eauto. + unfold proj_sig_res in *. rewrite H0; auto. +Qed. + +Lemma transf_function_at: + forall f tf pc tenv instr + (TF : transf_function f = OK tf) + (TYPE : type_function f = OK tenv) + (PC : (fn_code f) ! pc = Some instr), + (fn_code tf) ! pc = Some (transf_instr + (ctx := (context_from_hints (snd (preanalysis tenv f)))) + (fst (preanalysis tenv f)) + pc instr). +Proof. + intros. + unfold transf_function in TF. + monadInv TF. + replace x with tenv in * by congruence. + clear EQ. + destruct (preanalysis tenv f) as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + simpl. + rewrite PTree.gmap. + rewrite PC. + reflexivity. +Qed. + +Ltac TR_AT := erewrite transf_function_at by eauto. + +Hint Resolve wt_instrs type_function_correct : wt. + +Lemma wt_undef : + forall tenv rs dst, + wt_regset tenv rs -> + wt_regset tenv rs # dst <- Vundef. +Proof. + unfold wt_regset. + intros. + destruct (peq r dst). + { subst dst. + rewrite Regmap.gss. + constructor. + } + rewrite Regmap.gso by congruence. + auto. +Qed. + +Lemma rel_ge: + forall inv inv' + (GE : RELATION.ge inv' inv) + ctx sp rs m + (REL: sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) inv rs m), + sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) inv' rs m. +Proof. + unfold sem_rel, RELATION.ge. + intros. + apply (REL i); trivial. + eapply HashedSet.PSet.is_subset_spec1; eassumption. +Qed. + +Hint Resolve rel_ge : cse3. + +Lemma sem_rhs_sop : + forall sp op rs args m v, + eval_operation ge sp op rs ## args m = Some v -> + sem_rhs (genv:=ge) (sp:=sp) (SOp op) args rs m v. +Proof. + intros. simpl. + rewrite H. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sop : cse3. + +Lemma sem_rhs_sload : + forall sp chunk addr rs args m a v, + eval_addressing ge sp addr rs ## args = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m v. +Proof. + intros. simpl. + rewrite H. rewrite H0. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload : cse3. + +Lemma sem_rhs_sload_notrap1 : + forall sp chunk addr rs args m, + eval_addressing ge sp addr rs ## args = None -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m Vundef. +Proof. + intros. simpl. + rewrite H. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload_notrap1 : cse3. + +Lemma sem_rhs_sload_notrap2 : + forall sp chunk addr rs args m a, + eval_addressing ge sp addr rs ## args = Some a -> + Mem.loadv chunk m a = None -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m Vundef. +Proof. + intros. simpl. + rewrite H. rewrite H0. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload_notrap2 : cse3. + +Lemma sem_rel_top: + forall ctx sp rs m, sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) RELATION.top rs m. +Proof. + unfold sem_rel, RELATION.top. + intros. + rewrite HashedSet.PSet.gempty in *. + discriminate. +Qed. + +Hint Resolve sem_rel_top : cse3. + +Lemma sem_rel_b_top: + forall ctx sp rs m, sem_rel_b sp ctx (Some RELATION.top) rs m. +Proof. + intros. simpl. + apply sem_rel_top. +Qed. + +Hint Resolve sem_rel_b_top : cse3. + +Ltac IND_STEP := + match goal with + REW: (fn_code ?fn) ! ?mpc = Some ?minstr + |- + sem_rel_b ?sp (context_from_hints (snd (preanalysis ?tenv ?fn))) ((fst (preanalysis ?tenv ?fn)) # ?mpc') ?rs ?m => + assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv fn)))) fn tenv (fst (preanalysis tenv fn))) as IND by + (apply checked_is_inductive_allstep; + eapply transf_function_invariants_inductive; eassumption); + unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND; + specialize IND with (pc:=mpc) (pc':=mpc') (instr:=minstr); + simpl in IND; + rewrite REW in IND; + simpl in IND; + destruct ((fst (preanalysis tenv fn)) # mpc') as [zinv' | ]; + destruct ((fst (preanalysis tenv fn)) # mpc) as [zinv | ]; + simpl in *; + intuition; + eapply rel_ge; eauto with cse3; + idtac mpc mpc' fn minstr + end. + +Lemma if_same : forall {T : Type} (b : bool) (x : T), + (if b then x else x) = x. +Proof. + destruct b; trivial. +Qed. + +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. + induction 1; intros S1' MS; inv MS. + - (* Inop *) + exists (State ts tf sp pc' rs m). split. + + apply exec_Inop; auto. + TR_AT. reflexivity. + + econstructor; eauto. + IND_STEP. + - (* Iop *) + exists (State ts tf sp pc' (rs # res <- v) m). split. + + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'. + assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity. + unfold transf_instr, find_op_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct (if is_trivial_op op + then None + else + rhs_find pc (SOp op) + (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND. + ** destruct (is_trivial_op op). discriminate. + apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iop with (op := op) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)). + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_operation_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iop with (op := op) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)). + TR_AT. + { subst instr'. + rewrite if_same in H1. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_operation_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * eapply wt_exec_Iop with (f:=f); try eassumption. + eauto with wt. + * IND_STEP. + apply oper_sound; eauto with cse3. + + - (* Iload *) + exists (State ts tf sp pc' (rs # dst <- v) m). split. + + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. + assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. + unfold transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite H1 in FIND_SOUND. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := trap) (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * eapply wt_exec_Iload with (f:=f); try eassumption. + eauto with wt. + * IND_STEP. + apply oper_sound; eauto with cse3. + + - (* Iload notrap1 *) + exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * apply wt_undef; assumption. + * IND_STEP. + apply oper_sound; eauto with cse3. + + - (* Iload notrap2 *) + exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite H1 in FIND_SOUND. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload_notrap2 with (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * apply wt_undef; assumption. + * IND_STEP. + apply oper_sound; eauto with cse3. + + - (* Istore *) + exists (State ts tf sp pc' rs m'). split. + + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. + * TR_AT. reflexivity. + * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + rewrite eval_addressing_preserved with (ge1 := ge) by exact symbols_preserved. + assumption. + + econstructor; eauto. + IND_STEP. + apply store_sound with (a0:=a) (m0:=m); eauto with cse3. + + - (* Icall *) + destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. + econstructor. split. + + eapply exec_Icall; try eassumption. + * TR_AT. reflexivity. + * apply sig_preserved; auto. + + rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + assert (wt_instr f tenv (Icall (funsig fd) ros args res pc')) as WTcall by eauto with wt. + inv WTcall. + constructor; trivial. + * econstructor; eauto. + ** rewrite sig_preserved with (f:=fd); assumption. + ** intros. + IND_STEP. + apply kill_reg_sound; eauto with cse3. + eapply kill_mem_sound; eauto with cse3. + * rewrite sig_preserved with (f:=fd) by trivial. + rewrite <- H7. + apply wt_regset_list; auto. + - (* Itailcall *) + destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. + econstructor. split. + + eapply exec_Itailcall; try eassumption. + * TR_AT. reflexivity. + * apply sig_preserved; auto. + * rewrite stacksize_preserved with (f:=f); eauto. + + rewrite subst_args_ok with (m:=m) (sp := (Vptr stk Ptrofs.zero)) by trivial. + assert (wt_instr f tenv (Itailcall (funsig fd) ros args)) as WTcall by eauto with wt. + inv WTcall. + constructor; trivial. + * rewrite sig_preserved with (f:=fd) by trivial. + inv STACKS. + ** econstructor; eauto. + rewrite H7. + rewrite <- sig_preserved2 with (tf:=tf) by trivial. + assumption. + ** econstructor; eauto. + unfold proj_sig_res in *. + rewrite H7. + rewrite WTRES. + rewrite sig_preserved2 with (f:=f) by trivial. + reflexivity. + * rewrite sig_preserved with (f:=fd) by trivial. + rewrite <- H6. + apply wt_regset_list; auto. + - (* Ibuiltin *) + econstructor. split. + + eapply exec_Ibuiltin; try eassumption. + * TR_AT. reflexivity. + * eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + * eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + econstructor; eauto. + * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. + * IND_STEP. + - (* Icond *) + econstructor. split. + + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. + * TR_AT. reflexivity. + * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + eassumption. + * reflexivity. + + econstructor; eauto. + destruct b; IND_STEP. + + - (* Ijumptable *) + econstructor. split. + + eapply exec_Ijumptable with (arg := (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc arg)); try eassumption. + * TR_AT. reflexivity. + * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. + assumption. + + econstructor; eauto. + assert (In pc' tbl) as IN_LIST by (eapply list_nth_z_in; eassumption). + IND_STEP. + + - (* Ireturn *) + destruct or as [arg | ]. + -- econstructor. split. + + eapply exec_Ireturn with (or := Some (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc arg)). + * TR_AT. reflexivity. + * rewrite stacksize_preserved with (f:=f); eauto. + + simpl. + rewrite subst_arg_ok with (sp:=(Vptr stk Ptrofs.zero)) (m:=m) by trivial. + econstructor; eauto. + apply type_function_correct in WTF. + apply wt_instrs with (pc:=pc) (instr:=(Ireturn (Some arg))) in WTF. + 2: assumption. + inv WTF. + rewrite sig_preserved2 with (f:=f) by assumption. + rewrite <- H3. + unfold wt_regset in WTRS. + apply WTRS. + -- econstructor. split. + + eapply exec_Ireturn; try eassumption. + * TR_AT; reflexivity. + * rewrite stacksize_preserved with (f:=f); eauto. + + econstructor; eauto. + simpl. trivial. + - (* Callstate internal *) + monadInv FUN. + rename x into tf. + destruct (transf_function_is_typable f tf EQ) as [tenv TENV]. + econstructor; split. + + apply exec_function_internal. + rewrite stacksize_preserved with (f:=f); eauto. + + rewrite params_preserved with (tf:=tf) (f:=f) by assumption. + rewrite entrypoint_preserved with (tf:=tf) (f:=f) by assumption. + econstructor; eauto. + * apply type_function_correct in TENV. + inv TENV. + simpl in WTARGS. + rewrite sig_preserved2 with (f:=f) in WTARGS by assumption. + apply wt_init_regs. + rewrite <- wt_params in WTARGS. + assumption. + * rewrite @checked_is_inductive_entry with (tenv:=tenv) (ctx:=(context_from_hints (snd (preanalysis tenv f)))). + ** apply sem_rel_b_top. + ** apply transf_function_invariants_inductive with (tf:=tf); auto. + + - (* external *) + simpl in FUN. + inv FUN. + econstructor. split. + + eapply exec_function_external. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + econstructor; eauto. + eapply external_call_well_typed; eauto. + - (* return *) + inv STACKS. + econstructor. split. + + eapply exec_return. + + econstructor; eauto. + apply wt_regset_assign; trivial. + rewrite WTRES0. + exact WTRES. +Qed. + +Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. +Proof. + intros. inversion H. + exploit function_ptr_translated; eauto. + intros (tf & A & B). + exists (Callstate nil tf nil m0); split. + - econstructor; eauto. + + eapply (Genv.init_mem_match TRANSF); eauto. + + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main; eauto. + + rewrite <- H3. eapply sig_preserved; eauto. + - constructor; trivial. + + constructor. rewrite sig_preserved with (f:=f) by assumption. + rewrite H3. reflexivity. + + rewrite sig_preserved with (f:=f) by assumption. + rewrite H3. reflexivity. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> final_state S1 r -> 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. + - intros. eapply step_simulation; eauto. +Qed. + +End PRESERVATION. diff --git a/backend/FirstNop.v b/backend/FirstNop.v new file mode 100644 index 00000000..f7e5261e --- /dev/null +++ b/backend/FirstNop.v @@ -0,0 +1,18 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. + +Definition transf_function (f: function) : function := + let start_pc := Pos.succ (max_pc_function f) in + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.set start_pc (Inop f.(fn_entrypoint)) f.(fn_code); + fn_entrypoint := start_pc |}. + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. + diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v new file mode 100644 index 00000000..5d9a7d6a --- /dev/null +++ b/backend/FirstNopproof.v @@ -0,0 +1,274 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import FirstNop. +Require Import Lia. + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +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; reflexivity. +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. + +Lemma transf_function_at: + forall f pc i, + f.(fn_code)!pc = Some i -> + (transf_function f).(fn_code)!pc = Some i. +Proof. + intros until i. intro Hcode. + unfold transf_function; simpl. + destruct (peq pc (Pos.succ (max_pc_function f))) as [EQ | NEQ]. + { assert (pc <= (max_pc_function f))%positive as LE by (eapply max_pc_function_sound; eassumption). + subst pc. + lia. + } + rewrite PTree.gso by congruence. + assumption. +Qed. + +Hint Resolve transf_function_at : firstnop. + +Ltac TR_AT := + match goal with + | [ A: (fn_code _)!_ = Some _ |- _ ] => + generalize (transf_function_at _ _ _ A); intros + end. + + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := +| match_frames_intro: forall res f sp pc rs, + 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'), + 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 match_pc_refl : forall f pc, match_pc f pc pc. +Proof. + unfold match_pc. + left. + trivial. +Qed. + +Hint Resolve match_pc_refl : firstnop. + +Lemma initial_jump: + forall f, + (fn_code (transf_function f)) ! (Pos.succ (max_pc_function f)) = + Some (Inop (fn_entrypoint f)). +Proof. + intros. unfold transf_function. simpl. + apply PTree.gss. +Qed. + +Hint Resolve initial_jump : firstnop. + *) + +Lemma match_pc_same : + forall f pc i, + PTree.get pc (fn_code f) = Some i -> + PTree.get pc (fn_code (transf_function f)) = Some i. +Proof. + intros. + unfold transf_function. simpl. + rewrite <- H. + apply PTree.gso. + pose proof (max_pc_function_sound f pc i H) as LE. + unfold Ple in LE. + lia. +Qed. + +Hint Resolve match_pc_same : firstnop. + + +Definition measure (S: RTL.state) : nat := + match S with + | State _ _ _ _ _ _ => 0%nat + | Callstate _ _ _ _ => 1%nat + | Returnstate _ _ _ => 0%nat + end. + +Lemma step_simulation: + forall S1 t S2, + step ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. +Proof. + induction 1; intros; inv MS. + - left. econstructor. split. + + eapply plus_one. eapply exec_Inop; eauto with firstnop. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iop with (v:=v); eauto with firstnop. + rewrite <- H0. + apply eval_operation_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop. + rewrite <- H0. + apply eval_addressing_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop. + rewrite <- H0. + apply eval_addressing_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop. + rewrite <- H0. + apply eval_addressing_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Istore; eauto with firstnop. + rewrite <- H0. + apply eval_addressing_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Icall. + apply match_pc_same. exact H. + apply find_function_translated. + exact H0. + apply sig_preserved. + + constructor. + constructor; auto. + constructor. + - left. econstructor. split. + + eapply plus_one. eapply exec_Itailcall. + apply match_pc_same. exact H. + apply find_function_translated. + exact H0. + apply sig_preserved. + unfold transf_function; simpl. + eassumption. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ibuiltin; eauto with firstnop. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Icond; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ijumptable; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ireturn; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_two. + * eapply exec_function_internal; eauto with firstnop. + * eapply exec_Inop. + unfold transf_function; simpl. + rewrite PTree.gss. + reflexivity. + * auto. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_function_external; eauto with firstnop. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor; auto. + - left. + inv STACKS. inv H1. + econstructor; split. + + eapply plus_one. eapply exec_return; eauto. + + constructor; auto. +Qed. + +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_star. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION. diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml index 8905e252..c73bf30d 100644 --- a/backend/JsonAST.ml +++ b/backend/JsonAST.ml @@ -31,7 +31,7 @@ let pp_section pp sec = pp_jobject_end pp in match sec with | Section_text -> pp_simple "Text" - | Section_data init -> pp_complex "Data" init + | Section_data(init, thread_local) -> pp_complex "Data" init (* FIXME *) | Section_small_data init -> pp_complex "Small Data" init | Section_const init -> pp_complex "Const" init | Section_small_const init -> pp_complex "Small Const" init diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 1381877b..9d5a5ba6 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -193,8 +193,9 @@ let forward_sequences code entry = if get_some @@ PTree.get ifnot join_points then ([], [ifso; ifnot]) else let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem) | Some true -> - let errstr = Printf.sprintf ("Inconsistency detected in node %d: ifnot is not the preferred branch") (P.to_int node) in - failwith errstr) + if get_some @@ PTree.get ifso join_points then ([], [ifso; ifnot]) + else let ln, rem = traverse_fallthrough code ifso in (ln, [ifnot] @ rem) + ) | Ljumptable(_, ln) -> begin (* debug "STOP Ljumptable\n"; *) ([], ln) end in ([node] @ ln, rem) end diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 155f5e55..0635e32d 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -121,7 +121,7 @@ module Printer(Target:TARGET) = let sec = match C2C.atom_sections name with | [s] -> s - | _ -> Section_data true + | _ -> Section_data (true, false) and align = match C2C.atom_alignof name with | Some a -> a diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index d82e6f84..e14da87e 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -303,6 +303,7 @@ let print_version_and_options oc comment = fprintf oc " %s" Commandline.argv.(i) done; fprintf oc "\n" + (** Get the name of the common section if it is used otherwise the given section name, with bss as default *) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 902a5c5d..75f5eb3e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -46,16 +46,29 @@ let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103 let atom_is_static a = try - (Hashtbl.find decl_atom a).a_storage = C.Storage_static + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_static | C.Storage_thread_local_static -> true + | _ -> false with Not_found -> false let atom_is_extern a = try - (Hashtbl.find decl_atom a).a_storage = C.Storage_extern + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_extern| C.Storage_thread_local_extern -> true + | _ -> false with Not_found -> false +let atom_is_thread_local a = + try + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_thread_local_extern| C.Storage_thread_local_static + | C.Storage_thread_local -> true + | _ -> false + with Not_found -> + false + let atom_alignof a = try (Hashtbl.find decl_atom a).a_alignment @@ -1245,7 +1258,8 @@ let convertFundef loc env fd = let vars = List.map (fun (sto, id, ty, init) -> - if sto = Storage_extern || sto = Storage_static then + if sto = Storage_extern || sto = Storage_thread_local_extern + || sto = Storage_static || sto = Storage_thread_local_static then unsupported "'static' or 'extern' local variable"; if init <> None then unsupported "initialized local variable"; @@ -1348,15 +1362,21 @@ let convertGlobvar loc env (sto, id, ty, optinit) = let init' = match optinit with | None -> - if sto = C.Storage_extern then [] else [AST.Init_space sz] + if sto = C.Storage_extern || sto = C.Storage_thread_local_extern + then [] else [AST.Init_space sz] | Some i -> convertInitializer env ty i in let (section, access) = - Sections.for_variable env loc id' ty (optinit <> None) in + Sections.for_variable env loc id' ty (optinit <> None) + (match sto with + | Storage_thread_local | Storage_thread_local_extern + | Storage_thread_local_static -> true + | _ -> false) in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then error "'%s' is too big (%s bytes)" id.name (Z.to_string sz); - if sto <> C.Storage_extern && Cutil.incomplete_type env ty then + if sto <> C.Storage_extern && sto <> C.Storage_thread_local_extern + && Cutil.incomplete_type env ty then error "'%s' has incomplete type" id.name; Hashtbl.add decl_atom id' { a_storage = sto; @@ -1455,7 +1475,7 @@ let cleanupGlobals p = if IdentSet.mem fd.fd_name !strong then error "multiple definitions of %s" fd.fd_name.name; strong := IdentSet.add fd.fd_name !strong - | C.Gdecl(Storage_extern, id, ty, init) -> + | C.Gdecl((Storage_extern|Storage_thread_local_extern), id, ty, init) -> extern := IdentSet.add id !extern | C.Gdecl(sto, id, ty, Some i) -> if IdentSet.mem id !strong then @@ -1474,7 +1494,7 @@ let cleanupGlobals p = match g.gdesc with | C.Gdecl(sto, id, ty, init) -> let better_def_exists = - if sto = Storage_extern then + if sto = Storage_extern || sto = Storage_thread_local_extern then IdentSet.mem id !strong || IdentSet.mem id !weak else if init = None then IdentSet.mem id !strong diff --git a/common/Sections.ml b/common/Sections.ml index 839128a5..ea0b6dbc 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -17,7 +17,8 @@ type section_name = | Section_text - | Section_data of bool (* true = init data, false = uninit data *) + | Section_data of bool (* true = init data, false = uninit data *) + * bool (* thread local? *) | Section_small_data of bool | Section_const of bool | Section_small_const of bool @@ -47,8 +48,8 @@ type section_info = { } let default_section_info = { - sec_name_init = Section_data true; - sec_name_uninit = Section_data false; + sec_name_init = Section_data (true, false); + sec_name_uninit = Section_data (false, false); sec_writable = true; sec_executable = false; sec_access = Access_default @@ -63,8 +64,13 @@ let builtin_sections = [ sec_writable = false; sec_executable = true; sec_access = Access_default}; "DATA", - {sec_name_init = Section_data true; - sec_name_uninit = Section_data false; + {sec_name_init = Section_data (true, false); + sec_name_uninit = Section_data (false, false); + sec_writable = true; sec_executable = false; + sec_access = Access_default}; + "TDATA", + {sec_name_init = Section_data (true, true); + sec_name_uninit = Section_data (false, true); sec_writable = true; sec_executable = false; sec_access = Access_default}; "SDATA", @@ -175,7 +181,7 @@ let get_attr_section loc attr = (* Determine section for a variable definition *) -let for_variable env loc id ty init = +let for_variable env loc id ty init thrl = let attr = Cutil.attributes_of_type env ty in let readonly = List.mem C.AConst attr && not(List.mem C.AVolatile attr) in let si = @@ -194,7 +200,8 @@ let for_variable env loc id ty init = let name = if readonly then if size <= !Clflags.option_small_const then "SCONST" else "CONST" - else if size <= !Clflags.option_small_data then "SDATA" else "DATA" in + else if size <= !Clflags.option_small_data then "SDATA" else + if thrl then "TDATA" else "DATA" in try Hashtbl.find current_section_table name with Not_found -> diff --git a/common/Sections.mli b/common/Sections.mli index d9fd9239..00c06c20 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -18,7 +18,8 @@ type section_name = | Section_text - | Section_data of bool (* true = init data, false = uninit data *) + | Section_data of bool (* true = init data, false = uninit data *) + * bool (* thread local? *) | Section_small_data of bool | Section_const of bool | Section_small_const of bool @@ -46,7 +47,7 @@ val define_section: -> ?writable:bool -> ?executable:bool -> ?access:access_mode -> unit -> unit val use_section_for: AST.ident -> string -> bool -val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> bool -> +val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> bool -> bool -> section_name * access_mode val for_function: Env.t -> C.location -> AST.ident -> C.attributes -> section_name list val for_stringlit: unit -> section_name diff --git a/cparser/C.mli b/cparser/C.mli index 15717565..3c271f3f 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -86,8 +86,11 @@ type attributes = attribute list type storage = | Storage_default (* used for toplevel names without explicit storage *) + | Storage_thread_local | Storage_extern | Storage_static + | Storage_thread_local_extern + | Storage_thread_local_static | Storage_auto (* used for block-scoped names without explicit storage *) | Storage_register diff --git a/cparser/Cabs.v b/cparser/Cabs.v index 5f12e8a1..2dae061a 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -54,7 +54,7 @@ Inductive typeSpecifier := (* Merge all specifiers into one type *) | Tenum : option string -> option (list (string * option expression * loc)) -> list attribute -> typeSpecifier with storage := - AUTO | STATIC | EXTERN | REGISTER | TYPEDEF + AUTO | STATIC | EXTERN | REGISTER | TYPEDEF | THREAD_LOCAL with cvspec := | CV_CONST | CV_VOLATILE | CV_RESTRICT diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index ecf83779..7bae2fe2 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -354,7 +354,9 @@ and is_constant_lval env e = begin match Env.find_ident env id with | Env.II_ident(sto, _) -> begin match sto with - | Storage_default | Storage_extern | Storage_static -> true + | Storage_default | Storage_extern | Storage_static + | Storage_thread_local | Storage_thread_local_extern | Storage_thread_local_static + -> true | Storage_auto | Storage_register -> false end | Env.II_enum _ -> false (* should not happen *) diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index 63ac8ac1..9f19395a 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -126,14 +126,14 @@ let add_enum e = *) let visible_decl (sto, id, ty, init) = - sto = Storage_default && + (sto = Storage_default || sto = Storage_thread_local) && match ty with TFun _ -> false | _ -> true let visible_fundef f = match f.fd_storage with - | Storage_default -> not f.fd_inline - | Storage_extern -> true - | Storage_static -> false + | Storage_default | Storage_thread_local -> not f.fd_inline + | Storage_extern | Storage_thread_local_extern -> true + | Storage_static | Storage_thread_local_static -> false | Storage_auto | Storage_register -> assert false let rec add_init_globdecls accu = function diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 9aeec421..78970990 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -361,6 +361,9 @@ let storage pp = function | Storage_default -> () | Storage_extern -> fprintf pp "extern " | Storage_static -> fprintf pp "static " + | Storage_thread_local -> fprintf pp "_Thread_local" + | Storage_thread_local_extern -> fprintf pp "extern _Thread_local" + | Storage_thread_local_static -> fprintf pp "static _Thread_local" | Storage_auto -> () (* used only in blocks, where it can be omitted *) | Storage_register -> fprintf pp "register " diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 9e17cb7e..0504ad0b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -152,6 +152,9 @@ let name_of_storage_class = function | Storage_default -> "<default>" | Storage_extern -> "'extern'" | Storage_static -> "'static'" + | Storage_thread_local -> "'_Thread_local'" + | Storage_thread_local_extern -> "'_Thread_local extern'" + | Storage_thread_local_static -> "'_Thread_local static'" | Storage_auto -> "'auto'" | Storage_register -> "'register'" @@ -177,15 +180,29 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = | Storage_static,Storage_static | Storage_extern,Storage_extern | Storage_default,Storage_default -> sto - | _,Storage_static -> + | Storage_thread_local_static,Storage_thread_local_static + | Storage_thread_local_extern,Storage_thread_local_extern + | Storage_thread_local,Storage_thread_local -> sto + | _,Storage_static | _,Storage_thread_local_static -> error loc "static declaration of '%s' follows non-static declaration" s; sto | Storage_static,_ -> Storage_static (* Static stays static *) - | Storage_extern,_ -> if is_function_type env new_ty then Storage_extern else sto + | Storage_thread_local_static,_ -> Storage_thread_local_static (* Thread-local static stays static *) + | (Storage_extern|Storage_thread_local_extern),_ -> if is_function_type env new_ty then Storage_extern else sto | Storage_default,Storage_extern -> if is_global_defined s && is_function_type env ty then warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored"; Storage_extern + | Storage_thread_local,Storage_thread_local_extern -> + if is_global_defined s && is_function_type env ty then + warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored"; + Storage_extern + | Storage_thread_local, Storage_default -> + error loc "Non thread-local declaration follows thread-local"; + sto + | Storage_default, (Storage_thread_local|Storage_thread_local_extern) -> + error loc "Thread-local declaration follows non thread-local"; + sto | _,Storage_extern -> old_sto (* "auto" and "register" don't appear in toplevel definitions. Normally this was checked earlier. Generate error message @@ -639,13 +656,26 @@ let rec elab_specifier ?(only = false) loc env specifier = restrict := cv = CV_RESTRICT; attr := add_attributes (elab_cvspec env cv) !attr | SpecStorage st -> - if !sto <> Storage_default && st <> TYPEDEF then + if !sto <> Storage_default && st <> TYPEDEF && st <> THREAD_LOCAL then error loc "multiple storage classes in declaration specifier"; begin match st with | AUTO -> sto := Storage_auto | STATIC -> sto := Storage_static | EXTERN -> sto := Storage_extern | REGISTER -> sto := Storage_register + | THREAD_LOCAL -> + sto := (match !sto with + | Storage_static | Storage_thread_local_static -> + Storage_thread_local_static + | Storage_extern | Storage_thread_local_extern -> + Storage_thread_local_extern + | Storage_default | Storage_thread_local -> + Storage_thread_local + | Storage_auto|Storage_register -> + error loc "_Thread_local on auto or register variable"; + !sto + ) + | TYPEDEF -> if !typedef then error loc "multiple uses of 'typedef'"; diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index e44a330f..b36b3e81 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -72,6 +72,7 @@ let () = ("goto", fun loc -> GOTO loc); ("if", fun loc -> IF loc); ("inline", fun loc -> INLINE loc); + ("_Thread_local", fun loc -> THREAD_LOCAL loc); ("_Noreturn", fun loc -> NORETURN loc); ("int", fun loc -> INT loc); ("long", fun loc -> LONG loc); @@ -542,6 +543,7 @@ and singleline_comment = parse | Pre_parser.IF loc -> loop (Parser.IF_ loc) | Pre_parser.INC loc -> loop (Parser.INC loc) | Pre_parser.INLINE loc -> loop (Parser.INLINE loc) + | Pre_parser.THREAD_LOCAL loc -> loop (Parser.THREAD_LOCAL loc) | Pre_parser.INT loc -> loop (Parser.INT loc) | Pre_parser.LBRACE loc -> loop (Parser.LBRACE loc) | Pre_parser.LBRACK loc -> loop (Parser.LBRACK loc) diff --git a/cparser/Parser.vy b/cparser/Parser.vy index 03bfa590..4f3b9789 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -32,7 +32,7 @@ Require Cabs. LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN %token<Cabs.loc> LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA - SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE + SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE THREAD_LOCAL NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID STRUCT UNION ENUM UNDERSCORE_BOOL PACKED ALIGNAS ATTRIBUTE ASM @@ -397,6 +397,8 @@ storage_class_specifier: { (Cabs.AUTO, loc) } | loc = REGISTER { (Cabs.REGISTER, loc) } +| loc = THREAD_LOCAL + { (Cabs.THREAD_LOCAL, loc) } (* 6.7.2 *) type_specifier: diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 64412194..aeeb9326 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -257,13 +257,16 @@ let rec reserve_public env = function match dcl.gdesc with | Gdecl(sto, id, _, _) -> begin match sto with - | Storage_default | Storage_extern -> enter_public env id + | Storage_default | Storage_thread_local + | Storage_extern | Storage_thread_local_extern -> + enter_public env id | Storage_static -> env | _ -> assert false end | Gfundef f -> begin match f.fd_storage with - | Storage_default | Storage_extern -> enter_public env f.fd_name + | Storage_default | Storage_extern + -> enter_public env f.fd_name | Storage_static -> env | _ -> assert false end diff --git a/cparser/deLexer.ml b/cparser/deLexer.ml index de0e9b6e..43c1a679 100644 --- a/cparser/deLexer.ml +++ b/cparser/deLexer.ml @@ -30,6 +30,7 @@ let delex (symbol : string) : string = | "BUILTIN_VA_ARG" -> "__builtin_va_arg" | "CONST" -> "const" | "INLINE" -> "inline" + | "THREAD_LOCAL" -> "_Thread_local" | "PACKED" -> "__packed__" | "RESTRICT" -> "restrict" | "SIGNED" -> "signed" diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly index 669ecf5e..e21a3519 100644 --- a/cparser/pre_parser.mly +++ b/cparser/pre_parser.mly @@ -54,7 +54,7 @@ COLON AND MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT - AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE + AUTO REGISTER INLINE THREAD_LOCAL NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE UNDERSCORE_BOOL CONST VOLATILE VOID STRUCT UNION ENUM CASE DEFAULT IF ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK RETURN BUILTIN_VA_ARG ALIGNOF ATTRIBUTE ALIGNAS PACKED ASM BUILTIN_OFFSETOF @@ -430,6 +430,7 @@ storage_class_specifier_no_typedef: | STATIC | AUTO | REGISTER +| THREAD_LOCAL {} (* [declaration_specifier_no_type] matches declaration specifiers diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6986fb96..ff2647a7 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -25,8 +25,10 @@ let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true -let option_fcse = ref true -let option_fcse2 = ref true +let option_fcse = ref false +let option_fcse2 = ref false +let option_fcse3 = ref true +let option_fcse3_alias_analysis = ref true let option_fredundancy = ref true let option_fduplicate = ref (-1) let option_finvertcond = ref true diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..3dbd35ce 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 + @@@ partial_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. + destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl 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. 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. eapply partial_if_match; eauto. 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 848657e5..a3181da8 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -42,6 +42,12 @@ 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 -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE3_alias_analysis: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 388482a0..b167dbd1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -195,8 +195,10 @@ Processing options: -fconst-prop Perform global constant propagation [on] -ffloat-const-prop <n> Control constant propagation of floats (<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] + -fcse Perform common subexpression elimination [off] + -fcse2 Perform inter-loop common subexpression elimination [off] + -fcse3 Perform inter-loop common subexpression elimination [on] + -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [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] @@ -270,7 +272,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; ] @@ -397,6 +399,8 @@ 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 "cse3-alias-analysis" option_fcse3_alias_analysis @ 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 9b568951..cb461361 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. @@ -113,6 +116,10 @@ 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_CSE3_alias_analysis => + "fun _ -> !Clflags.option_fcse3_alias_analysis". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => @@ -160,6 +167,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. @@ -182,6 +195,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction + CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem 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. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 930b1c51..2489b959 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -157,8 +157,12 @@ module Target (*: TARGET*) = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" + | Section_data(true, true) -> + ".section .tdata,\"awT\",@progbits" + | Section_data(false, true) -> + ".section .tbss,\"awT\",@nobits" + | Section_data(i, false) | Section_small_data(i) -> + (if i then ".data" else "COMM") | Section_const i | Section_small_const i -> if i then ".section .rodata" else "COMM" | Section_string -> ".section .rodata" @@ -211,14 +215,20 @@ module Target (*: TARGET*) = (* Generate code to load the address of id + ofs in register r *) -(* FIXME DMonniaux ugly ugly hack to get at standard __thread data *) let loadsymbol oc r id ofs = if Archi.pic_code () then begin assert (ofs = Integers.Ptrofs.zero); - fprintf oc " make %a = %s\n" ireg r (extern_atom id) - end else begin - if (extern_atom id) = "_impure_thread_data" then begin - fprintf oc " addd %a = $r13, @tprel(%a)\n" ireg r symbol_offset (id, ofs) + if C2C.atom_is_thread_local id then begin + (* fprintf oc " addd %a = $r13, @tprel(%s)\n" ireg r (extern_atom id) *) + fprintf oc " addd %a = $r13, @tlsle(%s)\n" ireg r (extern_atom id) + end else begin + fprintf oc " make %a = %s\n" ireg r (extern_atom id) + end + end else + begin + if C2C.atom_is_thread_local id then begin + (* fprintf oc " addd %a = $r13, @tprel(%a)\n" ireg r symbol_offset (id, ofs) *) + fprintf oc " addd %a = $r13, @tlsle(%a)\n" ireg r symbol_offset (id, ofs) end else begin fprintf oc " make %a = %a\n" ireg r symbol_offset (id, ofs) end diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 0f608d25..3ea03786 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -117,7 +117,9 @@ module Linux_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) -> if i then ".data" else @@ -218,7 +220,9 @@ module Diab_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i -> if i then ".data" else common_section () + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data (i, false) -> if i then ".data" else common_section () | Section_small_data i -> if i then ".sdata" else ".sbss" | Section_const _ -> ".text" | Section_small_const _ -> ".sdata2" diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 64bcea4c..1f02ca71 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -107,7 +107,9 @@ module Target : TARGET = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h index f3fa11fe..7f111742 100644 --- a/runtime/include/ccomp_k1c_fixes.h +++ b/runtime/include/ccomp_k1c_fixes.h @@ -6,7 +6,7 @@ #endif #undef __GNUC__ -#define __thread +#define __thread _Thread_local struct __int128_ccomp { long __int128_ccomp_low; long __int128_ccomp_high; }; diff --git a/test/monniaux/cse2/storeload.c b/test/monniaux/cse2/storeload.c new file mode 100644 index 00000000..028fb835 --- /dev/null +++ b/test/monniaux/cse2/storeload.c @@ -0,0 +1,5 @@ +int toto(int *p, int x) { + p[0] = x; + p[1] = 3; + return *p; +} diff --git a/test/monniaux/thread_local/thread_local.c b/test/monniaux/thread_local/thread_local.c new file mode 100644 index 00000000..7a50db0a --- /dev/null +++ b/test/monniaux/thread_local/thread_local.c @@ -0,0 +1,13 @@ +#include <stdio.h> + +_Thread_local int toto; +_Thread_local int toto2 = 45; + +int foobar(void) { + return toto; +} + +int main() { + printf("%d %d\n", toto, toto2); + return 0; +} diff --git a/test/monniaux/thread_local/thread_local2.c b/test/monniaux/thread_local/thread_local2.c new file mode 100644 index 00000000..ba244ac6 --- /dev/null +++ b/test/monniaux/thread_local/thread_local2.c @@ -0,0 +1,18 @@ +#include <stdio.h> +#include <pthread.h> + +_Thread_local int toto; +_Thread_local int toto2 = 45; + +void* poulet(void * dummy) { + printf("%p %p\n", &toto, &toto2); + return NULL; +} + +int main() { + pthread_t thr; + poulet(NULL); + pthread_create(&thr, NULL, poulet, NULL); + pthread_join(thr, NULL); + return 0; +} diff --git a/test/mppa/hardcheck.sh b/test/mppa/hardcheck.sh index 82b63182..b6538f0e 100755 --- a/test/mppa/hardcheck.sh +++ b/test/mppa/hardcheck.sh @@ -3,4 +3,4 @@ source do_test.sh -do_test hardcheck +do_test hardcheck 1 diff --git a/test/mppa/hardtest.sh b/test/mppa/hardtest.sh index 09511da6..6321bc7d 100755 --- a/test/mppa/hardtest.sh +++ b/test/mppa/hardtest.sh @@ -3,4 +3,4 @@ source do_test.sh -do_test hardtest +do_test hardtest 1 diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 6159437e..e371380c 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -133,7 +133,9 @@ module ELF_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" @@ -191,7 +193,9 @@ module MacOS_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i || (not !Clflags.option_fcommon) then ".data" else "COMM" | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".const" else "COMM" @@ -268,7 +272,9 @@ module Cygwin_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rdata,\"dr\"" else "COMM" |