From 66a93549d583d6eb231764a3de05569cb58820e4 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Fri, 3 Jun 2016 21:44:54 -0400 Subject: More refactors that will make this whole thing very unstable --- src/Assembly/Pseudo.v | 73 ++++++++++++++++++++++- src/Assembly/PseudoMedialConversion.v | 105 ++++++++++++++++++++++++++++++---- 2 files changed, 165 insertions(+), 13 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index ce2c5878a..1f127f665 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -15,7 +15,8 @@ Module Pseudo (M: PseudoMachine) <: Language. (* Program Types *) Inductive Pseudo: nat -> nat -> Type := - | PVar: forall n, Index n -> Pseudo n 1 + (* Some true for registers, false for stack, None for default *) + | PVar: forall n, option bool -> Index n -> Pseudo n 1 | PMem: forall n m, Index n -> Index m -> Pseudo n 1 | PConst: forall n, const -> Pseudo n 1 @@ -38,7 +39,7 @@ Module Pseudo (M: PseudoMachine) <: Language. Fixpoint pseudoEval {n m} (prog: Pseudo n m) (st: State): option State := match prog with - | PVar n i => omap (getVar i st) (fun x => Some (setList [x] st)) + | PVar n _ i => omap (getVar i st) (fun x => Some (setList [x] st)) | PMem n m v i => omap (getMem v i st) (fun x => Some (setList [x] st)) | PConst n c => Some (setList [c] st) | PBin n o p => @@ -110,7 +111,73 @@ Module Pseudo (M: PseudoMachine) <: Language. Delimit Scope pseudo_notations with p. Open Scope pseudo_notations. - Notation "'LET' A := B 'IN' C" (at level 60, right associativity) : pseudo_notations. + Definition indexize (n: nat) (p: (n > 0)%nat) (x: nat): Index n. + intros; exists (x mod n); + abstract (pose proof (mod_bound_pos x n); omega). + Defined. + + Notation "% A" := (PVar _ (Some false) (indexize _ _ A)) + (at level 20, right associativity) : pseudo_notations. + + Notation "$ A" := (PVar _ (Some true) (indexize _ _ A)) + (at level 20, right associativity) : pseudo_notations. + + Notation "'MEM' ( A , B )" := (PMem _ _ (indexize _ _ A) (indexize _ _ B)) + (at level 20, right associativity) : pseudo_notations. + + Notation "# A" := (PConst _ (natToWord _ A)) + (at level 20, right associativity) : pseudo_notations. + + Notation "A :+: B" := (PBin _ Add (PComb _ _ _ A B)) + (at level 60, right associativity) : pseudo_notations. + + Notation "A :+c: B" := (PCarry _ AddWithCarry (PComb _ _ _ A B)) + (at level 60, right associativity) : pseudo_notations. + + Notation "A :-: B" := (PBin _ Sub (PComb _ _ _ A B)) + (at level 60, right associativity) : pseudo_notations. + + Notation "A :&: B" := (PBin _ And (PComb _ _ _ A B)) + (at level 45, right associativity) : pseudo_notations. + + Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B)) + (at level 45, right associativity) : pseudo_notations. + + Notation "A :|: B" := (PBin _ Or (PComb _ _ _ A B)) + (at level 60, right associativity) : pseudo_notations. + + Notation "A :>>: B" := (PShift _ Shr (indexize _ _ B) A) + (at level 60, right associativity) : pseudo_notations. + + Notation "A :<<: B" := (PShift _ Shl (indexize _ _ B) A) + (at level 60, right associativity) : pseudo_notations. + + Notation "A :**: B" := (PDual _ Mult (PComb _ _ _ A B)) + (at level 55, right associativity) : pseudo_notations. + + Notation "'IF' O ( A , B ) 'THEN' L 'ELSE' R" := + (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R) + (at level 70, left associativity) : pseudo_notations. + + Notation "'EXP' ( e ) ( F )" := + (PFunExp _ F e) + (at level 70, left associativity) : pseudo_notations. + + Notation "'LET' E 'IN' F" := + (PLet _ _ _ E F) + (at level 70, left associativity) : pseudo_notations. + + Notation "A | B" := + (PComb _ _ _ A B) + (at level 65, left associativity) : pseudo_notations. + + Notation "'CALL' n ::: A" := + (PCall _ _ n A) + (at level 65, left associativity) : pseudo_notations. + + Definition p0: Pseudo 1 2. + refine (CALL 0 ::: %0 :**: $0); intuition. + Defined. End Notations. (* world peace *) diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v index 055c6d1bf..a2ec6fe40 100644 --- a/src/Assembly/PseudoMedialConversion.v +++ b/src/Assembly/PseudoMedialConversion.v @@ -1,24 +1,22 @@ Require Export Language Conversion QhasmEvalCommon QhasmUtil. -Require Export Pseudo Medial AlmostQhasm State. +Require Export Pseudo AlmostQhasm State. Require Export Bedrock.Word NArith NPeano Euclid. -Require Export List Sumbool. -Require Import FMapAVL FMapList JMeq. -Require Import Vector. +Require Export List Sumbool Vector. -Module PseudoMedialConversion (Arch: PseudoMachine). +Module PseudoConversion (Arch: PseudoMachine). Import QhasmCommon AlmostQhasm EvalUtil Util. Import ListNotations. Module P := Pseudo Arch. - Module M := Medial Arch. + (* Module M := Medial Arch. *) (****************** Material Conversions ************************) - Module PseudoConversion <: Conversion P M. - Import P M Arch StateCommon. + Module PseudoConversion <: Conversion P AlmostQhasm. + Import P (* M *) Arch StateCommon. - Fixpoint convertState (st: M.State): option P.State := + (* Fixpoint convertState (st: M.State): option P.State := let try_cons := fun {T} (x: option T) (l: list T) => match x with | Some x' => x' :: l | _ => l end in @@ -31,7 +29,7 @@ Module PseudoMedialConversion (Arch: PseudoMachine). if (Nat.eq_dec (length varList) vars) then Some (varList, m, c) else None - end. + end. *) Fixpoint range (start len: nat): list nat := match len with @@ -58,6 +56,93 @@ Module PseudoMedialConversion (Arch: PseudoMachine). | [] => O end. + Definition MMap := NatM.t (Mapping width). + Definition mempty := NatM.empty (Mapping width). + + Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat) (M: MMap): + option (AlmostProgram * (list (Mapping width)) * MMap) := + let rM := fun (x: nat) => regM _ (reg width_spec x) in + let sM := fun (x: nat) => stackM _ (stack width_spec x) in + + let g := fun (k: nat) => + match (NatM.find k M) with + | Some v => v + | _ => rM k (* TODO: more intelligent defaults *) + end in + + let madd := fun (k: nat) (f: nat -> Mapping width) => NatM.add k (f k) M in + + match prog with + | PVar n (Some true) i => Some (ASkip, [rM i], madd i rM) + | PVar n (Some false) i => Some (ASkip, [sM i], madd i sM) + | PVar n None i => Some (ASkip, [g i], M) + | PConst n c => Some (AAssign (AConstInt (rM start) c), [rM start], madd start rM) + | PMem n m v i => Some (AAssign (ARegMem (rM start) v i), madd start rM) + | _ => None + end. + + + | PBin n o p => + match (convertProgram' p start) with + | Some (p', [a; b]) => + Some (MSeq p' (MOp (MIOpReg o a b)), [a]) + | _ => None + end + + | PCarry n o p => + match (convertProgram' p start) with + | Some (p', [a; b]) => + Some (MSeq p' (MOp (MCOpReg o a b)), [a]) + | _ => None + end + + | PDual n o p => + match (convertProgram' p start) with + | Some (p', [a; b]) => + let nextOpen := S (maxN [a; b]) in + Some (MSeq p' (MOp (MDOpReg o a b (Some nextOpen))), [a; nextOpen]) + | _ => None + end + + | PShift n o a x => + match (convertProgram' x start) with + | Some (p', [r]) => + Some (MSeq p' (MOp (MOpRot o r a)), [proj1_sig a]) + | _ => None + end + + | PLet n k m f g => + ft <- convertProgram' f (start + k); + gt <- convertProgram' g (S (maxN (snd ft))); + + match (ft, gt) with + | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, gr) + end + + | PComb n a b f g => + ft <- convertProgram' f start; + gt <- convertProgram' g (S (maxN (snd ft))); + match (ft, gt) with + | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, fr ++ gr) + end + + | PIf n m o i0 i1 l r => + lt <- convertProgram' l start; + rt <- convertProgram' r start; + match (lt, rt) with + | ((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 *) + + | PFunExp n f e => + match (convertProgram' f start) with + | Some (fp, fr) => Some (MFunexp e fp, fr) + | _ => None + end + + | PCall n m lbl _ => Some (MCall lbl, range n m) + end. + (* Results are in the locations described by the returned list. start is the next known open address *) Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat): -- cgit v1.2.3