verifit / angie Goto Github PK

Collected tasks relevant to console application variant of Angie. opt pass variant is also planned, and that should considered when implementing console functionality.

• Analysis should be self-contained, but for start all compiled into one application. One should be able to pick the analysis he ones to run via parameter.
• Print diagnostic messages in GCC/clang compatible format (create wrapper around LLVM pass diagnostics message machinery ?)

TODO:

• @michkot fix comments
• @michkot add new test cases, with heap memory, linked memory, gradually aiming for (ubounded?) list creation and abtraction
• Q: @peringer, @ondrik, @tfiedor Should macros be used in the test cases?
  a) in repo
  b) during compilation
• Q: @peringer, ... Is there a way to expand just #define and not includes?

Pick a unit testing framework (probably gtest) and write test for created (S)MG representation #2.

Create a functioning Memory Graph representation, without any abstraction.
Created implementation should have a solid API and be backed by tests.

Design several possible ways how to attach information to instructions or values.
Present motivation for this is dead/live variable analysis - results of such an analysis could be precomputed and assigned either to CfgNodes (instructions) or to FrontendIds (values / SSA registers).

Info sources:
https://github.com/kdudka/predator/blob/master/cl/killer.cc
http://llvm.org/docs/doxygen/html/LiveVariables_8h_source.html
http://llvm.org/docs/doxygen/html/classllvm_1_1LiveVariables.html

• Work on stabilizing API for some kind of SMG introspection
• Create recursive visitor for traversing SMG
• Create printing visitor taking advantage of new or existing visualization library

What should the interaction of user and the analysis look like when an error has been found?

We can assume it should like like some kind of back-trace explaining the origin of such erroneous state.
Could be:

• dumping analysis specific graphic/text (SMG plots) for deduced or manually specified points of program
• print compiler-message-like line-of-code back-trace for every line that participated in origin of error-triggering value
• dumping SVCOMP-like XML error trace for the user
• dumping executable (debugging possible) error trace for the user

This issue is about

1. coming up with other user interaction patterns
2. discussing those patterns, theirs pros, cons and whether their implementation is feasible ATM
3. which patterns should we implement framework-wide / we should at least provide support for them in Angie and which patterns are suitable only for analysis-specific implementation

Keep in mind that Angie is meant to be an analysis framework.

Running angie on this code:

  1 int main(void)
  2 {
  3         int *p = malloc(sizeof *p);
  4         free(p); 
  5         free(p);
  6 
  7         return 0;
  8 }

Results in

terminate called after throwing an instance of 'NotSupportedException'
  what():  attempted to call unknown function -- either an unsupported stdlib function or missing definition

The problem is that #include <stdlib.h> is missing and calls to free are wrapped in ConstExpr due to unknown prototype, e.g.:

call i32 (i32*, ...) bitcast (i32 (...)* @free to i32 (i32*, ...)*)(i32* %7)

Adding #include<stdlib.h> fixes the problem:

$./angie -f db.ll

Error: Program tried to free an already freed memory.

We need access to program/functions/instructions details for proper development and debugging.

• Function: name, return type, argument types, argument Frontend IDs. Optional: "is intrinsic", linkage type
• Instruction: LLVM string rep, source info {file, line, column}
• Values = {Constants and Instructions}: source name (named register vs named stack variable?)

Implementation notes:
Generate map for values when creating CFG
Add "debugger mode" functionality -> retrieve all information on construction and cache it in the wrapper

Deletion used when iterating over a container which invalidates iterators upon such an operation. See code comments for more.

Adding an intrinsic IR instruction to trigger a special behaviour is relatively easy.
I would be interested in a way of simply annotating the IR code such that the analysis would trigger __builtin_trap() / __debugbreak() if compiled in debug mode.