STATOR:Establishing code-base

Here we list pros and cons of all our approaches towards establishing STATOR's code-base. All pros/cons are listed in the order from the most important to the least one. We further assign for all listed pros/cons a global "importance level", which is a number in [1,...,10].

• TODO:
  • Update information in all pros/cons points in all subsections below such that free tools like PAGAI, FramaC, UFO, CPROVER, CBMC, KLEE, Bugst, etc. are included.

Perspective 1: Main implementation language/platform

Java

• pros
  • We can take a lot of code from tools like CPAchecker and Stanse with minimal effort.
  • Huge standard library
  • There several very good IDEs for development of Java applications.
  • It is stable and portable to many different platforms.
  • Many students know it.

• cons
  • Implementation of some program analyses may be slower then the one in programming languages like OCaml or F#. Nevertheless, it is quite difficult to predict impact of this potentially increased programming effort.

F# (.NET/Mono)

• pros
  • May provide faster implementation of some program analyses then in Java, because symbolic manipulations of particular data structures (like syntax trees, expressions, BDD,...)
  • We can take a C front end from tools like CPAchecker, Stanse, Bugst, or Predator with minimal effort. It only requires to dump internal CFG representations of the tools to disc and load them into equivalent data structures syntactically expressed in F#.
  • When we are in .NET we can freely use any other .NET language (C#, Visual basic, managed C++, ...). Since many students know C# and C# is similar to (or better then) Java, so from this point of view F# is better choice then Java. Moreover, there is also implemented integration of non-managed languages, but portability is then a question.
  • We can move to Windows and thus develop STATOR in Visual Studio. (Visual Studio can really speed-up development (e.g. excellent debugging, edit&continue, ...)

• cons
  • Development in Mono can be less comfortable. Also support of F# in Mono known to us yet. Similarly, state of standard library is not know.
  • Portability mostly depends on qualities of Mono.
  • Not many people knows it, but the situation improves.

OCaml

• pros
  • May provide faster implementation of some program analyses then in Java, because symbolic manipulations of particular data structures (like syntax trees, expressions, BDD,...)
  • We can take a C front end from tools like CPAchecker, Stanse, Bugst, or Predator with minimal effort. It only requires to dump internal CFG representations of the tools to disc and load them into equivalent data structures syntactically expressed in OCaml.

• cons
  • OCaml development environments are still immature and primitive. This can slow down whole development.
  • Not many people knows it, but the situation improves.
  • OCaml is not that portable as Java.

C++

• pros
  • a

• cons
  • a

Perspective 2: Programs in what languages should STATOR analyse

Using dedicated C front-end

• pros
  • Such front-ends are already available in tools like CPAchecker, Stanse, Predator, ...
  • In CPAchecker they are implementing front-end to Java. So there is posses their code, when it is ready.

• cons
  • Extension of STATOR to other languages will be complicated, unless Dirk's endeavour with Java front-end will continue (maybe they plan to implement front ends to further languages; then this cons would actually not be cons anymore.)

Using LLVM front-end

• pros
  • LLVM project intends to compile several languages into LLVM byte code (C,C++, Objective C, Java,...). So, this might be valuable for future of STATOR. But if development of STATOR will formally end in 2017. If there are no successor projects, then this feature does not matter.

• cons
  • I know only one tool, Bugst, which translates LLVM into an internal control-flow graph representation. So, only this tool can be used for F# or OCaml platform for STATOR. But Bugst is not finished, so some LLVM features are not supported. Other LLVM based tools like PAGAI, KLEE do not transform LLVM into an internal CFG representation.