diff options
-rw-r--r-- | _CoqProject | 12 | ||||
-rw-r--r-- | src/Assembly/Medial.v | 23 | ||||
-rw-r--r-- | src/Assembly/PipelineExample.v | 2 | ||||
-rw-r--r-- | src/Assembly/PseudoMedialConversion.v | 162 |
4 files changed, 115 insertions, 84 deletions
diff --git a/_CoqProject b/_CoqProject index a51cfed80..6d2b3a880 100644 --- a/_CoqProject +++ b/_CoqProject @@ -30,15 +30,3 @@ src/Util/NatUtil.v src/Util/NumTheoryUtil.v src/Util/WordUtil.v src/Util/ZUtil.v -src/Assembly/AlmostConversion.v -src/Assembly/AlmostQhasm.v -src/Assembly/BoundedWord.v -src/Assembly/Conversion.v -src/Assembly/GallinaConversion.v -src/Assembly/Language.v -src/Assembly/Qhasm.v -src/Assembly/State.v -src/Assembly/QhasmCommon.v -src/Assembly/QhasmEvalCommon.v -src/Assembly/QhasmUtil.v -src/Assembly/StringConversion.v diff --git a/src/Assembly/Medial.v b/src/Assembly/Medial.v index e46dd5547..5f082aa12 100644 --- a/src/Assembly/Medial.v +++ b/src/Assembly/Medial.v @@ -13,7 +13,7 @@ Module Medial (Arch: PseudoMachine) <: Language. Inductive MAssignment : Type := | MAVar: nat -> nat -> MAssignment - | MAMem: nat -> nat -> nat -> MAssignment + | MAMem: forall m, nat -> nat -> Index m -> MAssignment | MAConst: nat -> W -> MAssignment. Inductive MOperation := @@ -24,7 +24,9 @@ Module Medial (Arch: PseudoMachine) <: Language. | MOpRot: RotOp -> nat -> Index width -> MOperation. Inductive MConditional := - | MC: TestOp -> nat -> nat -> MConditional. + | MZ: nat -> MConditional + | MCReg: TestOp -> nat -> nat -> MConditional + | MCConst: TestOp -> nat -> W -> MConditional. Inductive Medial: Set := | MSkip: Medial @@ -80,7 +82,7 @@ Module Medial (Arch: PseudoMachine) <: Language. | _ => None end - | MAMem x y i => + | MAMem _ x y i => match (getMem y i st) with | Some v => Some (setVar x v st) | _ => None @@ -129,7 +131,13 @@ Module Medial (Arch: PseudoMachine) <: Language. | MCond c a b => match c with - | MC t x y => + | MCConst t x y => + omap (getVar x st) (fun vx => + if (evalTest t vx y) + then meval a st + else meval b st) + + | MCReg t x y => omap (getVar x st) (fun vx => (* TODO: why can't we infer width here? *) @@ -137,6 +145,13 @@ Module Medial (Arch: PseudoMachine) <: Language. if (evalTest t vx vy) then meval a st else meval b st)) + + | MZ x => + omap (getVar x st) (fun vx => + if (evalTest TEq vx (wzero width)) + then meval a st + else meval b st) + end | MFunexp n a => diff --git a/src/Assembly/PipelineExample.v b/src/Assembly/PipelineExample.v index d4cd4d142..b17a85c9b 100644 --- a/src/Assembly/PipelineExample.v +++ b/src/Assembly/PipelineExample.v @@ -45,4 +45,4 @@ Module Progs. Print result. End Progs. -(* Extraction "Progs.ml" Progs. *) +Extraction "Progs.ml" Progs. diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v index 81ef5dc41..055c6d1bf 100644 --- a/src/Assembly/PseudoMedialConversion.v +++ b/src/Assembly/PseudoMedialConversion.v @@ -1,7 +1,7 @@ Require Export Language Conversion QhasmEvalCommon QhasmUtil. Require Export Pseudo Medial AlmostQhasm State. -Require Export Bedrock.Word NArith NPeano. +Require Export Bedrock.Word NArith NPeano Euclid. Require Export List Sumbool. Require Import FMapAVL FMapList JMeq. Require Import Vector. @@ -66,7 +66,7 @@ Module PseudoMedialConversion (Arch: PseudoMachine). match prog with | PVar n i => Some (MSkip, [start]) | PConst n c => Some (MAssign (MAConst start c), [start]) - | PMem n m v i => Some (MAssign (MAMem start v i), [start]) + | PMem n m v i => Some (MAssign (MAMem _ start v i), [start]) | PBin n o p => match (convertProgram' p start) with @@ -116,7 +116,7 @@ Module PseudoMedialConversion (Arch: PseudoMachine). lt <- convertProgram' l start; rt <- convertProgram' r start; match (lt, rt) with - | ((lp, lr), (rp, rr)) => Some (MCond (MC o i0 i1) lp rp, lr) + | ((lp, lr), (rp, rr)) => Some (MCond (MCReg o i0 i1) lp rp, lr) end (* TODO: prove that all (Pseudo n m) will return the same list *) @@ -178,41 +178,33 @@ Module PseudoMedialConversion (Arch: PseudoMachine). End PseudoConversion. Module MedialConversion <: Conversion M AlmostQhasm. + Import Arch M FullState. - Import Arch M. + Definition ireg (x: nat): Reg width := reg width_spec x. + Definition iconst (x: word width): Const width := const width_spec x. + Definition istack (x: nat): Stack width := stack width_spec x. - Definition width_dec : {width = 32} + {width = 64}. - destruct width_spec; first [ - left; abstract intuition - | right; abstract intuition]. - Defined. + Definition tmpMap: nat -> Mapping width := (fun x => regM width (ireg x)). - Definition ireg (x: nat): Reg width := - reg width_spec x. - - Definition iconst (x: word width): Const width := - const width_spec x. - - Definition istack (x: nat): Stack width := - stack width_spec x. - - Fixpoint convertState (st: AlmostQhasm.State): option M.State := - let try_cons := fun (k: nat) (x: option N) (m: DefMap) => - match x with | Some x' => NatM.add k x' m | _ => m end in + Definition getMapping (m: Mapping width) (st: AlmostQhasm.State): option (word width) := + match m with + | regM r => getReg r st + | stackM s => getStack s st + | _ => None + end. - let get (n: nat): option N := - match (getIntReg (ireg n) st, getStack (stack n) st) with - | (Some v, _) => Some (wordToN v) - | (_, Some v) => Some (wordToN v) - | _ => None - end in + Definition convertState' (mapF: nat -> Mapping width) (st: AlmostQhasm.State): option M.State := + let tryAddVar := fun (k: nat) (x: option (word width)) (st: M.State) => + match x with | Some x' => MedState.setVar k x' st | _ => st end in - Some ( - (fix cs' (n: nat) := - try_cons n (get n) - (match n with | O => NatM.empty N | S m => cs' m end)) + Some ((fix cs' (n: nat) := + tryAddVar n (getMapping (mapF n) st) + (match n with | O => MedState.emptyState | S m => cs' m end)) vars). + Definition convertState (st: AlmostQhasm.State): option M.State := + convertState' tmpMap st. + Fixpoint convertProgram' (prog: M.Program) (mapF: nat -> Mapping width) @@ -234,21 +226,26 @@ Module PseudoMedialConversion (Arch: PseudoMachine). match a with | MAVar x y => match (mapF x, mapF y) with - | (regM rx _ _, regM ry _ _) => - Some (AAssign (ARegRegInt _ rx ry)) - | (stackM sx _ _, regM ry _ _) => - Some (AAssign (AStackRegInt _ sx ry)) - | (regM rx _ _, stackM sy _ _) => - Some (AAssign (ARegStackInt _ rx sy)) - | (regM rx _ _, constM cy _ _) => - Some (AAssign (AConstInt _ rx cy)) + | (regM rx, regM ry) => + Some (AAssign (ARegReg rx ry)) + | (stackM sx, regM ry) => + Some (AAssign (AStackReg sx ry)) + | (regM rx, stackM sy) => + Some (AAssign (ARegStack rx sy)) + | (regM rx, constM cy) => + Some (AAssign (AConstInt rx cy)) | _ => None end | MAConst x c => match (mapF x) with - | (regM rx _ _) => - Some (AAssign (AConstInt _ rx (iconst c))) + | (regM rx) => Some (AAssign (AConstInt rx (iconst c))) + | _ => None + end + + | MAMem m x v i => + match (mapF x) with + | (regM rx) => Some (AAssign (ARegMem rx (@mem _ m width_spec v) i)) | _ => None end end @@ -257,70 +254,101 @@ Module PseudoMedialConversion (Arch: PseudoMachine). match o with | MIOpConst io a c => match (mapF a) with - | (regM ra _ _) => - Some (AOp (IOpConst _ io ra (iconst c))) + | (regM ra) => + Some (AOp (IOpConst io ra (iconst c))) | _ => None end | MIOpReg io a b => match (mapF a, mapF b) with - | (regM ra _ _, regM rb _ _) => - Some (AOp (IOpReg _ io ra rb)) + | (regM ra, regM rb) => + Some (AOp (IOpReg io ra rb)) + | _ => None + end + + | MCOpReg co a b => + match (mapF a, mapF b) with + | (regM ra, regM rb) => + Some (AOp (COp co ra rb)) | _ => None end | MDOpReg duo a b (Some x) => match (mapF a, mapF b, mapF x) with - | (regM ra _ _, regM rb _ _, regM rx _ _) => - Some (AOp (DOpReg _ duo ra rb (Some rx))) + | (regM ra, regM rb, regM rx) => + Some (AOp (DOp duo ra rb (Some rx))) | _ => None end | MDOpReg duo a b None => match (mapF a, mapF b) with - | (regM ra _ _, regM rb _ _) => - Some (AOp (DOpReg _ duo ra rb None)) + | (regM ra, regM rb) => + Some (AOp (DOp duo ra rb None)) | _ => None end | MOpRot ro a c => match (mapF a) with - | (regM ra _ _) => - Some (AOp (OpRot _ ro ra c)) + | (regM ra) => + Some (AOp (ROp ro ra c)) | _ => None end end - | MCond (MC to i0 i1) a b => - let c := (fun x => convertProgram' x mapF nextFree tmp) in + | MCond c a b => - omap (c a) (fun aprog => omap (c b) (fun bprog => - match (mapF i0, mapF i1) with - | (regM r0 _ _, regM r1 _ _) => - Some (ACond (TestInt _ to r0 r1) aprog bprog) - | _ => None + let conv := (fun x => convertProgram' x mapF nextFree tmp) in + + omap (conv a) (fun aprog => omap (conv b) (fun bprog => + match c with + | MCReg t x y => + match (mapF x, mapF y) with + | (regM r0, regM r1) => + Some (ACond (CReg _ t r0 r1) aprog bprog) + | _ => None + end + + | MCConst t x y => + match (mapF x) with + | (regM r) => + Some (ACond (CConst _ t r (iconst y)) aprog bprog) + | _ => None + end + + | MZ x => + match (mapF x) with + | (regM r) => + Some (ACond (CZero _ r) aprog bprog) + | _ => None + end end)) | MFunexp e a => - let c := (fun x => convertProgram' x mapF (S nextFree) tmp) in - omap (c a) (fun aprog => + let conv := (fun x => convertProgram' x mapF (S nextFree) tmp) in + omap (conv a) (fun aprog => match (mapF nextFree, mapF tmp) with - | (regM rf _ _, regM rt _ _) => + | (regM rf, regM rt) => Some (ASeq (ASeq - (AAssign (AConstInt _ rf (iconst (natToWord _ O)))) - (AAssign (AConstInt _ rt (iconst (natToWord _ e))))) - (AWhile (TestInt _ TLt rf rt) + (AAssign (AConstInt rf (iconst (natToWord _ O)))) + (AAssign (AConstInt rt (iconst (natToWord _ e))))) + (AWhile (CReg _ TLt rf rt) (ASeq aprog (ASeq - (AOp (IOpConst _ IPlus rf (iconst (natToWord _ 1)))) - (AAssign (AConstInt _ rt (iconst (natToWord _ e)))))))) + (AOp (IOpConst Add rf (iconst (natToWord _ 1)))) + (AAssign (AConstInt rt (iconst (natToWord _ e)))))))) | _ => None end) + + | MDef lbl f a => + omap (convertProgram' f mapF nextFree tmp) (fun fprog => + omap (convertProgram' a mapF (S nextFree) tmp) (fun aprog => + Some (ADef lbl fprog aprog))) + | MCall lbl => Some (ACall lbl) end. (* TODO (rsloan): make these into parameters *) Definition convertProgram (prog: M.Program): option AlmostQhasm.Program := - convertProgram' prog (fun x => @regToM width width_spec (ireg x)) 100 100. + convertProgram' prog tmpMap 100 100. Lemma convert_spec: forall a a' b b' prog prog', convertProgram prog = Some prog' -> |