From 6ce4efc2b6ecd6ecbd4739f81c439b2f9420bcd9 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 27 Oct 2020 11:37:11 +0100 Subject: another start for Asmblockgen --- aarch64/Asmblockgen.v | 183 ++++++++++++++------------------------------------ 1 file changed, 52 insertions(+), 131 deletions(-) (limited to 'aarch64/Asmblockgen.v') diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 1dc7ca12..fc07bbb9 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -199,132 +199,31 @@ Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) := Definition negate_decomposition (l: list (Z * Z)) := List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l. -(* XXX Que faire des rd ici ? inutiles ? *) -(* XXX Faudra-t-il remplacer arith_pp par un type abstrait ? *) +(* TODO: Coercions to move in Asmblock ? *) +Coercion PArithP: arith_p >-> Funclass. +Coercion PArithPP: arith_pp >-> Funclass. +Coercion PArithRR0: arith_rr0 >-> Funclass. +Coercion PArith: ar_instruction >-> basic. -(* XXX Move this in Asmblock.v ? *) - -(*Inductive iar: Type :=*) - (*| IArithP (i: arith_p)*) - (*| IArithPP (i: arith_pp)*) - (*| IArithRR0 (i: arith_rr0).*) - -(*Coercion IArithP: arith_p >-> iar.*) -(*Coercion IArithPP: arith_pp >-> iar.*) -(*Definition larith := list iar.*) - -(*Fixpoint extract_larith_p (l: larith) :=*) - (*match l with*) - (*| nil => nil*) - (*| IArithP i :: l' => i :: extract_larith_p l'*) - (*| _ => nil*) - (*end.*) - -(*Fixpoint extract_larith_pp (l: larith) :=*) - (*match l with*) - (*| nil => nil*) - (*| IArithPP i :: l' => i :: extract_larith_pp l'*) - (*| _ => nil*) - (*end.*) - -(*Fixpoint larith_p_to_larith (l: list arith_p): larith :=*) - (*match l with*) - (*| nil => nil*) - (*| ar :: l' => IArithP ar :: (larith_p_to_larith l')*) - (*end.*) - -(*Fixpoint larith_pp_to_larith (l: list arith_pp): larith :=*) - (*match l with*) - (*| nil => nil*) - (*| ar :: l' => IArithPP ar :: (larith_pp_to_larith l')*) - (*end.*) - -(*Coercion PArithP: arith_p >-> Funclass.*) -(*Coercion PArithPP: arith_pp >-> Funclass.*) -(*Coercion PArithRR0: arith_rr0 >-> Funclass.*) - -(*Definition bcode := list basic.*) -(*Definition larith := list ar_instruction.*) -(*Definition larith_p := list arith_p.*) -(*Definition larith_pp := list arith_pp.*) -(*Definition larith_rr0 := list arith_rr0.*) - -(*Coercion PBasic: basic >-> instruction.*) -(*Coercion PControl: control >-> instruction.*) -(*Coercion PArith: ar_instruction >-> basic.*) - -Inductive basic : Type := - | I_BI (i: basic) - | I_Arith (i: ar_instruction) - | I_ArithP (i : arith_p) - | I_ArithPP (i : arith_pp) - | I_ArithRR0 (i : arith_rr0). - -Inductive instruction : Type := - | PBasic (i: basic) - | PControl (i: control) -. - -Definition code := list instruction. Definition bcode := list basic. -Fixpoint extract_basic (c: code) := - match c with - | nil => nil - | PBasic i :: c => i :: (extract_basic c) - | PControl i :: c => nil - end. +Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity). +(* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *) -Fixpoint extract_ctl (c: code) := - match c with - | nil => None - | PBasic i :: c => extract_ctl c - | PControl i :: nil => Some i - | PControl i :: _ => None (* if the first found control instruction isn't the last *) - end. - -(*Definition code := list instruction.*) - -(*Coercion PArith: ar_instruction >-> basic.*) -(*Coercion I_bi: bcode >-> code.*) -(*Coercion I_larith: larith >-> code.*) -(*Coercion I_larith_p: larith_p >-> code.*) -(*Coercion I_larith_pp: larith_pp >-> code.*) -(*Coercion I_larith_rr0: larith_rr0 >-> code.*) - -(*Fixpoint extract_larith (c: code) :=*) - (*match c with*) - (*| nil => nil*) - (*| PArith i :: l' => i :: extract_larith l'*) - (*| _ => nil*) - (*end.*) - -(*Fixpoint extract_larith_p (c: code) :=*) - (*match c with*) - (*| I_larith_p i :: l => i :: extract_larith_p l*) - (*| _ => nil*) - (*end.*) - -(*Fixpoint extract_arith_pp (ar: arith_pp) :=*) - (*match ar with*) - (*| Pmovk i => i :: extract_larith_pp l*) - (*| _ => nil*) - (*end.*) Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode := - List.fold_right ( - fun np k => (I_ArithPP (Pmovk sz (fst np) (snd np))) :: k) k l. + List.fold_right (fun np k => Pmovk sz (fst np) (snd np) rd rd ::bi k) k l. Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode := match l with - | nil => I_ArithP (Pmovz sz 0 0) :: k - | (n1, p1) :: l => I_ArithP (Pmovz sz n1 p1) :: loadimm_k sz rd l k + | nil => Pmovz sz 0 0 rd ::bi k + | (n1, p1) :: l => (Pmovz sz n1 p1 rd) ::bi loadimm_k sz rd l k end. Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode := match l with - | nil => I_ArithP (Pmovn sz 0 0) :: k - | (n1, p1) :: l => I_ArithP (Pmovn sz n1 p1) :: loadimm_k sz rd (negate_decomposition l) k + | nil => Pmovn sz 0 0 rd ::bi k + | (n1, p1) :: l => Pmovn sz n1 p1 rd ::bi loadimm_k sz rd (negate_decomposition l) k end. Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: bcode) : bcode := @@ -337,12 +236,12 @@ Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: bcode) : bcode := Definition loadimm32 (rd: ireg) (n: int) (k: bcode) : bcode := if is_logical_imm32 n - then I_ArithRR0 (Porrimm W (Int.unsigned n)) :: k + then Porrimm W (Int.unsigned n) rd XZR ::bi k else loadimm W rd (Int.unsigned n) k. Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode := if is_logical_imm64 n - then I_ArithRR0 (Porrimm X (Int64.unsigned n)) :: k + then Porrimm X (Int64.unsigned n) rd XZR ::bi k else loadimm X rd (Int64.unsigned n) k. (** Translation of the arithmetic operation [r <- op(args)]. @@ -405,7 +304,7 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool := (** This is an equivalent definition in continuation-passing style that runs in constant stack space. *) - +(* Fixpoint transl_code_rec (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode -> res bcode) := match il with @@ -417,14 +316,14 @@ Fixpoint transl_code_rec (f: Machblock.function) (il: list Machblock.basic_inst) Definition transl_code' (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := transl_code_rec f il it1p (fun c => OK c). +*) - -Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := +Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):= match il with | nil => OK nil | i1 :: il' => - do k <- transl_basic_code f il' (it1_is_parent it1p i1); - transl_instr_basic f i1 it1p k + do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k; + transl_instr_basic f i1 it1p k1 end. (** Translation of a whole function. Note that we must check @@ -432,13 +331,15 @@ Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_ins otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) +(* NB Sylvain: this issue with PExpand seems specific to kvx -- and not necessary here *) (* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *) +(* Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instruction) := match (extract_ctl ctl) with | None => match c with | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil - | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil + | i :: c => {| header := hd; body := ((i :: c) ++ extract_basic ctl); exit := None |} :: nil end | Some (PExpand (Pbuiltin ef args res)) => match c with @@ -449,21 +350,41 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil end . +*) -Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) := - do c <- transl_basic_code f fb.(Machblock.body) ep; - do ctl <- nil; (*transl_instr_control f fb.(Machblock.exit);*) - OK (gen_bblocks fb.(Machblock.header) c ctl) -. +(* XXX: the simulation proof may be complex with this pattern. We may fix this later *) +Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control) (k:bblocks): bblocks := + match non_empty_bblockb bdy ex with + | true => {| header := ll; body:= bdy; exit := ex |}::k + | false => k + end. +Obligation 1. + rewrite <- Heq_anonymous. constructor. +Qed. + +Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*control) := + Error (msg ("not yet implemented")). + +Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) (ep: bool) : res (bcode*option control) := + match ext with + Some ctl => do (b,c) <- transl_control f ctl ep; OK (b, Some c) + | None => OK (nil, None) + end. + +Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) (k:bblocks): res (list bblock) := + let stub := false in (* TODO: FIXME *) + do (bdy, ex) <- transl_exit f fb.(Machblock.exit) stub; + do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy; + OK (cons_bblocks fb.(Machblock.header) bdy' ex k) + . -Program Definition transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks := +Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks := match lmb with | nil => OK nil | mb :: lmb => - do lb <- transl_block f mb (if Machblock.header mb then ep else false); - do lb' <- transl_blocks f lmb false; - OK (lb @@ lb') - end + do lb <- transl_blocks f lmb false; (* TODO: check [false] here *) + transl_block f mb (if Machblock.header mb then ep else false) lb (* TODO: check this *) + end. (* OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *)*) (* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *) -- cgit