CSSE4630 Assignment 1: Array Bounds Analysis
Mark Utting, ITEE, UQ Version 1.2
1 Introduction
A software development company with a strong emphasis on cybersecurity is employing you to develop a static analysis for array bounds checking.
They have two main goals for the analysis:
Security: they want to be able to guarantee that every program they write is free from array bounds errors. The compiler for their programming language already generates code that checks the array bounds at runtime, but they want to give higher security assurances than just this. They want the static analysis to be able to prove that some array accesses are definitely safe (within bounds), and all remaining array accesses will generate warnings that will checked by a code review team to ensure that those array accesses are also within bounds. It is desirable for the static analysis to be able to put most of the array accesses into the first category (provably safe), in order to minimise work for the code review team.
Efficiency: Runtime checking of array bounds accesses has a significant overhead, so the company plans to modify their compiler to omit the bounds checking code for the cases where the static analysis can prove that the array access is within bounds.
Your task is to design and implement a suitable static analysis, for the TIP (Tiny Imperative Language) language, extended with mutable arrays.
2 TIP with Array Creation and Reading [20 Marks]
The company uses a safe subset of TIP (no pointers, records, or dynamic function calls), ex- tended with integer arrays, where each array has a fixed size that is known at compile time:
the expression newarray N creates an array of size N (which must be a constant non- negative integer value) and fills it with zeroes.
the expression A!E is an array read, and introduces the bounds-checking requirement that 0≤E
tip -interval wlrw tests/array_read1.tip >out/array_read1.tip.out
tip -interval wlrw tests/array_read2.tip >out/array_read2.tip.out
CSSE4630 Assignment 1 Page 3
4 Static Bounds Checking for Array WRITES [30 marks]
Your Task: Extend your static analysis to also check each array write to determine if the index is provably within bounds, or whether it needs a runtime bounds check and a warning about the bounds (which means that the code review team must review that access).
First you will need to extend the TIP language to allow array index expressions on the left- hand-side of assignments:
the assignment A!E = E2 is an array write, and introduces the bounds-checking require- mentthat0≤E
tip -interval wlrw tests/array_write2.tip >out/array_write2.tip.out
tip -interval wlrw tests/array_write3.tip >out/array_write3.tip.out
5 Customer Responses
You test your static analysis thoroughly and then release it to your customers. They are happy — for a week or so!
CSSE4630 Assignment 1 Page 4
Then they report that their programmers are complaining that the bounds analysis is reporting too many false positives. Their review teams are spending too much time reviewing potential out-of-bounds reports that turn out to be obviously within bounds. They want a more precise analysis with fewer false positives!
They would also like to have a static typechecker for the extended TIP language.
You have limited time, so you have to prioritise which of these two requests to work on.
6 Option A: Path-Sensitive Bounds Analysis [20 marks]
NOTE: this part of the assignment is more difficult than the previous parts. Attempt it only after you have completed the previous steps.
After investigating the complaints from your customer, you find that the above bounds analysis works well for straight-line code, but does not handle programs with if-else branches and loops in a very precise way.
Try your analysis on tests/array if1.tip. You will find that it reports possible out-of-bounds errors (false positives), even though the program actually uses if-else statements to ensure that the array accesses are within bounds. This lack of accuracy is because the effects of the control flow are not included in your analysis.
Your Task: add assertions into the (internal) TIP language and incorporate them into your bounds analysis so that the analysis is more accurate when programs contain branches and loops.
Steps:
Add an assert statement to the language, as a subclass of AStmtInNestedBlock.
You will also need to add this assert statement into AstPrinters, DepthFirstAstVisitor and TipNormalizers. Hint: I looked at the usages of AErrorStmt and used those usages as a guideline for the assert case.
You do not have to add it to the parser, since this assert statement will be for internal use only.
You need to insert assert statements after each condition check, where the flow of control changes in while and if statements. See Section 7.1 of the textbook for details. Hint: a nice place to do this is in TipNormalizers.normalizeStmtInNestedBlock.
Extendyourboundsanalysistohandleassertions,byimplementingtherulesforassert(X>E) and assert(E>X) that are discussed on page 84 of the textbook.
After implementing your bounds analysis of array writes, try running the command:
tip -normalizereturns -interval wlrw tests/array_if1.tip
Note that you must include the -normalizereturns flag from now on, to ask TIP to run your normalizer. (By default, TIP does no normalization).
You should see output that includes the following bounds-checking output lines (shown in blue):
[info] Running tip.Tip -normalizereturns -interval wlrw tests/array_if1.tip
[info] Normalized analysis of tests/array_if1.tip written to out/array_if1.tip__normalized.tip
Array bounds analysis results:
ArrayWrite:10:11: safe
[info] Interval analysis of tests/array_if1.tip written to out/array_if1.tip__interval.dot
CSSE4630 Assignment 1 Page 5
Once you have finished implementing your path-sensitive static bounds analyser, run it on ALL the test programs in the tests folder. For each test program P.tip, save the output of your run into a file out/P.tip.out. These will be part of your submission, to demonstrate how well your bounds checker works.
For example, here is a bash command to run them all:
#!/usr/bin/env bash
for T in $(cd tests; ls *.tip) do
echo $T
./tip -normalizereturns -interval wlrw tests/$T >out/$T.out done
7 Option B: Typechecking Arrays [20 marks]
Your customers would like to have a static typechecker for the TIP language, extended with arrays, and have offered to pay for the development of the typechecker.
Your Task: implment a static typechecker for TIP, including the extra type constraints asso- ciated with arrays.
Note: This ‘Typechecking’ task is an alternative task to the previous ‘Assertions’ task. You can attempt either task. If you attempt both, then your mark for these two sections will be max(A,T), where A is your mark from the ‘Assertions’ task and T is your mark from the ‘Typechecking’ task.
You will first need to implement the typechecking rules for standard TIP programs in TypeAnalysis.scala, since they not fully implemented.
Then you can add the new array(N) type as a subclass of TipType in Types.scala, and implement the additional typechecking rules for arrays.
See Section 3.2 of the textbook for the standard TIP type constraints. Here are the additional array-specific typechecking constraints for our custom TIP extension.
A!E [A] = array(N) ∧ [E] = int ∧ [A!E] = int newarray N [N ] = int ∧ [newarray N ] = array(N )
8 Submission
This assignment is due on Friday of Week 10 (16-Oct-20 6pm Queensland time). Submit your whole repository on Blackboard, in a single *.zip file. Make sure you include:
the ‘src’ folder, containing all the Scala source code, including your modifications.
your BoundsAnalysis.txt file (or BoundsAnalysis.docx) that documents the bounds- checking rules that you have designed. You can also explain any design decisions or limitations in that file, if needed.
the ‘out’ folder, containing all your final out/array*.tip.out files and all the *.dot files generated by your analysis. These show the final output from each run of your bounds analyser on the various test programs.
CSSE4630 Assignment 1 Page 6