https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add bound checking on arrays. Array accesses to undeclared arrays or out of bounds will now be caught and reported as an error. * src/str/xrm-to-prism.str: Add a type-checking pass in the main transformation pipeline. * src/str/type-check.str: New. Performs bounds checking on arrays at this time. * tests/xrm/rivf.xrm: Fix. src/str/type-check.str | 37 +++++++++++++++++++++++++++++++++++++ src/str/xrm-to-prism.str | 3 +++ tests/xrm/rivf.xrm | 2 +- 3 files changed, 41 insertions(+), 1 deletion(-) Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 82) +++ src/str/xrm-to-prism.str (working copy) @@ -38,6 +38,7 @@ builtin-rand log-timed properties-in-xrm + type-check strategies @@ -97,6 +98,8 @@ end | "AST normalization (flatten-list)", 2) + ; log-timed(type-check | "Type checking", 2) + ; if <is-module-file> start-symbol then log-timed( /* get the modules that generates random numbers (XRM rand builtin) */ Index: src/str/type-check.str --- src/str/type-check.str (revision 0) +++ src/str/type-check.str (revision 0) @@ -0,0 +1,37 @@ +module type-check + +strategies + + check-array-access = + where( + (?ArrayAccess(_, _) + \ ArrayAccessPrime(a, b) -> ArrayAccess(a, b) \) + ; ?aa + ; <fetch-idf> aa => idf + ; if <DeclaredArrays> Identifier(idf) => dims-dec then + <desugar-array-access> aa => aa-list + /* for aa in aa-list, aa must be in dims-dec otherwise it's an + * out of bounds array access. */ + ; map({aa: + ?aa + ; (where(<fetch(?aa)> dims-dec) + <+ out-of-bounds-array-access(|idf, aa, dims-dec)) + }) + else + err-msg(|["Array access on an undefined array `", idf, "'"]) + ; <debug> aa + ; <xtc-exit> 5 + end + ) + + out-of-bounds-array-access(|idf, aa-list, dims-dec) = + err-msg(|["Out of bounds array access on array `", idf, "'"]) + ; <debug(!"Out of bounds subscript: ")> aa-list + ; <debug(!"Possible subscripts: ")> dims-dec + ; <xtc-exit> 5 + + type-check = + check-array-access + <+ Module(id, type-check) + /* Because label can have array access with undefined identifiers: */ + <+ Command(id, type-check) + <+ all(type-check) Index: tests/xrm/rivf.xrm --- tests/xrm/rivf.xrm (revision 82) +++ tests/xrm/rivf.xrm (working copy) @@ -100,6 +100,6 @@ properties for T from 0 to 1200 step 100 do // Alarmed triggered before instant T? - P =? [ true U (t <= 0 & true) ] + P =? [ true U (t <= T & boundary_broadcasts) ] end end