{- CAO Compiler
Copyright (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see . -}
{-# LANGUAGE ViewPatterns #-}
{- |
Module : $Header$
Description : Expression evaluation.
Copyright : (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
License : GPL
Maintainer : Paulo Silva
Stability : experimental
Portability : non-portable
Frequently, source code may contain expressions using constant literals that
are not in their most evaluated format. For example, in cryptographic
implementations one often uses container sizes that are the explicit product
of two constants, to improve the clarity of the code. The expansion phase also
introduces literals in expressions by replacing the sequence indices by their
corresponding values. All these expression using literals are amenable to be
partially evaluated during compilation, thus resulting in simpler and more
efficient final code.
In this phase, several reductions are performed on expressions containing
literals accordingly with the rules defined in the operational semantics. In
many cases, these are quite identical to those defined in the language
interpreter. The main difference is that the interpreter needs all the values
fully defined while the evaluator can handle a mixture of defined and undefined
(variables) values. The evaluation does not give guarantees of completeness:
there may be some expressions that could be more reduced using more
sophisticated approaches. However all the reductions have been designed to be
safe and preserve the semantics of the program.
The following reductions on expressions are performed during this phase:
* Whenever possible, arithmetic expressions on literals are computed. This
resorts to some extent to commutativity, associativity and distributivity of
certain operators.
* Whenever possible, boolean expressions on literals are computed.
* Casts of literals are evaluated by converting their value to the target type,
accordingly with the semantics.
* Every nested range access is replaced by an equivalent non-nested range
access. This evaluation is always safe since the type checker already validated
the dimensions of the resulting ranges.
For vectors, the following rules are used, where @v@ is a vector and @l@,
@h@ and @n@ are integer literals:
@
v[l..h][n] → v[l + n]
v[l1..h1][l2..h2] → v[l1 + l2..l1 + h2]
@
For matrices, the rules are analogous using a second dimension.
After the evaluation of expressions, when the condition of a conditional or
iterative statement is a literal, the decision can be statically performed
without changing the meaning of the original program. Therefore, some
statements are also reduced:
* The corresponding branch of an if statement is chosen if its condition is
a literal.
* A while statement is removed if its condition is the false literal.
-}
module Language.CAO.Transformation.Eval ( evalExpr) where
import Language.CAO.Common.Literal
import Language.CAO.Common.SrcLoc
import Language.CAO.Common.Utils
import Language.CAO.Common.Var ( Var )
import Language.CAO.Common.Outputable
import Language.CAO.Semantics.Bool
import Language.CAO.Semantics.Casts
import Language.CAO.Semantics.Integer
import Language.CAO.Syntax
import Language.CAO.Syntax.Utils (isIntLit, isRange, typeOf)
import Language.CAO.Type
-- Consider the fusion with function checkIntExp of CaoTypeChecker
-- A more elaborated version could perform more distributivity laws
-- Can this step be fused with the remaining simplification?
evalExpr :: Prog Var -> Prog Var
evalExpr (Prog defs _) = Prog (map (fmap evalDef) defs) Nothing
evalDef :: Def Var -> Def Var
evalDef (VarDef vd) = VarDef $ evalVD vd
evalDef (FunDef fd) = FunDef $ evalFD fd
evalDef (TyDef td) = TyDef $ evalTDF td
evalDef (ConstDef cd) = ConstDef $ evalCD cd
evalVD :: VarDecl Var -> VarDecl Var
evalVD (VarD n td (Just e)) = VarD n td (Just $ evalLE e)
evalVD (ContD ln td es) = ContD ln td $ map evalLE es
evalVD vd = vd
-- Casts are not allowed inside constant initialization, and the type
-- annotation is never needed. Thus, it is safe to be undefined
evalCD :: ConstDecl Var -> ConstDecl Var
evalCD (ConstD c td (ConstInit e)) = ConstD c td (ConstInit (evalL undefined e))
evalCD cd = cd
evalFD :: Fun Var -> Fun Var
evalFD (Fun n args rt stmts)
= Fun n (map aux args)
(map evalTD rt)
(concatMap evalLStmt stmts)
where
aux (Arg a td) = Arg a (evalTD td)
aux (ArgConst a td e) = ArgConst a (evalTD td) e
evalTDF :: TyDef Var -> TyDef Var
evalTDF (TySynDef n td) = TySynDef n $ evalTD td
evalTDF (StructDecl n flds) = StructDecl n $ map (mapSnd evalTD) flds
evalLTD :: LTyDecl Var -> LTyDecl Var
evalLTD = fmap evalTD
evalTD :: TyDecl Var -> TyDecl Var
evalTD (BitsD s e) = BitsD s (evalL RInt e)
evalTD (ModD m) = ModD $ evalMod m
evalTD (VectorD e td) = VectorD (evalL RInt e) (evalTD td)
evalTD (MatrixD e1 e2 td) = MatrixD (evalL RInt e1) (evalL RInt e2) (evalTD td)
evalTD td = td
evalMod :: Mod Var -> Mod Var
evalMod (ModNum e) = ModNum $ evalL Int e
evalMod (ModPol td n p) = ModPol (evalTD td) n p
evalStmt :: Stmt Var -> [Stmt Var]
evalStmt (CDecl cd) = [CDecl $ evalCD cd]
evalStmt (VDecl vd) = [VDecl $ evalVD vd]
evalStmt (Assign lvs es) = [Assign (map evalLV lvs) (map evalLE es)]
evalStmt (FCallS n es) = [FCallS n $ map evalLE es]
evalStmt (Ret es) = [Ret $ map evalLE es]
evalStmt (Ite i t me) = let
i' = evalLE i
t' = concatMap evalLStmt t
me' = fmap (concatMap evalLStmt) me
in case unTyp $ unLoc i' of
Lit (BLit True) -> map unLoc t'
Lit (BLit False) -> maybe [] (map unLoc) me'
_ -> [Ite i' t' me']
evalStmt (Seq (SeqIter v s e b r) ss)
= [Seq (SeqIter v (evalL RInt s)
(evalL RInt e)
(fmap (evalL RInt) b)
r) $ concatMap evalLStmt ss]
evalStmt (While e ss) = let
e' = evalLE e
in case unTyp $ unLoc e' of
Lit (BLit False) -> []
_ -> [While e' (concatMap evalLStmt ss)]
evalStmt s@(Nop _) = [s]
evalLStmt :: LStmt Var -> [LStmt Var]
evalLStmt (L l s) = map (L l) $ evalStmt s
evalL :: Type Var -> LExpr Var -> LExpr Var
evalL t = fmap evalE . annL t
evalLE :: TLExpr Var -> TLExpr Var
evalLE (L loc e@(TyE tyann _)) = L loc $ TyE tyann $ evalE e
-- Type annotations are necessary to eval casts
evalE :: TExpr Var -> Expr Var
evalE (TyE _ v@(Var _)) = v
evalE (TyE _ l@(Lit _)) = l
evalE (TyE _ (FunCall n es)) = FunCall n $ map evalLE es
evalE (TyE _ (StructProj e f)) = StructProj (evalLE e) f
evalE (TyE _ (UnaryOp Sym e)) = reduceIntExpr $ UnaryOp Sym $ evalLE e
evalE (TyE _ (UnaryOp Not e)) = reduceBoolExpr $ UnaryOp Not $ evalLE e
evalE (TyE _ (UnaryOp BNot bs)) = UnaryOp BNot $ evalLE bs
evalE (TyE _ (BinaryOp (ArithOp o) l r)) = reduceIntExpr $
BinaryOp (ArithOp o) (evalLE l) (evalLE r)
evalE (TyE _ (BinaryOp (BoolOp o) l r)) = reduceBoolExpr $
BinaryOp (BoolOp o) (evalLE l) (evalLE r)
evalE (TyE _ (BinaryOp op e1 e2)) = BinaryOp op (evalLE e1) (evalLE e2)
evalE (TyE _ (Access e p)) = reduceRanges $ Access (evalLE e) (evalP p)
evalE (TyE t (Cast b td e)) =
case evalLE e of
-- Needed to evaluate nested casts of literals
L _ l@(TyE _ (Lit _)) -> convertTo t l
e' -> Cast b (map evalLTD td) e'
evalP :: APat Var -> APat Var
evalP (VectP p) = VectP $ evalAP p
evalP (MatP l r) = MatP (evalAP l) (evalAP r)
evalAP :: RowAPat Var -> RowAPat Var
evalAP (CElem e) = CElem $ evalLE e
evalAP (CRange l r) = CRange (evalLE l) (evalLE r)
evalLV :: LVal Var -> LVal Var
evalLV (LVStruct lv fi) = LVStruct (evalLV lv) fi
evalLV (LVCont ty lv p)
= case reduceLRanges (LVCont ty (evalLV lv) (evalP p)) of
LVCont ty' lv' p' -> LVCont ty' (evalLV lv') (evalP p')
_ -> error ".\
\: Unexpected error in 'reduceLRanges'"
evalLV v@(LVVar _) = v
--------------------------------------------------------------------------------
getTLInt :: TLExpr Var -> Either (Integer, SrcLoc, Type Var) (TLExpr Var)
getTLInt (L l (TyE t (Lit (ILit i)))) = Left (i, l, t)
getTLInt e = Right e
getTInt :: TLExpr Var -> Either (Integer, Type Var) (TLExpr Var)
getTInt (unLoc -> TyE t (Lit (ILit i))) = Left (i, t)
getTInt e = Right e
reduceAssoc :: AOp -> (Integer -> Integer) -> TLExpr Var -> TLExpr Var -> Expr Var
reduceAssoc op i (getTInt -> Left (j, _)) (getTInt -> Left (k, _))
= Lit $ ILit $ i $ fInt op j k
reduceAssoc op i (getTLInt -> Left (j,l, t)) (getTInt -> Right k)
= BinaryOp (ArithOp op) (L l $ annTyE t $ Lit $ ILit $ i j) k
reduceAssoc op i (getTInt -> Right j) (getTLInt -> Left (k,l,t))
= BinaryOp (ArithOp op) j (L l $ annTyE t $ Lit $ ILit $ i k)
reduceAssoc _ _ _ _
= error ".: Unexpected case"
reduceTimesPlus :: Integer -> TLExpr Var -> TLExpr Var -> Expr Var
reduceTimesPlus i (getTInt -> Left (j, _)) (getTInt -> Left (k, _)) =
Lit $ ILit $ i * (j + k)
reduceTimesPlus i (getTLInt -> Left (j, l, t)) (getTInt -> Right k) =
BinaryOp (ArithOp Plus)
(L l $ annTyE t $ Lit $ ILit $ j `integerTimes` i)
(L (getLoc k) $ annTyE t $
BinaryOp (ArithOp Times) (genLoc $ annTyE t $ Lit $ ILit i) k)
reduceTimesPlus i (getTInt -> Right j) (getTLInt -> Left (k, l, t)) =
BinaryOp (ArithOp Plus)
(L (getLoc j) $ annTyE t $
BinaryOp (ArithOp Times) (genLoc $ annTyE t $ Lit $ ILit i) j)
(L l $ annTyE t $ Lit $ ILit $ k `integerTimes` i)
reduceTimesPlus i (getTInt -> Right j) (getTInt -> Right k) =
BinaryOp (ArithOp Plus)
(L (getLoc j) $ annTyE tj $ BinaryOp (ArithOp Times) ei j)
(L (getLoc k) $ annTyE (typeOf k) $ BinaryOp (ArithOp Times) ei k)
where
tj = typeOf j
ei = genLoc $ annTyE tj $ Lit $ ILit i
reduceTimesPlus e1 e2 e3 =
error $ ".:\
\ Unexpected case: (" ++ showPpr e1 ++ ") * ((" ++ showPpr e2
++ ") + (" ++ showPpr e3 ++ "))"
reduceIntExpr :: Expr Var -> Expr Var
-- Simple exprs
reduceIntExpr (BinaryOp (ArithOp (fInt -> op))
(getTInt -> Left (b1, _))
(getTInt -> Left (b2, _)))
= Lit $ ILit $ b1 `op` b2
reduceIntExpr (UnaryOp Sym (getTInt -> Left (b1, _)))
= Lit $ ILit $ negate b1
-- Distributivity of '*'
reduceIntExpr (BinaryOp (ArithOp Times)
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Plus) e1 e2))
(getTInt -> Left (e3, _)))
= reduceTimesPlus e3 e1 e2
reduceIntExpr (BinaryOp (ArithOp Times)
(getTInt -> Left (e3, _))
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Plus) e1 e2)))
= reduceTimesPlus e3 e1 e2
-- Associativity
reduceIntExpr (BinaryOp (ArithOp oop)
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp iop) e1 e2))
(getTInt -> Left (e3, _)))
| isAssoc oop && oop == iop && (isIntLit (unTyp (unLoc e1)) || isIntLit (unTyp (unLoc e2)))
= reduceAssoc oop (flip (fInt oop) e3) e1 e2
reduceIntExpr (BinaryOp (ArithOp oop)
(getTInt -> Left (e3, _))
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp iop) e1 e2)))
| isAssoc oop && oop == iop && (isIntLit (unTyp (unLoc e1)) || isIntLit (unTyp (unLoc e2)))
= reduceAssoc oop (fInt oop e3) e1 e2
-- Minus Case
--
--
-- reduceAssoc takes advantage also from commutativity, so
-- isAssoc now is True only for associative and commutative ops)
reduceIntExpr
(BinaryOp (ArithOp Minus)
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
(getTInt -> Left (e1, _))
(getTInt -> Left (e2, _))))
(getTInt -> Left (e3, _)))
= Lit $ ILit (e1 - e2 - e3)
reduceIntExpr
(BinaryOp (ArithOp Minus)
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
(getTInt -> Right e1)
(getTLInt -> Left (e2, l, _))))
(getTInt -> Left (e3, t)))
= BinaryOp (ArithOp Minus) e1 (L l $ annTyE t $ Lit $ ILit (e2 - e3))
reduceIntExpr
(BinaryOp (ArithOp Minus)
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
(getTLInt -> Left (e1, l, _))
(getTInt -> Right e2)))
(getTInt -> Left (e3, t)))
= BinaryOp (ArithOp Minus) (L l $ annTyE t $ Lit $ ILit (e1 - e3)) e2
reduceIntExpr
(BinaryOp (ArithOp Minus)
(getTInt -> Left (e3, t))
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
(getTInt -> Right e1)
(getTLInt -> Left (e2, l, _)))))
= BinaryOp (ArithOp Minus) (L l $ annTyE t $ Lit $ ILit (e2 + e3)) e1
reduceIntExpr
(BinaryOp (ArithOp Minus)
(getTInt -> Left (e3, t))
(getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
(getTLInt -> Left (e1, l, _))
(getTInt -> Right e2))))
= BinaryOp (ArithOp Plus) (L l $ annTyE t $ Lit $ ILit (e3 - e1)) e2
--
reduceIntExpr e
= e
--------------------------------------------------------------------------------
getBool :: TLExpr Var -> Maybe Bool
getBool (unLoc -> unTyp -> Lit (BLit b)) = Just b
getBool _ = Nothing
reduceBoolExpr :: Expr Var -> Expr Var
reduceBoolExpr (BinaryOp (BoolOp (fBool -> op))
(getBool -> Just b1)
(getBool -> Just b2))
= Lit $ BLit $ b1 `op` b2
reduceBoolExpr (UnaryOp Not (getBool -> Just b1))
= Lit $ BLit $ boolNot b1
reduceBoolExpr e
= e
--------------------------------------------------------------------------------
reduceRanges :: Expr Var -> Expr Var
reduceRanges (Access (unLoc -> (TyE _ (Access e1 p1))) p2) | isRange p1
= Access e1 $ reducePats p1 p2
reduceRanges e
= e
-- | Reduce nested ranges in LValues
--
-- Examples:
-- m[1..5,2..3][3,1] ----->
-- m' = m[1..5,2..3] : matrix[5,2] of a'
-- m'[3,1] : a'
-- =====> reduces to m[4,3]
--
-- m[1..5,2..3][3 .. 4,1] ----->
-- m' = m[1..5,2..3] : matrix[5,2] of a'
-- m'[3 .. 4 ,1] : matrix [2, 1] of a'
-- reduces to m[4 .. 5, 3]
--
reduceLRanges :: LVal Var -> LVal Var
reduceLRanges (LVCont ty (LVCont _ lv' p1) p2) | isRange p1
= LVCont ty lv' (reducePats p1 p2)
reduceLRanges lv
= lv
reducePats :: APat Var -> APat Var -> APat Var
reducePats (VectP r1) (VectP r2)
= VectP $ reduceRngs r1 r2
reducePats (MatP r11 r12) (MatP r21 r22)
= MatP (reduceRngs r11 r21) (reduceRngs r12 r22)
reducePats _ _
= error $ ".\
\: Unexpected case."
reduceRngs :: RowAPat Var -> RowAPat Var -> RowAPat Var
reduceRngs (CRange e1 _) (CElem ei)
= CElem $ L (getLoc e1) $ annTyE RInt $ reduceIntExpr $
BinaryOp (ArithOp Plus) e1 ei
reduceRngs (CRange e1 _) (CRange el eh)
= CRange (L (getLoc e1) $ annTyE RInt $ reduceIntExpr $
BinaryOp (ArithOp Plus) e1 el)
(L (getLoc e1) $ annTyE RInt $ reduceIntExpr $
BinaryOp (ArithOp Plus) e1 eh)
reduceRngs _ _
= error $ ".\
\: Unexpected case."
--------------------------------------------------------------------------------
fInt :: AOp -> Integer -> Integer -> Integer
fInt Plus = integerPlus
fInt Minus = integerMinus
fInt Times = integerTimes
fInt Power = integerPower
fInt Div = integerDiv
fInt ModOp = integerMod
isAssoc :: AOp -> Bool
isAssoc Plus = True
isAssoc Times = True
isAssoc _ = False
fBool :: BOp -> Bool -> Bool -> Bool
fBool And = boolAnd
fBool Or = boolOr
fBool Xor = boolXor