Defer RETYPES safety check until runtime

fco2/GenerateC.hs

@@ -749,8 +749,8 @@ abbrevVariable am t v
     = (genVariableAM v am, noSize)
 
 -- | Generate the size part of a RETYPES/RESHAPES abbrevation of a variable.
-genRetypeSizes :: A.AbbrevMode -> A.Type -> A.Name -> A.Type -> A.Variable -> CGen ()
-genRetypeSizes am destT destN srcT srcV
+genRetypeSizes :: Meta -> A.AbbrevMode -> A.Type -> A.Name -> A.Type -> A.Variable -> CGen ()
+genRetypeSizes m am destT destN srcT srcV
     = case (destT, srcT) of
         -- An array -- figure out the new dimensions.
         (A.Array destDS destSubT, _) ->
@@ -774,11 +774,13 @@ genRetypeSizes am destT destN srcT srcV
                     tell ["_sizes[] = { "]
                     let dims = [case d of
                                   A.UnknownDimension ->
-                                    do tell ["("]
+                                    do tell ["occam_check_retype ("]
                                        genVariable srcV
                                        tell ["_sizes[", show srcNum, "]"]
                                        tell [" * ", show srcBytes]
-                                       tell [") / ", show destBytes]
+                                       tell [", ", show destBytes, ", "]
+                                       genMeta m
+                                       tell [")"]
                                   A.Dimension n -> tell [show n]
                                 | d <- destDS]
                     sequence_ $ intersperse genComma dims
@@ -968,7 +970,7 @@ introduceSpec (A.Specification _ n (A.Proc _ sm fs p))
           tell [") {\n"]
           genProcess p
           tell ["}\n"]
-introduceSpec (A.Specification _ n (A.Retypes _ am t v))
+introduceSpec (A.Specification _ n (A.Retypes m am t v))
     =  do origT <- typeOfVariable v
           let (rhs, rhsSizes) = abbrevVariable A.Abbrev origT v
           genDecl am t n
@@ -987,7 +989,7 @@ introduceSpec (A.Specification _ n (A.Retypes _ am t v))
           tell [") "]
           rhs
           tell [";\n"]
-          genRetypeSizes am t n origT v
+          genRetypeSizes m am t n origT v
 --introduceSpec (A.Specification _ n (A.RetypesExpr _ am t e))
 introduceSpec n = missing $ "introduceSpec " ++ show n
 

fco2/Parse.hs

@@ -1326,10 +1326,12 @@ checkRetypes fromT toT
           let ok = case (bf, bt) of
                      (BIJust a, BIJust b) -> a == b
                      (BIJust a, BIOneFree b _) -> (b <= a) && (a `mod` b == 0)
-                     (BIOneFree a _, BIOneFree b _) -> (b <= a) && (a `mod` b == 0)
+                     -- In this case we do a runtime check.
+                     (BIOneFree _ _, BIOneFree _ _) -> True
+                     -- Otherwise we can't tell.
                      _ -> False
           when (not ok) $
-            fail $ "cannot prove that RETYPES/RESHAPES is safe"
+            fail $ "RETYPES/RESHAPES sizes do not match"
 
 dataSpecifier :: OccParser A.Type
 dataSpecifier

fco2/tock_support.h

@@ -68,6 +68,13 @@ static int occam_check_index (int i, int limit, const char *pos) {
 	}
 	return i;
 }
+static int occam_check_retype (int, int, const char *) occam_unused;
+static int occam_check_retype (int src, int dest, const char *pos) {
+	if (src % dest != 0) {
+		occam_stop (pos, "invalid size for RETYPES/RESHAPES (%d does not divide into %d)", dest, src);
+	}
+	return src / dest;
+}
 //}}}
 
 //{{{ type-specific arithmetic ops and runtime checks