allow ternary conditional + implement fPreNot, fPreBitCompl + better document LogicIR.Expr

src/LogicIR/Backend/Z3.hs

@@ -9,7 +9,7 @@ lExprToZ3Ast :: LExpr -> Z3 AST
 lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
 
 lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
-lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray) where
+lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray, fnIf) where
     flConst = undefined
     flVar = undefined
     flNot = undefined
@@ -21,4 +21,5 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
     fnVar = undefined
     fnUnop = undefined
     fnBinop = undefined
-    fnArray = undefined
\ No newline at end of file
+    fnArray = undefined
+    fnIf = undefined
\ No newline at end of file

src/LogicIR/Expr.hs

@@ -16,21 +16,21 @@ data Var = Var Type String
          deriving (Show, Eq, Read)
 
 -- Numeral unary operators
-data NUnop = NNeg
-           | NNot
+data NUnop = NNeg -- -n (negation)
+           | NNot -- ~n (binary not)
            deriving (Show, Eq, Read)
 
 -- Numeral binary operators
-data NBinop = NAdd
-            | NSub
-            | NMul
-            | NDiv
-            | NRem
-            | NShl
-            | NShr
-            | NAnd
-            | NOr
-            | NXor
+data NBinop = NAdd -- a + b
+            | NSub -- a - b
+            | NMul -- a * b
+            | NDiv -- a / b
+            | NRem -- a % b
+            | NShl -- a >> b
+            | NShr -- a << b
+            | NAnd -- a & b
+            | NOr -- a | b
+            | NXor -- a ^ b
             deriving (Show, Eq, Read)
 
 -- Reference: https://en.wikipedia.org/wiki/First-order_logic#Logical_symbols
@@ -71,4 +71,5 @@ data LExpr = LConst Bool -- True/False
            | NUnop NUnop NExpr -- Unary operator
            | NBinop NExpr NBinop NExpr -- Binary operators
            | NArray Var [NExpr] -- Integer array access
+           | NIf LExpr NExpr NExpr -- if c then a else b
            deriving (Show, Eq, Read)
\ No newline at end of file

src/LogicIR/Fold.hs

@@ -14,12 +14,13 @@ type LExprAlgebra r = (Bool -> r, -- LConst
                        Var -> r, -- NVar
                        NUnop -> r -> r, -- NUnop
                        r -> NBinop -> r -> r, -- NBinop
-                       Var -> [NExpr] -> r -- NArray
+                       Var -> [NExpr] -> r, -- NArray
+                       r -> r -> r -> r -- NIf
                       )
 
 -- Fold for logical expressions
 foldLExpr :: LExprAlgebra r -> LExpr -> r
-foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray) = fold where
+foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray, fnIf) = fold where
     fold e = case e of
                   LConst c -> flConst c
                   LVar n -> flVar n
@@ -32,4 +33,5 @@ foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fn
                   NVar n -> fnVar n
                   NUnop o e -> fnUnop o (fold e)
                   NBinop a o b -> fnBinop (fold a) o (fold b)
-                  NArray n e -> fnArray n e
\ No newline at end of file
+                  NArray n e -> fnArray n e
+                  NIf c a b -> fnIf (fold c) (fold a) (fold b)
\ No newline at end of file

src/LogicIR/Frontend/Java.hs

@@ -16,20 +16,21 @@ javaExpToLExpr = foldExp javaExpToLExprAlgebra
 
 javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> LExpr)
 javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualInstanceCreation, fArrayCreate, fArrayCreateInit, fFieldAccess, fMethodInv, fArrayAccess, fExpName, fPostIncrement, fPostDecrement, fPreIncrement, fPreDecrement, fPrePlus, fPreMinus, fPreBitCompl, fPreNot, fCast, fBinOp, fInstanceOf, fCond, fAssign, fLambda, fMethodRef) where
-    fLit lit _ _ = case lit of
+    fLit lit _ _ = case lit of -- TODO: support more type literals
                     Boolean b -> LConst b
                     Int n -> NConst (fromIntegral n) -- TODO: use Integer in LExpr?
+                    Null -> undefined -- TODO: null support
                     _ -> error $ show $ lit
-    fClassLit = undefined
-    fThis = undefined
-    fThisClass = undefined
-    fInstanceCreation = undefined
-    fQualInstanceCreation = undefined
+    fClassLit = error "fClassLit not supported..."
+    fThis = error "fThis not supported..."
+    fThisClass = error "fThisClass not supported..."
+    fInstanceCreation = error "fInstanceCreation not supported..."
+    fQualInstanceCreation = error "fQualInstanceCreation not supported..."
     fArrayCreate = undefined
     fArrayCreateInit = undefined
     fFieldAccess = undefined
     fMethodInv = undefined
-    fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: better type checking + multiple dimension arrays
+    fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: better type checking + multiple dimension arrays + better abstractions
                                              ArrayIndex (ExpName name) [ExpName index] ->
                                                 let (arrayType, indexType) = (lookupType decls env name, lookupType decls env index) in
                                                     case arrayType of
@@ -44,16 +45,16 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
                                         PrimType BooleanT    -> LVar (Var (TPrim PBool) symbol)
                                         PrimType IntT        -> NVar (Var (TPrim PInt) symbol)
                                         t                    -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
-    fPostIncrement = undefined
-    fPostDecrement = undefined
-    fPreIncrement = undefined
-    fPreDecrement = undefined
+    fPostIncrement = error "fPostIncrement has side effects..."
+    fPostDecrement = error "fPostDecrement has side effects..."
+    fPreIncrement = error "fPreIncrement has side effects..."
+    fPreDecrement = error "fPreDecrement has side effects..."
     fPrePlus e env decls = e env decls
     fPreMinus e env decls = NUnop NNeg (e env decls)
-    fPreBitCompl = undefined
-    fPreNot = undefined
-    fCast = undefined
-    fBinOp e1 op e2 env decls = let (a, b) = (e1 env decls, e2 env decls) in -- TODO: type checking
+    fPreBitCompl e env decls = NUnop NNot (e env decls)
+    fPreNot e env decls = LNot (e env decls)
+    fCast = undefined -- TODO: perhaps support cast for some types?
+    fBinOp e1 op e2 env decls = let (a, b) = (e1 env decls, e2 env decls) in -- TODO: type checking?
                                 case op of
                                      -- Integer
                                      Mult -> NBinop a NMul b
@@ -78,7 +79,7 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
                                      Equal -> LComp a CEqual b
                                      NotEq -> LComp a CNEqual b
     fInstanceOf = undefined
-    fCond = undefined
-    fAssign = undefined
-    fLambda = undefined
+    fCond c a b env decls = NIf (c env decls) (a env decls) (b env decls)
+    fAssign = error "fAssign has side effects..."
+    fLambda = undefined -- TODO: see if this should be ignored and handled in function call instead...
     fMethodRef = undefined
\ No newline at end of file