diff options
Diffstat (limited to 'kvx/lib/PseudoAsmblock.v')
| -rw-r--r-- | kvx/lib/PseudoAsmblock.v | 267 |
1 files changed, 267 insertions, 0 deletions
diff --git a/kvx/lib/PseudoAsmblock.v b/kvx/lib/PseudoAsmblock.v new file mode 100644 index 00000000..b33ea1bd --- /dev/null +++ b/kvx/lib/PseudoAsmblock.v @@ -0,0 +1,267 @@ +Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep. +Require Import Op Machregs Locations Stacklayout Conventions. +Require Import Mach Machblock OptionMonad. + + +(** Registers and States *) + +Inductive preg: Type := + | PC: preg (* program counter *) + | RA: preg (* return-address *) + | SP: preg (* stack-pointer *) + | preg_of: mreg -> preg. +Coercion preg_of: mreg >-> preg. + +Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. +Proof. + decide equality. + apply mreg_eq. +Defined. + +Module PregEq. + Definition t := preg. + Definition eq := preg_eq. +End PregEq. + +Module Pregmap := EMap(PregEq). + +Definition regset := Pregmap.t val. + +Module AsmNotations. + +(* Declare Scope asm. *) +Notation "a # b" := (a b) (at level 1, only parsing) : asm. +Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. +Open Scope asm. + +End AsmNotations. + +Import AsmNotations. + +Definition to_Machrs (rs: regset): Mach.regset := + fun (r:mreg) => rs r. +Coercion to_Machrs: regset >-> Mach.regset. + +Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset := + fun (r:preg) => + match r with + | preg_of mr => mrs mr + | _ => rs r + end. + +Local Open Scope option_monad_scope. + +Record state: Type := State { _rs: regset; _m: mem }. +Definition outcome := option state. +Definition Next rs m: outcome := Some (State rs m). +Definition Stuck: outcome := None. + +(* Asm semantic on Mach *) + +Section RELSEM. + +(** "oracle" stating the successive position (ie offset) of each block in the final assembly function *) +Variable next: function -> Z -> Z. + +Inductive is_pos (f: function): Z -> code -> Prop := + | First_pos: is_pos f 0 (fn_code f) + | Next_pos pos b c: is_pos f pos (b::c) -> is_pos f (next f pos) c. + +Fixpoint label_pos (f: function) (lbl: label) (pos: Z) (c: code) {struct c} : option Z := + match c with + | nil => None + | b :: c' => + if is_label lbl b then Some pos else label_pos f lbl (next f pos) c' + end. + +Definition goto_label (f: function) (lbl: label) (rs: regset) : option val := + SOME pos <- label_pos f lbl 0 (fn_code f) IN + match rs#PC with + | Vptr b _ => Some (Vptr b (Ptrofs.repr pos)) + | _ => None + end. + +Definition next_addr (f: function) (rs: regset): option val := + match rs#PC with + | Vptr b ofs => Some (Vptr b (Ptrofs.repr (next f (Ptrofs.unsigned ofs)))) + | _ => None + end. + +Variable ge:genv. + +Inductive basic_step (f: function) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop := + | exec_MBgetstack: + forall ofs ty dst v, + load_stack m (rs#SP) ty ofs = Some v -> + basic_step f rs m (MBgetstack ofs ty dst) (rs#dst <- v) m + | exec_MBsetstack: + forall (src: mreg) ofs ty m' rs', + store_stack m (rs#SP) ty ofs (rs src) = Some m' -> + rs' = set_from_Machrs (undef_regs (destroyed_by_setstack ty) rs) rs -> + basic_step f rs m (MBsetstack src ofs ty) rs' m' + | exec_MBgetparam: + forall ofs ty (dst: mreg) v rs' psp, + load_stack m (rs#SP) Tptr f.(fn_link_ofs) = Some psp -> + load_stack m psp ty ofs = Some v -> + rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) -> + basic_step f rs m (MBgetparam ofs ty dst) rs' m + | exec_MBop: + forall op args v rs' (res: mreg), + eval_operation ge (rs#SP) op (to_Machrs rs)##args m = Some v -> + rs' = (set_from_Machrs (undef_regs (destroyed_by_op op) rs) rs)#res <- v -> + basic_step f rs m (MBop op args res) rs' m + | exec_MBload: + forall addr args a v rs' trap chunk (dst: mreg), + eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a -> + Mem.loadv chunk m a = Some v -> + rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- v -> + basic_step f rs m (MBload trap chunk addr args dst) rs' m + | exec_MBload_notrap1: + forall addr args rs' chunk (dst: mreg), + eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = None -> + rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) -> + basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m + | exec_MBload_notrap2: + forall addr args a rs' chunk (dst: mreg), + eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a -> + Mem.loadv chunk m a = None -> + rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) -> + basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m + | exec_MBstore: + forall chunk addr args (src: mreg) m' a rs', + eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a -> + Mem.storev chunk m a (rs src) = Some m' -> + rs' = set_from_Machrs (undef_regs (destroyed_by_store chunk addr) rs) rs -> + basic_step f rs m (MBstore chunk addr args src) rs' m' + . + + +Inductive body_step (f: function) : bblock_body -> regset -> mem -> regset -> mem -> Prop := + | exec_nil_body rs m: + body_step f nil rs m rs m + | exec_cons_body rs m bi p rs' m' rs'' m'': + basic_step f rs m bi rs' m' -> + body_step f p rs' m' rs'' m'' -> + body_step f (bi::p) rs m rs'' m'' + . + + +Definition find_function_ptr (ros: mreg + ident) (rs: regset) : option val := + match ros with + | inl r => Some (rs#r) + | inr symb => + SOME b <- Genv.find_symbol ge symb IN + Some (Vptr b Ptrofs.zero) + end. + +Definition exec_epilogue (f: function) (rs: regset) (m: mem) : outcome := + SOME sp <- load_stack m rs#SP Tptr f.(fn_link_ofs) IN + SOME ra <- load_stack m rs#SP Tptr f.(fn_retaddr_ofs) IN + match rs#SP with + | Vptr stk ofs => + SOME m' <- Mem.free m stk 0 f.(fn_stacksize) IN + Next (rs#SP <- sp #RA <- ra) m' + | _ => Stuck + end. + +Inductive cfi_step (f: function): control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop := + | exec_MBcall sig ros rs m pc: + find_function_ptr ros rs = Some pc -> + cfi_step f (MBcall sig ros) rs m E0 ((rs#RA <- (rs#PC))#PC <- pc) m + | exec_MBtailcall sig ros rs m rs' m' pc: + find_function_ptr ros rs = Some pc -> + exec_epilogue f rs m = Next rs' m' -> + cfi_step f (MBtailcall sig ros) rs m E0 (rs'#PC <- pc) m' + | exec_MBreturn rs m rs' m': + exec_epilogue f rs m = Next rs' m' -> + cfi_step f MBreturn rs m E0 (rs'#PC <- (rs'#RA)) m' + | exec_MBgoto lbl rs m pc: + goto_label f lbl rs = Some pc -> + cfi_step f (MBgoto lbl) rs m E0 (rs#PC <- pc) m + | exec_MBcond_true cond args lbl rs m pc rs': + eval_condition cond (to_Machrs rs)##args m = Some true -> + goto_label f lbl rs = Some pc -> + rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs -> + cfi_step f (MBcond cond args lbl) rs m E0 (rs'#PC <- pc) m + | exec_MBcond_false cond args lbl rs m rs': + eval_condition cond (to_Machrs rs)##args m = Some false -> + rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs -> + cfi_step f (MBcond cond args lbl) rs m E0 rs' m + | exec_MBjumptable arg tbl rs m index lbl pc rs': + to_Machrs rs arg = Vint index -> + list_nth_z tbl (Int.unsigned index) = Some lbl -> + goto_label f lbl rs = Some pc -> + rs' = set_from_Machrs (undef_regs destroyed_by_jumptable rs) rs -> + cfi_step f (MBjumptable arg tbl) rs m E0 (rs'#PC <- pc) m + | exec_MBbuiltin rs m ef args res vargs t vres rs' m': + eval_builtin_args ge (to_Machrs rs) (rs#SP) m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = set_from_Machrs (set_res res vres (undef_regs (destroyed_by_builtin ef) rs)) rs -> + cfi_step f (MBbuiltin ef args res) rs m t rs' m' + . + +Inductive exit_step f : option control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop := + | exec_Some_exit ctl rs m t rs' m': + cfi_step f ctl rs m t rs' m' -> + exit_step f (Some ctl) rs m t rs' m' + | exec_None_exit rs m: + exit_step f None rs m E0 rs m + . + +Inductive exec_bblock f: bblock -> regset -> mem -> trace -> regset -> mem -> Prop := + | exec_bblock_all (bb: bblock) rs0 m0 rs1 m1 pc t rs2 m2: + body_step f (body bb) rs0 m0 rs1 m1 -> + next_addr f rs1 = Some pc -> + exit_step f (exit bb) (rs1#PC <- pc) m1 t rs2 m2 -> + exec_bblock f bb rs0 m0 t rs2 m2. + +Definition exec_prologue f (pos:Z) (rs: regset) (m:mem) : option state := + if Z.eq_dec pos 0 then + let (m1, stk) := Mem.alloc m 0 f.(fn_stacksize) in + let sp := Vptr stk Ptrofs.zero in + SOME m2 <- store_stack m1 sp Tptr f.(fn_link_ofs) rs#SP IN + SOME m3 <- store_stack m2 sp Tptr f.(fn_retaddr_ofs) rs#RA IN + Next ((set_from_Machrs (undef_regs destroyed_at_function_entry rs) rs)#SP <- sp) m3 + else + Next rs m. + + +Inductive step: state -> trace -> state -> Prop := + | exec_step_internal b ofs f bb c rs0 m0 rs1 m1 t rs2 m2: + rs0 PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + is_pos f (Ptrofs.unsigned ofs) (bb::c) -> + exec_prologue f (Ptrofs.unsigned ofs) rs0 m0 = Next rs1 m1 -> + exec_bblock f bb rs1 m1 t rs2 m2 -> + step (State rs0 m0) t (State rs2 m2) + | exec_step_external: + forall b ef args res rs m t rs' m', + rs PC = Vptr b Ptrofs.zero -> + Genv.find_funct_ptr ge b = Some (External ef) -> + extcall_arguments (to_Machrs rs) m (rs#SP) (ef_sig ef) args -> + external_call ef ge args m t res m' -> + rs' = (set_from_Machrs (set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs)) rs) #PC <- (rs RA) -> + step (State rs m) t (State rs' m'). + +End RELSEM. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + let rs0 := + (Pregmap.init Vundef) + # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero) + # SP <- Vnullptr + # RA <- Vnullptr in + initial_state p (State rs0 m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall rs m r retcode, + loc_result signature_main = One r -> + rs PC = Vnullptr -> + rs r = Vint retcode -> + final_state (State rs m) retcode. + +Definition semantics (next: function -> Z -> Z) (p: program) := + Semantics (step next) (initial_state p) final_state (Genv.globalenv p). |