Skip to content

Latest commit

 

History

History
179 lines (117 loc) · 6.77 KB

readme.md

File metadata and controls

179 lines (117 loc) · 6.77 KB
Raw

BASIL Development

Scala

Basil is implemented in Scala 3.

See also: Scala Gotchas.

Scala is a mixed functional and object-oriented programming language implemented on the JVM. It is a very complicated language with a lot of depth, so it is important to carefully chose the implementation complexity introduced.

Generally, this means favouring simple standard solutions and choosing functional programming over stateful object oriented style (use filter and map rather than loops), prefer immutable case classes and enums to regular mutable classes, etc.

ADTs and functions between ADTs are all you need to solve most problems. Most things more complicated than this make the code unnecessarily difficult to maintain.

It is recommended to explore the Scala documentation. There is also the incomplete Scala 3 language specification, which contains details not present in the documentation, but is not completely updated from Scala 2.

Some general advice:

  • Prefer Enums over inheritance trees
  • Use functional programming over imperative wherever possible
  • Prefer immutable case classes to regular classes wherever possible
  • Don't unneccessarily use generics or type aliases
  • Correct code should not require explicit casts (.asInstanceOf)

Code style

We do not have a strict code style however

  • Use two spaces for indentation
  • Use {} braces rather than purely indentation-based scoping
  • Do not use new or semicolons

Getting Started

  1. To set up an editor for Scala development see editor-setup.
  2. Become familiar with the project structure to start understanding the code.
  3. Install the neccessary tools here, it may be useful to try lifting examples, or just looking at existing examples in the src/test/correct directory.
  4. Use the below as a guide to common development tasks as they may arise.

Development tasks

Building

The sbt shell can also be used for multiple tasks with less overhead by executing sbt and then the relevant sbt commands.

To build a standalone .jar file, use the following command:

mill assembly

From sbt the resulting .jar is located at target/scala-3.1.0/wptool-boogie-assembly-0.0.1.jar and from mill this is out/assembly.dest/out.jar.

To compile the source without running it - this helps IntelliJ highlight things properly:

mill compile

This is used to keep track of which tests have passed previously, as well as changes to the basil output.

Debugging

Printing an analysis result

Run basil with the --analysis-result <filepath> flag to print the results of the analyses to files. The --analysis-result-dot <filepath> does the same, but outputs a graphviz digraph, which can be viewed by pasting it into edotor.net, or compiling with dot.

This prints the program with the abstract-domain lattice value at each program point following the ::.

Procedure main
  Block $main$__0__$kIwlZLaTRp6qaf6BnFzwlA
    1816$0: Register(R9, bv64) := 69632bv64
        :: Map(Register(R31, bv64) -> Bottom)
...

To achieve this for a new result in development use the following method defined in RunUtils.scala

def printAnalysisResults(prog: Program, result: Map[CFGPosition, _]): String

Tests

Unit tests

We use the ScalaTest unit testing framework. Example unit tests can be found in src/test/scala.

The dsl can be used to construct simple example BASIL IR programs, which can then be fed through into the whole pipeline via IRLoading.load() in RunUtils.scala. Prefer to write tests that depend only on the single piece of code under test rather than the whole BASIL translation.

Integration tests

These are the SystemTests.scala test case with the files present in src/test/correct for examples that should verify and src/test/incorrect for examples that should not verify.

These are lifted via the Makefiles, to add another test simply add a directory, c source file, and optionally specification file and run

cd src/test/
make

The config.mk file in the test directory can be used to exclude unnecessary compilers, and change compilation flags. Full details can be found here.

Running Tests

The test suites use ScalaTest, they can be run via.

$ mill test

To run a single test suite, for example only the system tests (requires boogie):

$ mill.test.testOnly SystemTests

To run single tests in from the test suite, they can be selected using globbing on the full test class name with the testOnly task:

$ mill test.testOnly '*SystemTests*' -- -z basic_arrays_read -z basic_arrays_write

To update the expected basil output files from the test results run

$ mill updateExpected

Performance profiling

While the first priority is correctness, the performance target for the static analyses is that we can run through the entire cntlm binary in a reasonable amount of time (seconds), depending on the expected performance of the analysis involved. Loading cntlm requires increasing the heap size by providing the -Xmx8G flag.

IntelliJ professional (which can be obtained for free by students) includes a performance profiler.

Alternatively, async-profiler can be used to produce a flame graph showing the hot-spots in the program. Download the library from the releases tab, compile a basil .jar with mill assembly and run the jar with the following arguments.

Instructions for Linux and Mac:

mill assembly
java -agentpath:$YOUR_PATH/async-profiler-2.9-linux-x64/build/libasyncProfiler.so=start,event=cpu,file=profile.html -Xmx8G -jar out/assembly.dest/out.jar -i examples/cntlm-new/cntlm-new.adt -r examples/cntlm-new/cntlm-new.relf --analyse;
firefox profile.html

You may have to give it permission to collect perf events

sudo sysctl kernel.perf_event_paranoid=1
sudo sysctl kernel.kptr_restrict=0

Managing docker containers

See docker readme