From ccd6cc8f48fe9c312a716ce01d547626d7d13b9a Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Thu, 5 May 2016 16:24:20 -0400 Subject: Finished first draft of PseudoConversions --- src/Assembly/Pseudo.v | 7 +-- src/Assembly/PseudoConversion.v | 121 ++++++++++++++++++++++++++++------------ 2 files changed, 88 insertions(+), 40 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index edb95d38a..10f9f4ab2 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -43,7 +43,7 @@ Module Pseudo (M: PseudoMachine) <: Language. Definition State := list const. Inductive WBinOp: Set := - | Wplus: WBinOp | Wmult: WBinOp + | Wplus: WBinOp | Wminus: WBinOp | Wand: WBinOp. Inductive WNatOp: Set := @@ -57,8 +57,8 @@ Module Pseudo (M: PseudoMachine) <: Language. | PConst: forall n, const -> Pseudo n 1 | PBin: forall n, WBinOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 1 - | PNat: forall n, WNatOp -> nat -> Pseudo n 1 - | PShift: forall n, WShiftOp -> Pseudo n 1 -> nat -> Pseudo n 1 + | PNat: forall n, WNatOp -> Index width -> Pseudo n 1 + | PShift: forall n, WShiftOp -> Pseudo n 1 -> Index width -> Pseudo n 1 | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m | PComp: forall n k m, Pseudo n k -> Pseudo k m -> Pseudo n m @@ -74,7 +74,6 @@ Module Pseudo (M: PseudoMachine) <: Language. Definition applyBin (op: WBinOp) (a b: word width): option (list const) := match op with | Wplus => Some [(wplus a b)] - | Wmult => Some [(wmult a b)] | Wminus => Some [(wminus a b)] | Wand => Some [(wand a b)] end. diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v index cf5a3d11b..9050dc94e 100644 --- a/src/Assembly/PseudoConversion.v +++ b/src/Assembly/PseudoConversion.v @@ -25,14 +25,14 @@ Module PseudoConversion (M: PseudoMachine). Import P M. Definition activeRegisters := 5. - Definition r0 := ireg 5. + Definition r0 := ireg 5. (* Invariant: these are never used in a Mapping *) Definition r1 := ireg 6. - Definition convertState (st: AlmostQhasm.State): P.State := + Definition convertState (st: AlmostQhasm.State): option P.State := match st with | fullState _ stackState _ => - take vars (map (fun x => NToWord width (snd x)) - (NatM.elements stackState)) + Some (take vars (map (fun x => NToWord width (snd x)) + (NatM.elements stackState))) end. Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}. @@ -157,16 +157,18 @@ Module PseudoConversion (M: PseudoMachine). (AOp (IOpReg width iop ra r0)), regM ra va pa) - | (stackM ra va _, stackM rb vb _) => + | (stackM ra va pa, stackM rb vb _) => (ASeq (AAssign (ARegStackInt width r1 ra)) (ASeq (AAssign (ARegStackInt width r0 rb)) - (AOp (IOpReg width iop r1 r0))), - regM r1 (getIRegIndex r1) eq_refl) + (ASeq (AOp (IOpReg width iop r1 r0)) + (AAssign (AStackRegInt width ra r1)))), + stackM ra va pa) - | (stackM ra va _, constM rb vb _) => - (ASeq (AAssign (ARegStackInt width r1 ra)) - (AOp (IOpConst width iop r1 rb)), - regM r1 (getIRegIndex r1) eq_refl) + | (stackM ra va pa, constM rb vb _) => + (ASeq (AAssign (ARegStackInt width r0 ra)) + (ASeq (AOp (IOpConst width iop r0 rb)) + (AAssign (AStackRegInt width ra r0))), + stackM ra va pa) | (constM ra va _, constM rb vb _) => (ASkip, @@ -187,8 +189,10 @@ Module PseudoConversion (M: PseudoMachine). | regM r v _ => (AOp (OpRot width qop r n), regM r (getIRegIndex r) eq_refl) | stackM r v _ => - (ASeq (AAssign (ARegStackInt width r1 r)) (AOp (OpRot width qop r1 n)), - regM r1 (getIRegIndex r1) eq_refl) + (ASeq (AAssign (ARegStackInt width r0 r)) + (ASeq (AOp (OpRot width qop r0 n)) + (AAssign (AStackRegInt width r r0))), + m) | constM r v _ => (ASkip, wordToConstM match qop with @@ -200,9 +204,8 @@ Module PseudoConversion (M: PseudoMachine). Fixpoint convertProgram' {n m} (prog: Pseudo n m) (mapping: list Mapping) - (avoid: list Mapping) - (ret: nat): - option (AlmostQhasm.Program * list nat) := + (avoid: list Mapping): + option (AlmostQhasm.Program * list Mapping) := let option_map' := fun x f => option_map f x in let otup_map := fun x f => @@ -220,40 +223,86 @@ Module PseudoConversion (M: PseudoMachine). option_map' (nth_error mapping n) (fun v => (ASkip, [v])) | PConst n c => - (ASkip, [constM (iconst c) (getIConstValue (iconst c)) eq_refl]) + Some (ASkip, [constM (iconst c) (getIConstValue (iconst c)) eq_refl]) | PBin n o a b => - let ret' := (ret + 1) mod activeRegisters in - let tmp0 := freshMapping (avoid ++ mapping) n in - let tmp1 := freshMapping (avoid ++ mapping ++ tmp0) m in - - otup_map (convertProgram' a mapping avoid ret) (fun aprog amap => - otup_map (convertProgram' b mapping avoid ret') (fun bprog bmap => - let m0 := moveMapping mapping tmp0 in - let m1 := moveMapping bmap tmp1 in + otup_map (convertProgram' a mapping avoid) (fun aprog amap => + let tmp := freshMapping (avoid ++ mapping ++ amap) n in + let mov := moveMapping mapping tmp in + otup_map (convertProgram' b tmp (avoid ++ amap)) (fun bprog bmap => match (amap, bmap) with - | ([av], [bv]) => - let oper := binProg m o av bv r1 in - Some (ASeq m0 (ASeq bprog (ASeq m1 (ASeq aprog oper))), amap) + | ([av], [bv]) => let oper := binProg o av bv in + + Some (ASeq mov (ASeq bprog (ASeq aprog (fst oper))), [snd oper]) | _ => None end)) - | PNat n o v => None + | PNat n o v => + match (applyNat o v) with + | Some [c] => let ic := iconst c in - | PShift n o a x => None + Some (ASkip, [constM ic (getIConstValue ic) eq_refl]) - | PLet n k m f g => None + | _ => None + end - | PComp n k m f g => None + | PShift n o a x => + otup_map (convertProgram' a mapping avoid) (fun aprog amap => + match amap with + | [av] => let oper := shiftProg o av x in - | PComb n a b f g => None + Some (ASeq aprog (fst oper), [snd oper]) - | PIf n m o i0 i1 l r => None + | _ => None + end) - | PFunExp n f e => None + | PLet n k m f g => + otup_map (convertProgram' f mapping avoid) (fun fprog fmap => + otup_map (convertProgram' g (mapping ++ fmap) avoid) (fun gprog gmap => + Some (ASeq fprog gprog, gmap))) + + | PComp n k m f g => + otup_map (convertProgram' f mapping avoid) (fun fprog fmap => + otup_map (convertProgram' g fmap avoid) (fun gprog gmap => + Some (ASeq fprog gprog, gmap))) + + | PComb n a b f g => + otup_map (convertProgram' f mapping avoid) (fun fprog fmap => + otup_map (convertProgram' g (mapping ++ fmap) avoid) (fun gprog gmap => + Some (ASeq fprog gprog, fmap ++ gmap))) + + | PIf n m o i0 i1 l r => + otup_map (convertProgram' l mapping avoid) (fun lprog lmap => + otup_map (convertProgram' r mapping avoid) (fun rprog rmap => + match (nth_error mapping i0, nth_error mapping i1) with + | (Some (regM a _ _), Some (regM b _ _)) => + Some (ACond (TestInt width o a b) lprog (ASeq rprog (moveMapping rmap lmap)), lmap) + | _ => None + end)) + + | PFunExp n f e => + otup_map (convertProgram' f mapping avoid) (fun fprog fmap => + let mov := moveMapping mapping fmap in + + match (freshMapping (avoid ++ fmap) 1) with + | [regM rc _ _] => + Some (ASeq mov + (ASeq (AAssign (AConstInt width rc (iconst (natToWord width e)))) + (AWhile (TestInt width TGt rc r0) + (ASeq fprog + (ASeq (AAssign (AConstInt width r0 (iconst (wzero width)))) + (AOp (IOpConst width IMinus rc (iconst (natToWord width 1)))))))), fmap) + | [stackM sc _ _] => None + | _ => None + end) + end. + Definition convertProgram (prog: Pseudo vars vars): option AlmostQhasm.Program := + match (convertProgram' prog (freshMapping [] vars) []) with + | Some (prog', _) => Some prog' + | _ => None end. Lemma convert_spec: forall a a' b b' prog prog', @@ -263,4 +312,4 @@ Module PseudoConversion (M: PseudoMachine). Admitted. End Conv. -End PseudoConversions. +End PseudoConversion. -- cgit v1.2.3