Overview
02141 Computer Science Modelling Mandatory Assignment
The overall goal of the assignment is to build a tool for running and analysing programs written in a variant of the Guarded Command Language (GCL). The tool you will develop can be seen as a basic version of formalmethods.dk/fm4fun with a text-based interface.
The assignment is divided in tasks. Each task is devoted to a module of the tool (a parser, a compiler, an interpreter and two analysers). Each module should be runnable as a standalone program that takes as input a GCL program and produces a result.
The overall structure of the assignment is illustrated below and it can be used as a guideline for structuring the implementation.
TASK 2
Compiler
TASK 5 TASK 4 TASK 3
GCL program
TASK 1
parser generator
GCL AST
GCL Parser
ok/ko
PG
memory
Analysis Results
Analysis Results
Grammar for GCL
GCL AST PG Interpreter
Signs Analyzer
Security Analyzer
1
Yet Another GCL variant
The variant of GCL that you have to consider is the following subset of the language used in formalmethods.dk/fm4fun:
C ::= x := a | skip | C ; C | if GC fi | do GC od
GC ::= b -> C | GC [] GC
a ::= n | x | a + a | a – a | a * a | a / a | a ^ a | (a)
b ::= true | false | b & b | b | b | b && b | b || b | !b
| a = a | a != a | a > a | a >= a | a < a | a <= a | (b)
This GCL variant can be seen as a language in between the one presented in [Formal Methods, Definition 2.3] and the one used in formalmethods.dk/fm4fun.
The syntax of variables and numbers, and the associativity and precedence of operators must be the same as in formalmethods.dk/fm4fun, which can be read by clicking on the question mark left to “Examples”. We reproduce part of them here for your convenience:
• Variables x are strings matching the regular expression [a-zA-Z][a-zA-Z\d ]* and can- not be any of the keywords.
• Numbers n match the regular expression \d+. Negative numbers are expressed using the unary minus operator -n.
• A whitespace matches the regular expression [\u00A0\f\n\r\t\v], with a mandatory whitespace after if, do, and before fi, od. Whitespaces are ignored anywhere else.
• Precedence and associativity rules:
– In arithmetic expressions, precedence is highest for - (unary minus), then ^, then *
and /, and lowest for + and - (binary minus).
– In boolean expressions, precedence is highest for !, then & and &&, and lowest for |
and ||.
– Operators *, /, +, -, &, |, &&, and || are left-associative.
– Operators ^, [], and ; are right associative.
In the rest of the document GCL refers to the above language.
2
Tasks
Task 1: A parser for GCL. The goal of this task is to implement a parser for GCL that accepts or rejects programs, thus working like the syntax checker of formalmethods.dk/fm4fun but in a simplified way. The parser must take as input a string intended to describe a GCL program and must produce the string ok if the input is a program accepted by the GCL grammar specified above, or ko otherwise.
Submission deadline: March 14, 23:59
Hints: Use a parser generator as seen in class. Start with the grammar as given above and adapt it to your parser generator. You may need to specify precedence/associativity of some operators in the parser generator language, or by applying some of the grammar transformations seen in class. Your parser does not need to generate abstract syntax, which is the main aim of task 2.
Task 2: A compiler for GCL. The goal of this task is to implement a compiler of GCL programs into Program Graphs (PGs) similar to results you obtain under “Program Graph” in formalmethods.dk/fm4fun. The program must take a GCL program as input and must produce a PG in the output. The format of the output must be the same textual graphviz format used by the export feature of formalmethods.dk/fm4fun. Decide if you want to construct a deterministic PG or a non-deterministic PG first. You are encouraged to write a compiler that supports both options.
Submission deadline: March 28, 23:59
Hints: Enrich the parser developed in Task 1 so that it builds abstract syntax for GCL pro- grams. Follow [Formal Methods, Chapter 2.2] to construct a PG for a GCL program. You can use graphviz tools to visualize the PGs that your compiler produces.
Task 3: An interpreter for GCL. The goal of this task is to implement an interpreter for deterministic GCL programs that works similarly to the Environment “Step-wise Execution” in formalmethods.dk/fm4fun. The interpreter must take a GCL program as input and must output the status of the program (terminated/stuck) and the memory when the program stops. The initial value of all variables must be 0. Variables can of course be initialised differently at the beginning of the program via assignments. The format for the output must be like in this example:
status x y z
terminated 7 13 0
i.e. a line with with the string status followed by the variables of the program and a second line with the actual status (terminated/stuck) and the values for each variable.
Submission deadline: April 4, 23:59
Hints: Enrich the parser developed in Task 2 so that it produces abstract syntax for PGs. Fol- low [Formal Methods, Chapter 1.2] and [Formal Methods, Chapter 2.3] to build an interpreter based on the semantics of GCL programs and their PGs.
3
Task 4: A sign analyser for GCL. The goal of this task is to implement a tool for sign analysis of GCL programs that works like the one available under Environment “Detection of Signs Analysis” in formalmethods.dk/fm4fun. The tool must take a GCL program as input and must print the result of a sign analysis for the variables at the end of the computation. The sign analysis must follow the approach in [Formal methods, Chapter 4]. You will need a way to specify the abstract initial values in the tool (e.g. reading them from a file or from the console input). The variables and their signs must be printed in the same order as formalmethods.dk/ fm4fun does. An example of the output of an analysis that produces three abstract memories should look like this:
xyz +-- -+- 0+0
Submission deadline: April 25, 23:59
Hints: Enrich the parser as you did in Task 3 and follow [Formal Methods, Chapter 4] for implementing the sign analysis.
Task 5: A security analyser for GCL. The goal of this task is to implement a tool for security analysis of GCL programs, that works as a simplified version of the Environment “Security Analysis” in formalmethods.dk/fm4fun. The tool must take a GCL program as input and must print the result of the security analysis (secure/not secure). The security analysis must follow the approach in [Formal methods, Chapter 5.3]. You will need a way to specify the admissible flows between variables (e.g. reading them from a file or from the console input).
Submission deadline: May 9, 23:59
Hints: Enrich the parser as you did in Task 3 and follow [Formal Methods, Chapter 5.3] for im- plementing security analysis. Base your analysis on deterministic PG. Note that formalmethods. dk/fm4fun implements a different approach (based on the approach described in Chapter 5.4) but you can still use it to test your analyzer. To do so, you need to proceed as follows. Partition the set of variables in the program into disjoint sets Vi, .., VN . Each Vi becomes a security label. Label the variables accordingly, i.e. in the tool you specify x = Vi iff x ∈ Vi. In your analysis, consider a flow relation ⇒ between the sets Vi,..,VN that forms a directed acyclic graph. In formalmethods.dk/fm4fun specify only the edges of the graph.
4
Additional Information
Guidelines and software installations Guidelines for installing and using parser gener- ators can be found at https://gitlab.gbar.dtu.dk/02141. Installation of software is your responsibility. If you run into problems try first to report them in Piazza to share knowledge about problems and solutions. Inquiry the TAs only after having invested enough time trying to find a solution.
Requirements The project can be done in teams. The maximum size of a team is 3, which is also the suggested size.
There is no constraint on specific programming languages or parser generators to be used. However, the TAs will provide support on F#/FSLexYacc only.
There is also no requirement on how input and output should be handled. One option is to use the standard input and ouput. Another option is to use textfiles.
Submission is through CampusNet. For each task you need to do a submission on Campus- Net within the specified deadline.
You can continue working on the module of a task after the corresponding deadline has passed. For example, if you discover bugs in the parser while doing the interpreter.
You have to submit well-commented code and instructions (e.g. a README file) explaining which are the key files and how to install and run the project. You can also submit a reference to a specific version of a software repository (github and similar). You don’t need to submit a report.
Feedback and testing We promote active and immediate feedback for your assignment. This means that you have to proactively seek feedback by testing your solution.
We suggest several ways to achieve this:
• For each task prepare a set of (manually or automatically generated) test cases (GCL programs).
• Use the test cases to test your project against formalmethods.dk/fm4fun. Do you obtain the same results? If not, reflect on which of the two tools is providing the correct result.
• Use the test cases to test your project against the project of another team. Do you obtain the same results? If not, reflect on which of the two tools is providing the correct result.
• Challenge other teams to “hack” your project: can they find cases where your project provides wrong results?
• In case of disagreement on a result, ask the TAs or the teacher for feedback.
Evaluation Mandatory assignments do not contribute to the grade. Recall the course de- scription: “Mandatory assignments provide a good background for learning the methodology of the course as will be tested at the exam.”
5