diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-14 11:42:11 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-14 11:42:11 +0100 |
commit | afa25aac9373e4a7b37433ed861257a630264c29 (patch) | |
tree | c835f6b8371d998f04e66347a7e6f9bb3eda3db4 /mppa_k1c/Asmvliw.v | |
parent | 802badd4bdf9b0e836935b74a25facb245558004 (diff) | |
download | compcert-kvx-afa25aac9373e4a7b37433ed861257a630264c29.tar.gz compcert-kvx-afa25aac9373e4a7b37433ed861257a630264c29.zip |
definition of VLIW semantics
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
-rw-r--r-- | mppa_k1c/Asmvliw.v | 329 |
1 files changed, 329 insertions, 0 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v new file mode 100644 index 00000000..2c88673b --- /dev/null +++ b/mppa_k1c/Asmvliw.v @@ -0,0 +1,329 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Prashanth Mundkur, SRI International *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* The contributions by Prashanth Mundkur are reused and adapted *) +(* under the terms of a Contributor License Agreement between *) +(* SRI International and INRIA. *) +(* *) +(* *********************************************************************) + +(** Abstract syntax and semantics for K1c assembly language. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Locations. +Require Stacklayout. +Require Import Conventions. +Require Import Errors. +Require Import Asmblock. + +Local Open Scope asm. + +Section RELSEM. + +(** Execution of arith instructions *) + +Variable ge: genv. + +(* TODO: on pourrait mettre ça dans Asmblock pour factoriser le code + en définissant + exec_arith_instr ai rs := parexec_arith_instr ai rs rs +*) +Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := + match ai with + | PArithR n d => rsw#d <- (arith_eval_r ge n) + + | PArithRR n d s => rsw#d <- (arith_eval_rr n rsr#s) + + | PArithRI32 n d i => rsw#d <- (arith_eval_ri32 n i) + | PArithRI64 n d i => rsw#d <- (arith_eval_ri64 n i) + | PArithRF32 n d i => rsw#d <- (arith_eval_rf32 n i) + | PArithRF64 n d i => rsw#d <- (arith_eval_rf64 n i) + + | PArithRRR n d s1 s2 => rsw#d <- (arith_eval_rrr n rsr#s1 rsr#s2) + + | PArithRRI32 n d s i => rsw#d <- (arith_eval_rri32 n rsr#s i) + + | PArithRRI64 n d s i => rsw#d <- (arith_eval_rri64 n rsr#s i) + end. + +(** * load/store *) + +(* TODO: factoriser ? *) +Definition parexec_load (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) + (d: ireg) (a: ireg) (ofs: offset) := + match (eval_offset ge ofs) with + | OK ptr => + match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with + | None => Stuck + | Some v => Next (rsw#d <- v) mw + end + | _ => Stuck + end. + +(* rem: parexec_store = exec_store *) + +(** * basic instructions *) + +(* TODO: factoriser ? *) +Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := + match bi with + | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw + + | PLoadRRO n d a ofs => parexec_load (load_chunk n) rsr rsw mr mw d a ofs + + | PStoreRRO n s a ofs => exec_store ge (store_chunk n) rsr mr s a ofs + + | Pallocframe sz pos => + let (mw, stk) := Mem.alloc mr 0 sz in + let sp := (Vptr stk Ptrofs.zero) in + match Mem.storev Mptr mw (Val.offset_ptr sp pos) rsr#SP with + | None => Stuck + | Some mw => Next (rsw #FP <- (rsr SP) #SP <- sp #RTMP <- Vundef) mw + end + + | Pfreeframe sz pos => + match Mem.loadv Mptr mr (Val.offset_ptr rsr#SP pos) with + | None => Stuck + | Some v => + match rsr SP with + | Vptr stk ofs => + match Mem.free mr stk 0 sz with + | None => Stuck + | Some mw => Next (rsw#SP <- v #RTMP <- Vundef) mw + end + | _ => Stuck + end + end + | Pget rd ra => + match ra with + | RA => Next (rsw#rd <- (rsr#ra)) mw + | _ => Stuck + end + | Pset ra rd => + match ra with + | RA => Next (rsw#ra <- (rsr#rd)) mw + | _ => Stuck + end + | Pnop => Next rsw mw +end. + +(* parexec with writes-in-order *) +Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) := + match body with + | nil => Next rsw mw + | bi::body' => + match parexec_basic_instr bi rsr rsw mr mw with + | Next rsw mw => parexec_wio_body body' rsr rsw mr mw + | Stuck => Stuck + end + end. + +(** Manipulations over the [PC] register: continuing with the next + instruction ([nextblock]) or branching to a label ([goto_label]). *) + +(* TODO: factoriser ? *) +Definition par_nextblock size_b (rsr rsw: regset) := + rsw#PC <- (Val.offset_ptr rsr#PC size_b). + +(* TODO: factoriser ? *) +Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) := + match label_pos lbl 0 (fn_blocks f) with + | None => Stuck + | Some pos => + match rsr#PC with + | Vptr b ofs => Next (rsw#PC <- (Vptr b (Ptrofs.repr pos))) mw + | _ => Stuck + end + end. + +(** Evaluating a branch + +Warning: in m PC is assumed to be already pointing on the next instruction ! + +*) +(* TODO: factoriser ? *) +Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) := + match res with + | Some true => par_goto_label f l rsr rsw mw + | Some false => Next rsw mw + | None => Stuck + end. + + +(** Execution of a single control-flow instruction [i] in initial state [rs] and + [m]. Return updated state. + + As above: PC is assumed to be incremented on the next block before the control-flow instruction + + For instructions that correspond tobuiltin + actual RISC-V instructions, the cases are straightforward + transliterations of the informal descriptions given in the RISC-V + user-mode specification. For pseudo-instructions, refer to the + informal descriptions given above. + + Note that we set to [Vundef] the registers used as temporaries by + the expansions of the pseudo-instructions, so that the RISC-V code + we generate cannot use those registers to hold values that must + survive the execution of the pseudo-instruction. *) + +Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) (mw: mem) := + match oc with + | Some ic => +(** Get/Set system registers *) + match ic with + + +(** Branch Control Unit instructions *) + | Pret => + Next (rsw#PC <- (rsr#RA)) mw + | Pcall s => + Next (rsw#RA <- (rsr#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw + | Picall r => + Next (rsw#RA <- (rsr#PC) #PC <- (rsr#r)) mw + | Pgoto s => + Next (rsw#PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw + | Pigoto r => + Next (rsw#PC <- (rsr#r)) mw + | Pj_l l => + par_goto_label f l rsr rsw mw + | Pcb bt r l => + match cmp_for_btest bt with + | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val.cmp_bool c rsr#r (Vint (Int.repr 0))) + | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.cmpl_bool c rsr#r (Vlong (Int64.repr 0))) + | (None, _) => Stuck + end + | Pcbu bt r l => + match cmpu_for_btest bt with + | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val_cmpu_bool c rsr#r (Vint (Int.repr 0))) + | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val_cmplu_bool c rsr#r (Vlong (Int64.repr 0))) + | (None, _) => Stuck + end + + +(** Pseudo-instructions *) + | Pbuiltin ef args res => + Stuck (**r treated specially below *) + end + | None => Next rsw mw +end. + + +Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: mem): outcome := + match parexec_wio_body bdy rs rs m m with + | Next rsw mw => + let rsw := par_nextblock size_b rs rsw in + parexec_control f ext rs rsw mw + | Stuck => Stuck + end. + +(* utile ? *) +Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome := + parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m. + + +Require Import Sorting.Permutation. + +Inductive parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome -> Prop := + parexec_bblock_Next bdy1 bdy2 rsw mw: + Permutation (bdy1++bdy2) (body b) -> + parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Next rsw mw -> + parexec_bblock f b rs m (parexec_wio_body bdy2 rs rsw m mw) + | parexec_bblock_Stuck bdy1 bdy2: + Permutation (bdy1++bdy2) (body b) -> + parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Stuck -> + parexec_bblock f b rs m Stuck. + + +Inductive step: state -> trace -> state -> Prop := + | exec_step_internal: + forall b ofs f bi rs m rs' m', + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi -> + exec_bblock ge f bi rs m = Next rs' m' -> + parexec_bblock f bi rs m (Next rs' m') -> + step (State rs m) E0 (State rs' m') + | exec_step_builtin: + forall b ofs f ef args res rs m vargs t vres rs' m' bi, + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_bblock (Ptrofs.unsigned ofs) f.(fn_blocks) = Some bi -> + exit bi = Some (PExpand (Pbuiltin ef args res)) -> + eval_builtin_args ge rs (rs SP) m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = nextblock bi + (set_res res vres + (undef_regs (map preg_of (destroyed_by_builtin ef)) + (rs#RTMP <- Vundef))) -> + step (State rs m) t (State rs' m') + | 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) -> + external_call ef ge args m t res m' -> + extcall_arguments rs m (ef_sig ef) args -> + rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs rs))#PC <- (rs RA) -> + step (State rs m) t (State rs' m') + . + +End RELSEM. + +(** Execution of whole programs. *) + +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + +Lemma semantics_determinate: forall p, determinate (semantics p). +Proof. +Ltac Equalities := + match goal with + | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => + rewrite H1 in H2; inv H2; Equalities + | _ => idtac + end. + intros; constructor; simpl; intros. +- (* determ *) + inv H; inv H0; Equalities. + + split. constructor. auto. + + unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate. + rewrite H10 in H4. discriminate. + + unfold exec_bblock in H14. (* FIXME: destruct (exec_body _ _ _ _); try discriminate. + rewrite H4 in H13. discriminate. + + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H6. eexact H13. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. + + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. + exploit external_call_determ. eexact H3. eexact H8. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. +- (* trace length *) + red; intros. inv H; simpl. + omega. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. +- (* initial states *) + inv H; inv H0. f_equal. congruence. +- (* final no step *) + assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs). + { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. } + inv H. unfold Vzero in H0. red; intros; red; intros. + inv H; rewrite H0 in *; eelim NOTNULL; eauto. +- (* final states *) + inv H; inv H0. congruence. *) +Admitted.
\ No newline at end of file |