1%if false 2 Copyright (c) 2009, ETH Zurich. 3 All rights reserved. 4 5 This file is distributed under the terms in the attached LICENSE file. 6 If you do not find this file, copies can be found by writing to: 7 ETH Zurich D-INFK, Haldeneggsteig 4, CH-8092 Zurich. Attn: Systems Group. 8%endif 9 10%include polycode.fmt 11 12%if false 13 14> module Eval where 15 16> import Data.Bits as B 17 18> import PureExpressions 19 20%endif 21 22\section{Functional core interpreter} 23\label{sec:semantics_core} 24 25 26In this Section, we implement an expression evaluator. Given 27any (correct) expression, it will compute the corresponding value. The 28implementation is decomposed in several steps. In Section 29\ref{sec:sub:eval_top}, we evaluate top-level expressions. Doing so, 30we rely on case-specific evaluators. This includes unary operators 31(Section \ref{sec:sub:eval_unary}), binary operators (Section 32\ref{sec:sub:eval_binary}), the sizeof operation (Section 33\ref{sec:sub:eval_sizeof}), the conditional operation (Section 34\ref{sec:sub:eval_test}), and the cast operation (Section 35\ref{sec:sub:eval_cast}). 36 37Note that the following functions are \emph{partial}: not all 38expressions can be successfully evaluated. Indeed, some operations are 39simply meaningless. For example, computing the sum of a structure and 40a float is illegal. Currently, we are simply ignore these errors and this might 41result in run-time errors of the DSL compiler. Satisfactory solutions of 42this problem exist, though. For example, we could implement a 43type-checker that would ensure the absence of run-time errors. Another 44approach would be improve our error handling code. 45 46 47\subsubsection{Top-level Evaluation} 48\label{sec:sub:eval_top} 49 50The purpose of this section is implement the following function: 51 52> symbEval :: PureExpr -> PureExpr 53 54That reduces a given expression to a value. Hence, for values, this is 55trivial: 56 57> symbEval Void = Void 58> symbEval x@(CLInteger _ _ _) = x 59> symbEval x@(CLFloat _) = x 60> symbEval x@(CLRef _ _ _) = x 61 62Then, for inductive constructions, we rely on the specific functions 63implemented in the following sections. 64 65> symbEval (Unary op x) = 66> symbEvalUnary op x' 67> where x' = symbEval x 68> 69> symbEval (Binary op x y) = 70> symbEvalBinary op x' y' 71> where x' = symbEval x 72> y' = symbEval y 73> 74> symbEval (Sizeof typ) = symbEvalSizeof typ 75> 76> symbEval (Test x y z) = 77> symbEvalTest x' y z 78> where x' = symbEval x 79> 80> symbEval (Cast t x) = 81> symbEvalCast t x' 82> where x' = symbEval x 83 84 85\subsubsection{Unary Operator Evaluation} 86\label{sec:sub:eval_unary} 87 88For unary operators, we need to implement the following function: 89 90> symbEvalUnary :: UnaryOp -> PureExpr -> PureExpr 91 92Hence the following code: 93 94> symbEvalUnary Minus x = 95> case x of 96> CLInteger Signed size x -> CLInteger Signed size (-x) 97> CLFloat x -> CLFloat (-x) 98> _ -> error "symbEvalUnary: minus on wrong type" 99> 100> symbEvalUnary Complement x = 101> case x of 102> CLInteger sg sz x -> CLInteger sg sz (complement x) 103> _ -> error "symbEvalUnary: complement on wrong type" 104> 105> symbEvalUnary Negation x = 106> case x of 107> CLInteger sg sz 0 -> CLInteger sg sz 1 108> CLInteger sg sz _ -> CLInteger sg sz 0 109> _ -> error "symbEvalUnary: negation on wrong type" 110 111 112\subsubsection{Binary Operator Evaluation} 113\label{sec:sub:eval_binary} 114 115For binary operators, here is our goal: 116 117> symbEvalBinary :: BinaryOp -> PureExpr -> PureExpr -> PureExpr 118 119Achieved by the following, messy codes. 120 121\paragraph{Arithmetic Operations\\} 122 123> symbEvalBinary Plus (CLInteger sg si x) (CLInteger sg' si' y) 124> | sg == sg' && si == si' = CLInteger sg si (x + y) 125> | otherwise = error "symbEvalBinary: Plus undefined" 126> symbEvalBinary Plus (CLInteger _ _ x) (CLFloat y) = 127> CLFloat ( (fromRational $ toRational x) + y ) 128> symbEvalBinary Plus (CLFloat x) (CLInteger _ _ y) = 129> CLFloat ( x + (fromRational $ toRational y) ) 130> symbEvalBinary Plus (CLFloat x) (CLFloat y) = CLFloat ( x + y) 131> symbEvalBinary Plus _ _ = error "symbEvalBinary: Plus undefined" 132 133More checks should be added here. For examples, we should ensure that 134the result of the subtraction of two unsigned numbers is still 135positive, or make it wrap. 136 137> symbEvalBinary Sub (CLInteger sg si x) (CLInteger sg' si' y) 138> | sg == sg' && si == si' = CLInteger sg si (x - y) 139> | otherwise = error "symbEvalBinary: Sub undefined" 140> symbEvalBinary Sub (CLInteger _ _ x) (CLFloat y) = 141> CLFloat ( (fromRational $ toRational x) - y ) 142> symbEvalBinary Sub (CLFloat x) (CLInteger _ _ y) = 143> CLFloat ( x - (fromRational $ toRational y) ) 144> symbEvalBinary Sub (CLFloat x) (CLFloat y) = CLFloat ( x - y) 145> symbEvalBinary Sub _ _ = error "symbEvalBinary: Sub undefined" 146> 147> symbEvalBinary Mul (CLInteger sg si x) (CLInteger sg' si' y) 148> | sg == sg' && si == si' = CLInteger sg si (x * y) 149> | otherwise = error "symbEvalBinary: Mul undefined" 150> symbEvalBinary Mul (CLInteger _ _ x) (CLFloat y) = 151> CLFloat ( (fromRational $ toRational x) * y ) 152> symbEvalBinary Mul (CLFloat x) (CLInteger _ _ y) = 153> CLFloat ( x * (fromRational $ toRational y) ) 154> symbEvalBinary Mul (CLFloat x) (CLFloat y) = CLFloat ( x * y ) 155> symbEvalBinary Mul _ _ = error "symbEvalBinary: Mul undefined" 156> 157> symbEvalBinary Div (CLInteger sg si x) (CLInteger sg' si' y) 158> | sg == sg' && si == si' = CLInteger sg si (x `div` y) 159> | otherwise = error "symbEvalBinary: Div undefined" 160> symbEvalBinary Div (CLInteger _ _ x) (CLFloat y) = 161> CLFloat ( (fromRational $ toRational x) / y ) 162> symbEvalBinary Div (CLFloat x) (CLInteger _ _ y) = 163> CLFloat ( x / (fromRational $ toRational y) ) 164> symbEvalBinary Div (CLFloat x) (CLFloat y) = CLFloat (x / y) 165> symbEvalBinary Div _ _ = error "symbEvalBinary: Div undefined" 166> 167> symbEvalBinary Mod (CLInteger sg si x) (CLInteger sg' si' y) 168> | sg == sg' && si == si' = CLInteger sg si (x `mod` y) 169> | otherwise = error "symbEvalBinary: Mod undefined" 170> symbEvalBinary Mod _ _ = error "symbEvalBinary: Mod undefined" 171 172 173\paragraph{Boolean Operations\\} 174 175 176> symbEvalBinary Shl (CLInteger sg si x) (CLInteger sg' si' y) 177> | sg == sg' && si == si' = CLInteger sg si (shiftL x (fromInteger y)) 178> | otherwise = error "symbEvalBinary: Shl undefined" 179> symbEvalBinary Shl _ _ = error "symbEvalBinary: Shl undefined" 180> 181> symbEvalBinary Shr (CLInteger sg si x) (CLInteger sg' si' y) 182> | sg == sg' && si == si' = CLInteger sg si (shiftR x (fromInteger y)) 183> | otherwise = error "symbEvalBinary: Shr undefined" 184> symbEvalBinary Shr _ _ = error "symbEvalBinary: Shr undefined" 185> 186> symbEvalBinary AndBit (CLInteger sg si x) (CLInteger sg' si' y) 187> | sg == sg' && si == si' = CLInteger sg si (x B..|. y) 188> | otherwise = error "symbEvalBinary: And undefined" 189> symbEvalBinary AndBit _ _ = error "symbEvalBinary: And undefined" 190> 191> symbEvalBinary OrBit (CLInteger sg si x) (CLInteger sg' si' y) 192> | sg == sg' && si == si' = CLInteger sg si (x B..&. y) 193> | otherwise = error "symbEvalBinary: Or undefined" 194> symbEvalBinary OrBit _ _ = error "symbEvalBinary: Or undefined" 195> 196> symbEvalBinary XorBit (CLInteger sg si x) (CLInteger sg' si' y) 197> | sg == sg' && si == si' = CLInteger sg si (x `xor` y) 198> | otherwise = error "symbEvalBinary: Xor undefined" 199> symbEvalBinary XorBit _ _ = error "symbEvalBinary: Xor undefined" 200 201 202\paragraph{Comparison Operations\\} 203 204 205> symbEvalBinary op (CLInteger sg si x) (CLInteger sg' si' y) 206> | sg == sg' && si == si' = symbEvalComp op x y 207> | otherwise = error ("symbEvalBinary: " ++ show op ++ " undefined") 208> symbEvalBinary op (CLInteger _ _ x) (CLFloat y) = 209> symbEvalComp op (fromRational $ toRational x) y 210> symbEvalBinary op (CLFloat x) (CLInteger _ _ y) = 211> symbEvalComp op x (fromRational $ toRational y) 212> symbEvalBinary op (CLFloat x) (CLFloat y) = symbEvalComp op x y 213 214> symbEvalBinary Le _ _ = error "symbEvalBinary: Le undefined" 215> symbEvalBinary Leq _ _ = error "symbEvalBinary: Leq undefined" 216> symbEvalBinary Ge _ _ = error "symbEvalBinary: Leq undefined" 217> symbEvalBinary Geq _ _ = error "symbEvalBinary: Leq undefined" 218> symbEvalBinary Eq _ _ = error "symbEvalBinary: Leq undefined" 219> symbEvalBinary Neq _ _ = error "symbEvalBinary: Leq undefined" 220 221> symbEvalComp :: (Ord a, Num a) => BinaryOp -> a -> a -> PureExpr 222> symbEvalComp op x y = 223> let cmp = case op of 224> Le -> (<) 225> Leq -> (<=) 226> Ge -> (>) 227> Geq -> (>=) 228> Eq -> (==) 229> Neq -> (/=) in 230> if cmp x y then 231> CLInteger Unsigned TInt64 1 232> else CLInteger Unsigned TInt64 0 233 234\subsubsection{Sizeof Evaluation} 235\label{sec:sub:eval_sizeof} 236 237Our |sizeof| operator follows the corresponding C operation: 238 239> symbEvalSizeof :: TypeExpr -> PureExpr 240> symbEvalSizeof TVoid = CLInteger Unsigned TInt64 1 241> symbEvalSizeof (TInt _ TInt8) = CLInteger Unsigned TInt64 1 242> symbEvalSizeof (TInt _ TInt16) = CLInteger Unsigned TInt64 2 243> symbEvalSizeof (TInt _ TInt32) = CLInteger Unsigned TInt64 4 244> symbEvalSizeof (TInt _ TInt64) = CLInteger Unsigned TInt64 8 245> symbEvalSizeof TFloat = CLInteger Unsigned TInt64 4 246> symbEvalSizeof (TPointer _ _) = CLInteger Unsigned TInt64 8 247> symbEvalSizeof (TCompPointer _) = CLInteger Unsigned TInt64 8 248> symbEvalSizeof (TArray _ typ) = CLInteger Unsigned TInt64 8 249> symbEvalSizeof (TStruct _ _ fields) = CLInteger Unsigned TInt64 8 250> symbEvalSizeof (TUnion _ _ fields) = CLInteger Unsigned TInt64 8 251 252%if false 253 254 symbEvalSizeof (TFunction _ _ _) = CLInteger Unsigned TInt64 1 255 256%endif 257 258 259\subsubsection{Conditionals Evaluation} 260\label{sec:sub:eval_test} 261 262The semantics of the conditional mimics a restricted version of the C 263standard: True corresponds to everything which is not a float or 264integer equal to zero. Hence, we evaluate the corresponding branch 265accordingly. 266 267> symbEvalTest :: PureExpr -> PureExpr -> PureExpr -> PureExpr 268> symbEvalTest (CLInteger _ _ 0) _ y = symbEval y 269> symbEvalTest (CLFloat 0) _ y = symbEval y 270> symbEvalTest _ x _ = symbEval x 271 272 273\subsubsection{Cast Evaluation} 274\label{sec:sub:eval_cast} 275 276Here is our stripped-down version of |cast|. It will probably deserve 277some work in the future, as it is quite restrictive. Also, it should 278ensure that the type modification are reflected on the data: 279converting a signed, negative number to an unsigned form changes the 280value of this number. This is currently unsupported. 281 282> symbEvalCast :: TypeExpr -> PureExpr -> PureExpr 283> symbEvalCast (TInt sg sz) (CLInteger sg' sz' x) 284> | sg' < sg && sz' < sz = CLInteger sg sz x 285> | otherwise = error "symbEvalCast: illegal integer cast" 286> symbEvalCast TFloat (CLInteger _ _ x) = 287> CLFloat (fromRational $ toRational x) 288> symbEvalCast TFloat vx@(CLFloat x) = vx 289> symbEvalCast _ _ = 290> error "symbEvalCast: Not yet implemented/undefined cast" 291