Merge pull request #14 from gridaphobe/index-type

Track index bounds in the types of Ivory procs

.gitignore

@@ -1 +1,2 @@
 cabal.sandbox.config
+/ivory-examples/test_dir/

ivory-backend-aadl/src/Ivory/Compile/AADL/Gen.hs

@@ -2,6 +2,7 @@
 
 module Ivory.Compile.AADL.Gen where
 
+import qualified Ivory.Language.Array  as I
 import qualified Ivory.Language.Syntax as I
 
 import qualified Data.Set as Set
@@ -32,6 +33,7 @@ mkType ty = case ty of
     I.TyChar              -> basetype "Char"
     I.TyInt i             -> intSize i
     I.TyWord w            -> wordSize w
+    I.TyIndex _           -> mkType I.ixRep
     I.TyBool              -> basetype "Boolean"
     I.TyFloat             -> basetype "Float"
     I.TyDouble            -> basetype "Double"

ivory-backend-c/src/Ivory/Compile/C/Gen.hs

@@ -9,6 +9,7 @@ module Ivory.Compile.C.Gen where
 import qualified "language-c-quote" Language.C.Syntax as C
 import Language.C.Quote.GCC
 
+import qualified Ivory.Language.Array  as I
 import qualified Ivory.Language.Syntax as I
 import qualified Ivory.Language.Proc as P
 
@@ -163,6 +164,7 @@ toTypeCxt arrCase = convert
     I.TyChar              -> [cty| char |]
     I.TyInt i             -> intSize i
     I.TyWord w            -> wordSize w
+    I.TyIndex _           -> toTypeCxt arrCase I.ixRep
     I.TyBool              -> [cty| typename bool |]
     I.TyFloat             -> [cty| float |]
     I.TyDouble            -> [cty| double |]
@@ -294,7 +296,7 @@ toBody ens stmt =
                               $exp:incExp ) {
                        $items:loopBd } |]]
       where
-      ty = I.TyInt I.Int32
+      ty = I.ixRep
       (test,incExp)  = toIncr incr
       ix = toVar var
       toIncr (I.IncrTo to) =
@@ -353,6 +355,7 @@ toExpr t (I.ExpLit lit)  =
       where fromInt = case t of
                         I.TyWord _  -> show i ++ "U"
                         I.TyInt  _  -> show i
+                        I.TyIndex _ -> show i
                         I.TyFloat   -> show (fromIntegral i :: Float) ++ "F"
                         I.TyDouble  -> show (fromIntegral i :: Double)
                         _           -> error ("Nonint type " ++ (show t) ++
@@ -415,6 +418,7 @@ toExpr ty (I.ExpMaxMin b) = [cexp| $id:macro |]
         I.Word16    -> "UINT16_MAX"
         I.Word32    -> "UINT32_MAX"
         I.Word64    -> "UINT64_MAX"
+      I.TyIndex n -> show n
       _           -> err
     False -> case ty of
       I.TyInt sz -> case sz of
@@ -427,6 +431,7 @@ toExpr ty (I.ExpMaxMin b) = [cexp| $id:macro |]
         I.Word16    -> 0
         I.Word32    -> 0
         I.Word64    -> 0
+      I.TyIndex _ -> "0"
       _           -> err
   err = error $ "unexpected type " ++ show ty ++ " in ExpMaxMin."
 ----------------------------------------

ivory-examples/examples/Makefile → ivory-examples/Makefile

@@ -3,11 +3,10 @@ MAIN="int main(void) { return 0; }"
 
 # Where to put all our generated files
 TESTDIR=test_dir
-IDIR=../runtime
+IDIR=runtime
 CFLAGS=-I$(IDIR) -O2
 
-EXECPATH=../../../cabal-dev/bin
-EXEC=ivory-c-clang-test
+EXEC=cabal run ivory-c-clang-test
 
 # Our tests
 TESTS=PID.out FibLoop.out FunPtr.out String.out Factorial.out \
@@ -21,9 +20,9 @@ all : clean $(TESTS)
 	clang -Wall -Wno-missing-braces $(CFLAGS) -lm -DIVORY_TEST -o $(TESTDIR)/$@ $<
 
 .PRECIOUS : $(TESTDIR)/%.c
-$(TESTDIR)/%.c : %.hs | $(TESTDIR)
+$(TESTDIR)/%.c : examples/%.hs | $(TESTDIR)
 	# Will generate all the files on the first run
-	$(EXECPATH)/$(EXEC) $(TESTDIR)
+	$(EXEC) $(TESTDIR)
 
 $(TESTDIR):
 	mkdir -p $@
@@ -42,3 +41,4 @@ cbmc2 :
 .PHONY : clean
 clean :
 	rm -rf $(TESTDIR)
+	cabal clean

ivory-opts/src/Ivory/Opts/AssertFold.hs

@@ -18,6 +18,7 @@ import           Control.Applicative
 import           Data.Monoid
 import qualified Data.DList as D
 import           Ivory.Opts.Utils
+import qualified Ivory.Language.Array        as I
 import qualified Ivory.Language.Syntax.AST   as I
 import qualified Ivory.Language.Syntax.Type  as I
 
@@ -130,7 +131,7 @@ stmtFold ef stmt = case stmt of
                                         insert stmt
   I.Call _ty _mv _nm args         -> do mapM_ efTyped args
                                         insert stmt
-  I.Loop v e incr blk             -> do ef (I.TyInt I.Int32) e
+  I.Loop v e incr blk             -> do ef (I.ixRep) e
                                         efIncr incr
                                         blk' <- runFreshStmts ef blk
                                         insert (I.Loop v e incr blk')
@@ -149,7 +150,7 @@ stmtFold ef stmt = case stmt of
   efIncr incr = case incr of
     I.IncrTo e -> ef ty e
     I.DecrTo e -> ef ty e
-    where ty = I.TyInt I.Int32
+    where ty = I.ixRep
   efInit init' = case init' of
     I.InitZero          -> return ()
     I.InitExpr ty e     -> ef ty e

ivory-opts/src/Ivory/Opts/CFG.hs

@@ -20,7 +20,8 @@ module Ivory.Opts.CFG
   )
     where
 
-import qualified Ivory.Language.Syntax.AST as I
+import qualified Ivory.Language.Array       as I
+import qualified Ivory.Language.Syntax.AST  as I
 import qualified Ivory.Language.Syntax.Type as I
 import qualified Data.Graph.Inductive as G
 
@@ -130,6 +131,7 @@ toStackType ty =
     I.TyVoid       -> TyVoid
     I.TyInt i      -> TyInt (toIntType i)
     I.TyWord w     -> TyWord (toWordType w)
+    I.TyIndex n    -> toStackType I.ixRep
     I.TyBool       -> TyBool
     I.TyChar       -> TyChar
     I.TyFloat      -> TyFloat
@@ -171,7 +173,7 @@ toAlloc stmt =
                                                     (concatMap toAlloc blk1) ]
                                            -- For the loop variable.
     I.Loop _ e _ blk                    ->
-      let ty = I.TyInt I.Int32 in
+      let ty = I.ixRep in
       [Stmt (toStackType ty), Loop (getIdx e) (concatMap toAlloc blk)]
     I.Forever blk                       ->
       [Loop Nothing (concatMap toAlloc blk)]

ivory-opts/src/Ivory/Opts/ConstFold.hs

@@ -14,6 +14,7 @@ module Ivory.Opts.ConstFold
 
 import Ivory.Opts.ConstFoldComp
 
+import qualified Ivory.Language.Array  as I
 import qualified Ivory.Language.Syntax as I
 import Ivory.Language.Cast (toMaxSize, toMinSize)
 
@@ -114,7 +115,7 @@ stmtFold cxt opt stmt =
     I.AllocRef{}         -> return $ D.singleton stmt
     I.Loop v e incr blk' -> do
       copies <- get
-      let ty = I.TyInt I.Int32
+      let ty = I.ixRep
       case opt copies ty e of
         I.ExpLit (I.LitBool b) ->
           if b then error $ "Constant folding evaluated True expression "
@@ -162,7 +163,7 @@ cf copies ty e =
             return e0'
 
     I.ExpToIx e0 maxSz    ->
-      let ty' = I.TyInt I.Int32 in
+      let ty' = I.ixRep in
       let e0' = cf copies ty' e0 in
       case destIntegerLit e0' of
         Just i  -> I.ExpLit $ I.LitInteger $ i `rem` maxSz

ivory-opts/src/Ivory/Opts/ConstFoldComp.hs

@@ -240,6 +240,7 @@ cfNum ty op args = case args of
         I.Word16      -> appI1 op1 (fromInteger l :: Word16)
         I.Word32      -> appI1 op1 (fromInteger l :: Word32)
         I.Word64      -> appI1 op1 (fromInteger l :: Word64)
+      I.TyIndex n  -> appI1 op1 (fromInteger l :: Int32)
       _ -> err $ "bad type to cfNum loc 1 "
     CfFloat   l -> CfFloat   (op1 l)
     CfDouble  l -> CfDouble  (op1 l)
@@ -265,6 +266,8 @@ cfNum ty op args = case args of
                                    (fromInteger r :: Word32)
         I.Word64      -> appI2 op2 (fromInteger l :: Word64)
                                    (fromInteger r :: Word64)
+      I.TyIndex n -> appI2 op2 (fromInteger l :: Int32)
+                               (fromInteger r :: Int32)
       _ -> err "bad type to cfNum loc 2"
     (CfFloat   l, CfFloat r)   -> CfFloat   (op2 l r)
     (CfDouble l,  CfDouble r)  -> CfDouble  (op2 l r)
@@ -305,6 +308,8 @@ cfIntOp2 ty iOp [CfInteger _ l, CfInteger _ r] = case ty of
                                (fromInteger r :: Word32)
     I.Word64      -> appI2 op2 (fromInteger l :: Word64)
                                (fromInteger r :: Word64)
+  I.TyIndex n  -> appI2 op2 (fromInteger l :: Int32)
+                            (fromInteger r :: Int32)
   _ -> err "bad type to cfIntOp2 loc 1"
 
   where

ivory-opts/src/Ivory/Opts/DivZero.hs

@@ -37,6 +37,7 @@ divAssert ty e0 = case e0 of
   zeroExp = case ty of
               I.TyInt  _ -> I.ExpLit (I.LitInteger 0)
               I.TyWord _ -> I.ExpLit (I.LitInteger 0)
+              I.TyIndex _-> I.ExpLit (I.LitInteger 0)
               I.TyFloat  -> I.ExpLit (I.LitFloat 0)
               I.TyDouble -> I.ExpLit (I.LitDouble 0)
               _          -> error $

ivory-opts/src/Ivory/Opts/Index.hs

@@ -10,7 +10,8 @@ module Ivory.Opts.Index
 import           Ivory.Opts.AssertFold
 import           Ivory.Opts.Utils
 
-import qualified Ivory.Language.Syntax.AST as I
+import qualified Ivory.Language.Array       as I
+import qualified Ivory.Language.Syntax.AST  as I
 import qualified Ivory.Language.Syntax.Type as I
 
 --------------------------------------------------------------------------------
@@ -33,7 +34,7 @@ expFold ty e = case e of
   I.ExpIndex tIdx eIdx tArr eArr -> do expFold tIdx eIdx
                                        expFold tArr eArr
   I.ExpToIx e0 maxSz             -> do insert (toIxAssert e0 maxSz)
-                                       expFold ixTy e0
+                                       expFold I.ixRep e0
   I.ExpSafeCast ty' e0           -> expFold ty' e0
   I.ExpOp op args                -> mapM_ (expFold $ expOpType ty op) args
   I.ExpAddrOfGlobal{}            -> return ()
@@ -47,18 +48,13 @@ expFold ty e = case e of
 -- @
 toIxAssert :: I.Expr -> Integer -> I.Stmt
 toIxAssert e maxSz = I.CompilerAssert $ I.ExpOp I.ExpAnd
-  [ I.ExpOp (I.ExpLt True ixTy)  [ lit 0, e ]
-  , I.ExpOp (I.ExpLt False ixTy) [ e, lit maxSz ]
-  , I.ExpOp (I.ExpLt False ixTy) [ lit 0, lit maxSz ]
+  [ I.ExpOp (I.ExpLt True I.ixRep)  [ lit 0, e ]
+  , I.ExpOp (I.ExpLt False I.ixRep) [ e, lit maxSz ]
+  , I.ExpOp (I.ExpLt False I.ixRep) [ lit 0, lit maxSz ]
   ]
 
 --------------------------------------------------------------------------------
 
-ixTy :: I.Type
-ixTy = I.TyInt I.Int32
-
---------------------------------------------------------------------------------
-
 lit :: Integer -> I.Expr
 lit i = I.ExpLit (I.LitInteger i)
 

ivory-opts/src/Ivory/Opts/Overflow.hs

@@ -12,6 +12,7 @@ module Ivory.Opts.Overflow
 
 import Ivory.Opts.AssertFold
 
+import qualified Ivory.Language.Array        as I
 import qualified Ivory.Language.Syntax.AST   as I
 import qualified Ivory.Language.Syntax.Type  as I
 import qualified Ivory.Language.Syntax.Names as I
@@ -50,6 +51,7 @@ litAssert ty lit = case lit of
       I.TyInt I.Int16   -> boundLit (minMax :: Bounds Int16)
       I.TyInt I.Int32   -> boundLit (minMax :: Bounds Int32)
       I.TyInt I.Int64   -> boundLit (minMax :: Bounds Int64)
+      I.TyIndex n       -> boundLit (0 :: Integer, n)
       _                 -> return ()
       where
       boundLit (min,max) = insert ca
@@ -76,6 +78,7 @@ arithAssert' ty op args =
       I.TyInt I.Int16   -> mkCall addBase ty args
       I.TyInt I.Int32   -> mkCall addBase ty args
       I.TyInt I.Int64   -> mkCall addBase ty args
+      I.TyIndex _       -> mkCall addBase ty args
       _                 -> return ()
 
     I.ExpSub -> case ty of
@@ -87,6 +90,7 @@ arithAssert' ty op args =
       I.TyInt I.Int16   -> mkCall subBase ty args
       I.TyInt I.Int32   -> mkCall subBase ty args
       I.TyInt I.Int64   -> mkCall subBase ty args
+      I.TyIndex _       -> mkCall subBase ty args
       _                 -> return ()
 
     I.ExpMul -> case ty of
@@ -98,6 +102,7 @@ arithAssert' ty op args =
       I.TyInt I.Int16   -> mkCall mulBase ty args
       I.TyInt I.Int32   -> mkCall mulBase ty args
       I.TyInt I.Int64   -> mkCall mulBase ty args
+      I.TyIndex _       -> mkCall mulBase ty args
       _                 -> return ()
 
     I.ExpDiv -> case ty of
@@ -109,6 +114,7 @@ arithAssert' ty op args =
       I.TyInt I.Int16   -> mkCall divBase ty args
       I.TyInt I.Int32   -> mkCall divBase ty args
       I.TyInt I.Int64   -> mkCall divBase ty args
+      I.TyIndex _       -> mkCall divBase ty args
       _                 -> return ()
 
     I.ExpMod -> case ty of
@@ -120,6 +126,7 @@ arithAssert' ty op args =
       I.TyInt I.Int16   -> mkCall divBase ty args
       I.TyInt I.Int32   -> mkCall divBase ty args
       I.TyInt I.Int64   -> mkCall divBase ty args
+      I.TyIndex _       -> mkCall divBase ty args
       _                 -> return ()
 
     _ -> return ()
@@ -172,4 +179,5 @@ ext ty = case ty of
          I.Word16 ->  "u16"
          I.Word32  -> "u32"
          I.Word64  -> "u64"
+  I.TyIndex _ -> ext I.ixRep
   _ -> error $ "Unexpected type " ++ show ty ++ " in ext."

ivory-opts/src/Ivory/Opts/TypeCheck.hs

@@ -121,7 +121,7 @@ tyChk ty        stmts = void (tyChk' (False, False) stmts)
   where
   tyChk' :: (SubBlk, Ret) -> [I.Stmt] -> TCResults Ret
   -- Ret and no other statemnts
-  tyChk' (_, True) []
+  tyChk' (_, True) ss | all isComment ss
     = return True
   -- Ret and other statements
   tyChk' (sb, True) ss
@@ -152,5 +152,8 @@ tyChk ty        stmts = void (tyChk' (False, False) stmts)
   tyChk' b (_:ss)
     = tyChk' b ss
 
+  isComment (I.Comment _) = True
+  isComment _             = False
+
 xor :: Bool -> Bool -> Bool
 xor a b = (not a && b) || (a && not b)

ivory/src/Ivory/Language/Array.hs

@@ -29,11 +29,16 @@ import GHC.TypeLits (Nat)
 -- modifying the other packages.
 type IxRep = Sint32
 
+-- | The representation type of a @TyIndex@, this is fixed to @Int32@ for the
+-- time being.
+ixRep :: I.Type
+ixRep = ivoryType (Proxy :: Proxy IxRep)
+
 -- | Values in the range @0 .. n-1@.
 newtype Ix (n :: Nat) = Ix { getIx :: I.Expr }
 
 instance (ANat n) => IvoryType (Ix n) where
-     ivoryType _ = ivoryType (Proxy :: Proxy IxRep)
+  ivoryType _ = I.TyIndex (fromTypeNat (Proxy :: Proxy n))
 
 instance (ANat n) => IvoryVar (Ix n) where
   wrapVar    = wrapVarExpr
@@ -123,4 +128,3 @@ arrayLen _ = fromInteger (fromTypeNat (aNat :: NatType len))
 arr ! ix = wrapExpr (I.ExpIndex ty (unwrapExpr arr) ixRep (getIx ix))
   where
   ty    = ivoryArea (Proxy :: Proxy (Array len area))
-  ixRep = ivoryType (Proxy :: Proxy IxRep)

ivory/src/Ivory/Language/Cast.hs

@@ -281,6 +281,7 @@ toMaxSize ty =
                     AST.Word16 -> fromIntegral (maxBound :: Word16)
                     AST.Word32 -> fromIntegral (maxBound :: Word32)
                     AST.Word64 -> fromIntegral (maxBound :: Word64)
+    AST.TyIndex n -> Just n
     _          -> Nothing
 
 toMinSize :: AST.Type -> Maybe Integer
@@ -296,6 +297,7 @@ toMinSize ty =
                     AST.Word16 -> fromIntegral (minBound :: Word16)
                     AST.Word32 -> fromIntegral (minBound :: Word32)
                     AST.Word64 -> fromIntegral (minBound :: Word64)
+    AST.TyIndex _ -> Just 0
     _          -> Nothing
 
 --------------------------------------------------------------------------------

ivory/src/Ivory/Language/Loop.hs

@@ -37,6 +37,7 @@ loop incr fromIdx toIdx body = do
   ix        <- freshVar "ix"
   let ixVar = wrapExpr (AST.ExpVar ix)
   (_,block) <- collect (body ixVar)
+  -- XXX TODO: are these still needed??
   let asst v = compilerAssert (wrapExpr v <? maxSz .&& (-1::IxRep) <=? wrapExpr v)
   asst from
   asst to

ivory/src/Ivory/Language/Syntax/AST.hs

@@ -267,7 +267,7 @@ data Expr
   | ExpLabel Type Expr String
     -- ^ Struct label indexing.
 
-  | ExpIndex Type Expr Type Expr
+  | ExpIndex Type Expr Type Expr -- XXX Do we need the 2nd (index) Type?
     -- ^ Array indexing.  The type is the type of the array being indexed, it's
     -- implied that the expression with the array in it is a reference.