From 405847450b9464c899a16bc8ef6a752a58ab34e0 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 21 May 2019 16:26:43 +0200 Subject: move Machblock*.v into mppa_k1c/lib Indeed, these files may not be specific to our backend. --- mppa_k1c/Machblock.v | 355 --------------------------------------------------- 1 file changed, 355 deletions(-) delete mode 100644 mppa_k1c/Machblock.v (limited to 'mppa_k1c/Machblock.v') diff --git a/mppa_k1c/Machblock.v b/mppa_k1c/Machblock.v deleted file mode 100644 index 30393fd5..00000000 --- a/mppa_k1c/Machblock.v +++ /dev/null @@ -1,355 +0,0 @@ -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import Conventions. -Require Stacklayout. -Require Import Mach. -Require Import Linking. - -(** instructions "basiques" (ie non control-flow) *) -Inductive basic_inst: Type := - | MBgetstack: ptrofs -> typ -> mreg -> basic_inst - | MBsetstack: mreg -> ptrofs -> typ -> basic_inst - | MBgetparam: ptrofs -> typ -> mreg -> basic_inst - | MBop: operation -> list mreg -> mreg -> basic_inst - | MBload: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst - | MBstore: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst - . - -Definition bblock_body := list basic_inst. - -(** instructions de control flow *) -Inductive control_flow_inst: Type := - | MBcall: signature -> mreg + ident -> control_flow_inst - | MBtailcall: signature -> mreg + ident -> control_flow_inst - | MBbuiltin: external_function -> list (builtin_arg mreg) -> builtin_res mreg -> control_flow_inst - | MBgoto: label -> control_flow_inst - | MBcond: condition -> list mreg -> label -> control_flow_inst - | MBjumptable: mreg -> list label -> control_flow_inst - | MBreturn: control_flow_inst - . - -Record bblock := mk_bblock { - header: list label; - body: bblock_body; - exit: option control_flow_inst -}. - -Lemma bblock_eq: - forall b1 b2, - header b1 = header b2 -> - body b1 = body b2 -> - exit b1 = exit b2 -> - b1 = b2. -Proof. - intros. destruct b1. destruct b2. - simpl in *. subst. auto. -Qed. - -Definition length_opt {A} (o: option A) : nat := - match o with - | Some o => 1 - | None => 0 - end. - -Definition size (b:bblock): nat := (length (header b))+(length (body b))+(length_opt (exit b)). - -Lemma size_null b: - size b = 0%nat -> - header b = nil /\ body b = nil /\ exit b = None. -Proof. - destruct b as [h b e]. simpl. unfold size. simpl. - intros H. - assert (length h = 0%nat) as Hh; [ omega |]. - assert (length b = 0%nat) as Hb; [ omega |]. - assert (length_opt e = 0%nat) as He; [ omega|]. - repeat split. - destruct h; try (simpl in Hh; discriminate); auto. - destruct b; try (simpl in Hb; discriminate); auto. - destruct e; try (simpl in He; discriminate); auto. -Qed. - -Definition code := list bblock. - -Record function: Type := mkfunction - { fn_sig: signature; - fn_code: code; - fn_stacksize: Z; - fn_link_ofs: ptrofs; - fn_retaddr_ofs: ptrofs }. - -Definition fundef := AST.fundef function. - -Definition program := AST.program fundef unit. - -Definition genv := Genv.t fundef unit. - -(*** sémantique ***) - -Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. -Proof. - apply List.in_dec. - apply Pos.eq_dec. -Qed. - -Definition is_label (lbl: label) (bb: bblock) : bool := - if in_dec lbl (header bb) then true else false. - -Lemma is_label_correct_true lbl bb: - List.In lbl (header bb) <-> is_label lbl bb = true. -Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. -Qed. - -Lemma is_label_correct_false lbl bb: - ~(List.In lbl (header bb)) <-> is_label lbl bb = false. -Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. -Qed. - - -Local Open Scope nat_scope. - -Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := - match c with - | nil => None - | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl - end. - -Section RELSEM. - -Variable rao:function -> code -> ptrofs -> Prop. -Variable ge:genv. - -Definition find_function_ptr - (ge: genv) (ros: mreg + ident) (rs: regset) : option block := - match ros with - | inl r => - match rs r with - | Vptr b ofs => if Ptrofs.eq ofs Ptrofs.zero then Some b else None - | _ => None - end - | inr symb => - Genv.find_symbol ge symb - end. - -(** Machblock execution states. *) - -Inductive stackframe: Type := - | Stackframe: - forall (f: block) (**r pointer to calling function *) - (sp: val) (**r stack pointer in calling function *) - (retaddr: val) (**r Asm return address in calling function *) - (c: code), (**r program point in calling function *) - stackframe. - -Inductive state: Type := - | State: - forall (stack: list stackframe) (**r call stack *) - (f: block) (**r pointer to current function *) - (sp: val) (**r stack pointer *) - (c: code) (**r current program point *) - (rs: regset) (**r register state *) - (m: mem), (**r memory state *) - state - | Callstate: - forall (stack: list stackframe) (**r call stack *) - (f: block) (**r pointer to function to call *) - (rs: regset) (**r register state *) - (m: mem), (**r memory state *) - state - | Returnstate: - forall (stack: list stackframe) (**r call stack *) - (rs: regset) (**r register state *) - (m: mem), (**r memory state *) - state. - -Definition parent_sp (s: list stackframe) : val := - match s with - | nil => Vnullptr - | Stackframe f sp ra c :: s' => sp - end. - -Definition parent_ra (s: list stackframe) : val := - match s with - | nil => Vnullptr - | Stackframe f sp ra c :: s' => ra - end. - -Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop := - | exec_MBgetstack: - forall ofs ty dst v, - load_stack m sp ty ofs = Some v -> - basic_step s fb sp rs m (MBgetstack ofs ty dst) (rs#dst <- v) m - | exec_MBsetstack: - forall src ofs ty m' rs', - store_stack m sp ty ofs (rs src) = Some m' -> - rs' = undef_regs (destroyed_by_setstack ty) rs -> - basic_step s fb sp rs m (MBsetstack src ofs ty) rs' m' - | exec_MBgetparam: - forall ofs ty dst v rs' f, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m sp Tptr f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (parent_sp s) ty ofs = Some v -> - rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) -> - basic_step s fb sp rs m (MBgetparam ofs ty dst) rs' m - | exec_MBop: - forall op args v rs' res, - eval_operation ge sp op rs##args m = Some v -> - rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) -> - basic_step s fb sp rs m (MBop op args res) rs' m - | exec_MBload: - forall addr args a v rs' chunk dst, - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) -> - basic_step s fb sp rs m (MBload chunk addr args dst) rs' m - | exec_MBstore: - forall chunk addr args src m' a rs', - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a (rs src) = Some m' -> - rs' = undef_regs (destroyed_by_store chunk addr) rs -> - basic_step s fb sp rs m (MBstore chunk addr args src) rs' m' - . - - -Inductive body_step (s: list stackframe) (f: block) (sp: val): bblock_body -> regset -> mem -> regset -> mem -> Prop := - | exec_nil_body: - forall rs m, - body_step s f sp nil rs m rs m - | exec_cons_body: - forall rs m bi p rs' m' rs'' m'', - basic_step s f sp rs m bi rs' m' -> - body_step s f sp p rs' m' rs'' m'' -> - body_step s f sp (bi::p) rs m rs'' m'' - . - -Inductive cfi_step: control_flow_inst -> state -> trace -> state -> Prop := - | exec_MBcall: - forall s fb sp sig ros c b rs m f f' ra, - find_function_ptr ge ros rs = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - rao f c ra -> - cfi_step (MBcall sig ros) (State s fb sp (b::c) rs m) - E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) - f' rs m) - | exec_MBtailcall: - forall s fb stk soff sig ros c rs m f f' m', - find_function_ptr ge ros rs = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - cfi_step (MBtailcall sig ros) (State s fb (Vptr stk soff) c rs m) - E0 (Callstate s f' rs m') - | exec_MBbuiltin: - forall s f sp rs m ef args res b c vargs t vres rs' m', - eval_builtin_args ge rs sp m args vargs -> - external_call ef ge vargs m t vres m' -> - rs' = set_res res vres (undef_regs (destroyed_by_builtin ef) rs) -> - cfi_step (MBbuiltin ef args res) (State s f sp (b :: c) rs m) - t (State s f sp c rs' m') - | exec_MBgoto: - forall s fb f sp lbl c rs m c', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - cfi_step (MBgoto lbl) (State s fb sp c rs m) - E0 (State s fb sp c' rs m) - | exec_MBcond_true: - forall s fb f sp cond args lbl c rs m c' rs', - eval_condition cond rs##args m = Some true -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - rs' = undef_regs (destroyed_by_cond cond) rs -> - cfi_step (MBcond cond args lbl) (State s fb sp c rs m) - E0 (State s fb sp c' rs' m) - | exec_MBcond_false: - forall s f sp cond args lbl b c rs m rs', - eval_condition cond rs##args m = Some false -> - rs' = undef_regs (destroyed_by_cond cond) rs -> - cfi_step (MBcond cond args lbl) (State s f sp (b :: c) rs m) - E0 (State s f sp c rs' m) - | exec_MBjumptable: - forall s fb f sp arg tbl c rs m n lbl c' rs', - rs arg = Vint n -> - list_nth_z tbl (Int.unsigned n) = Some lbl -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - rs' = undef_regs destroyed_by_jumptable rs -> - cfi_step (MBjumptable arg tbl) (State s fb sp c rs m) - E0 (State s fb sp c' rs' m) - | exec_MBreturn: - forall s fb stk soff c rs m f m', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - cfi_step MBreturn (State s fb (Vptr stk soff) c rs m) - E0 (Returnstate s rs m') - . - -Inductive exit_step: option control_flow_inst -> state -> trace -> state -> Prop := - | exec_Some_exit: - forall ctl s t s', - cfi_step ctl s t s' -> - exit_step (Some ctl) s t s' - | exec_None_exit: - forall stk f sp b lb rs m, - exit_step None (State stk f sp (b::lb) rs m) E0 (State stk f sp lb rs m) - . - -Inductive step: state -> trace -> state -> Prop := - | exec_bblock: - forall sf f sp bb c rs m rs' m' t s', - body_step sf f sp (body bb) rs m rs' m' -> - exit_step (exit bb) (State sf f sp (bb::c) rs' m') t s' -> - step (State sf f sp (bb::c) rs m) t s' - | exec_function_internal: - forall s fb rs m f m1 m2 m3 stk rs', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> - let sp := Vptr stk Ptrofs.zero in - store_stack m1 sp Tptr f.(fn_link_ofs) (parent_sp s) = Some m2 -> - store_stack m2 sp Tptr f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> - rs' = undef_regs destroyed_at_function_entry rs -> - step (Callstate s fb rs m) - E0 (State s fb sp f.(fn_code) rs' m3) - | exec_function_external: - forall s fb rs m t rs' ef args res m', - Genv.find_funct_ptr ge fb = Some (External ef) -> - extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> - external_call ef ge args m t res m' -> - rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) -> - step (Callstate s fb rs m) - t (Returnstate s rs' m') - | exec_return: - forall s f sp ra c rs m, - step (Returnstate (Stackframe f sp ra c :: s) rs m) - E0 (State s f sp c rs m) - . - -End RELSEM. - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall fb m0, - let ge := Genv.globalenv p in - Genv.init_mem p = Some m0 -> - Genv.find_symbol ge p.(prog_main) = Some fb -> - initial_state p (Callstate nil fb (Regmap.init Vundef) m0). - -Inductive final_state: state -> int -> Prop := - | final_state_intro: forall rs m r retcode, - loc_result signature_main = One r -> - rs r = Vint retcode -> - final_state (Returnstate nil rs m) retcode. - -Definition semantics (rao: function -> code -> ptrofs -> Prop) (p: program) := - Semantics (step rao) (initial_state p) final_state (Genv.globalenv p). -- cgit