(* * Copyright (c) 2017-present, * Programming Research Laboratory (ROPAS), Seoul National University, Korea * This software is distributed under the term of the BSD-3 clause license. *) (** * Basic Abstract Domains. *) Set Implicit Arguments. Require Import Morphisms. Require Import VocabA. Require Import hpattern vgtac Fold DFMapAVL DLat DUnit DNList DStr DProd DMap DSum DPow DItv InterCfg UserInputType Global. (** ** Procedure names *) Module Proc <: KEY := DStr.DStr. Module PowProc <: LAT := Pow Proc. (** ** Global/Local variables *) Module GVar <: KEY := DStr.DStr. Module LVar <: KEY := ProdKey2 Proc DStr.DStr. Module Var <: KEY := SumKey2 GVar LVar. (** ** Abstract C struct *) Module Field <: KEY := DStr.DStr. Module Fields <: KEY := NListKey Field. Module ExtAllocsite <: KEY := SumKey2 Unit Proc. Module Allocsite <: KEY := SumKey2 InterNode ExtAllocsite. (** ** Abstract locations *) Module VarAllocsite <: KEY := SumKey2 Var Allocsite. Module FldLoc <: KEY := ProdKey2 VarAllocsite Fields. (* NOTE: The last Proc location in Loc is to remember return locations, which Dump dealt with before. *) Module Loc <: KEY := SumKey2 FldLoc Proc. Module PowLoc <: LAT := Pow Loc. Definition var_of_gvar (x : GVar.t) : Var.t := Var.Inl x. Definition var_of_lvar (x : LVar.t) : Var.t := Var.Inr x. Definition approx_one_loc (g : G.t) (l : Loc.t) : bool := match l with | Loc.Inl (VarAllocsite.Inl (Var.Inl _), Fields.nil) => true | Loc.Inl (VarAllocsite.Inl (Var.Inr (f, _)), Fields.nil) => negb (G.is_rec f g) | _ => false end. Lemma approx_one_loc_mor : forall g, Proper (Loc.eq ==> eq) (approx_one_loc g). Proof. unfold approx_one_loc; inversion 1. - destruct x', y'. destruct Heq as [Hva Hf]; simpl in *. destruct t, t1; [|by inversion Hva|by inversion Hva|by inversion Hva]. destruct a, a0; [ by inversion Hf | inversion Hva; by inversion Heq | inversion Hva; by inversion Heq |]. destruct b, b0; f_equal. destruct t0, t2; [|by inversion Hf|by inversion Hf|by auto]. inversion Hva; inversion Heq; subst; simpl in *. destruct Heq0 as [Hs _]. rewrite G.is_rec_mor; [reflexivity|by apply Hs|reflexivity]. - reflexivity. Qed. Definition is_local_of f l := match l with | Loc.Inl (VarAllocsite.Inl (Var.Inr (g, _)), _) => if DStr.eq_dec f g then true else false | _ => false end. Lemma is_local_of_mor : forall f, Proper (Loc.eq ==> eq) (is_local_of f). Proof. intros f l1 l2 Hl. unfold is_local_of. inversion Hl; [|by auto]. destruct x' as [vax ?], y' as [vay ?]. simpl in Heq. destruct Heq as [Heq1 Heq2]. inversion Heq1; [|by auto]. inversion Heq; [by auto|]. destruct x'0 as [gx ?], y'0 as [gy ?]. simpl in Heq0. destruct Heq0 as [Heq3 Heq4]; subst. reflexivity. Qed. Definition loc_of_var (x : Var.t) : Loc.t := Loc.Inl (VarAllocsite.Inl x, Fields.nil). Lemma loc_of_var_mor : Proper (Var.eq ==> Loc.eq) loc_of_var. Proof. unfold loc_of_var; intros x1 x2 Hx. constructor; s; split; by constructor. Qed. Definition loc_of_allocsite (x : Allocsite.t) : Loc.t := Loc.Inl (VarAllocsite.Inr x, Fields.nil). Lemma loc_of_allocsite_mor : Proper (Allocsite.eq ==> Loc.eq) loc_of_allocsite. Proof. unfold loc_of_allocsite; intros a1 a2 Ha. constructor; s; split; by constructor. Qed. Definition loc_of_proc (x : Proc.t) : Loc.t := Loc.Inr x. Lemma loc_of_proc_mor : Proper (Proc.eq ==> Loc.eq) loc_of_proc. Proof. unfold loc_of_proc; intros p1 p2 Hp. by constructor. Qed. Definition append_field (l : Loc.t) (f : Field.t) : Loc.t := match l with | Loc.Inl va => Loc.Inl (fst va, Fields.app (snd va) f) | _ => l end. Lemma append_field_mor : Proper (Loc.eq ==> Field.eq ==> Loc.eq) append_field. Proof. unfold append_field; intros l1 l2 Hl f1 f2 Hf. inversion Hl; s. - constructor; s; split. + by apply Heq. + apply Fields.app_mor; [by apply Heq|by apply Hf]. - by constructor. Qed. Module SMLocLoc := SetMap Loc PowLoc Loc PowLoc. Definition pow_loc_append_field (ls : PowLoc.t) (f : Field.t) : PowLoc.t := SMLocLoc.map (fun l => append_field l f) ls. Lemma pow_loc_append_field_mor : Proper (PowLoc.eq ==> Field.eq ==> PowLoc.eq) pow_loc_append_field. Proof. unfold pow_loc_append_field; intros ls1 ls2 Hls f1 f2 Hf. unfold SMLocLoc.map; apply PowLoc.fold_mor. - constructor ; [ intros ?; by apply PowLoc.eq_refl | intros ? ?; by apply PowLoc.eq_sym | intros ? ? ?; by apply PowLoc.eq_trans ]. - i; apply PowLoc.add_mor; [|by auto]. apply append_field_mor; by auto. - by auto. - by apply PowLoc.eq_refl. Qed. Definition allocsite_of_node (node : InterNode.t) : Allocsite.t := Allocsite.Inl node. Lemma allocsite_of_node_mor : Proper (InterNode.eq ==> Allocsite.eq) allocsite_of_node. Proof. unfold allocsite_of_node; intros n1 n2 Hn. inversion Hn. by constructor. Qed. Definition allocsite_of_ext (fid_opt : option Proc.t) : Allocsite.t := match fid_opt with | None => Allocsite.Inr (ExtAllocsite.Inl tt) | Some fid => Allocsite.Inr (ExtAllocsite.Inr fid) end. Lemma allocsite_of_ext_mor : Proper (opt_eq Proc.eq ==> Allocsite.eq) allocsite_of_ext. Proof. unfold opt_eq, allocsite_of_ext; intros n1 n2 Hn. destruct n1, n2 ; [constructor; by constructor|tauto|tauto|constructor; by constructor]. Qed.