This PR brings multiple new features from our development branches. In general this PR focuses on three main features:

1. BIL correctness and normalization
2. BIL readability and performance
3. Primus interpreter

Note for reviewers and readers: I wouldn't expect you guys to check the code thoroughly, but you are welcome to ask questions, request clarifications, and discuss changes. Most likely just reading this PR message would be enough for the review.

Note: the Table of Contents doesn't work since Github doesn't emit anchors on the PR page. They will work (I hope so), when we will move this page to the release page.

Table of Contents

• Detailed description
  • BIL Typechecker
  • BIL effect analysis
  • New BIL simplification and constant propagation algorithm
  • BIL normal form and normalization utilities
  • SSA transformation plugin
  • Dead code elimination plugin
  • New pretty printer for bitvectors
  • New functions for bitvectors
  • New pretty printer for BIL
  • Identifiable values for the Primus interpreter
  • New Primus interpreter
  • New Primus Value representation
  • New Primus Mark Visitied plugin
  • Diagnostic messages with better backtraces
  • Fixes and updates for the x86 lifter
  • Bug fixes in ARM lifter
  • Support for tracing and other minor fixes
• Caveats, Limitations, and Regressions
• TODO

Detailed Description

BIL Typechecker

We added a type checker, and now force all BIL code to be well-typed. Lifters must produce only well-typed code. So far, we will issue a warning for each piece of code that is not, along the 1.4 we are planning to fix all issues if any. The Type module now have the infer function, that will infer type for an expression, and check that will type check a BIL program.

BIL Effect Analysis

A precise effect analysis was added to ensure correctness of program transformations. The effect analysis distinguishes between different effects and coeffects:

• reads (coeffect)
• loads (coeffect)
• writes (effect)
• raises (effect)

The raises effect includes the division by zero CPU exception and a conservative AI will infer a possible presence of the division by zero in a BIL expression.
A new module, called Eff is added, that provides functions for the effect analysis.

BIL Simplification and Constant Propagation

The old constant propagation and simplification algorithm was buggy, and didn't take into account effects when removing statements and subexpressions. It was rewritten from scratch with an algorithm that is sound and parametrized by the set of effects, that may be ignored during the analysis. The new analysis treats operations accurately with respect to their algebraic properties and takes into account operations associativity. It is also now a big step analysis and no longer requires to be wrapped into the fixpoint function. Basically, we are moving from the open and semi-open recursion to the closed recursion wherever it is possible, as it is more efficient and intuitive approach. We will probably remove the fixpoint function in BAP.2.0.

BIL normal form and normalization utilities

We introduce a notion of a BIL Normal Form, that is a sub-language of BIL that disallows certain constructions, such as let and if/then/else expressions, complex memory expressions, and complex conditionals. This doesn't impose, that those expressions are not allowed in general, and lifters can still emit code that is easier to write. All such expressions are removed, i.e., are rewritten during the normalization process. The normalization procedure is described in details in the documentation, as well as in comments. Here is a brief highlight:

1. no let expressions
2. no if/then/else expressions
3. all memory operations are one-byte only (size and endianness can be ignored)
4. no anonymous memory storages - load expressions may load only from a variable
5. no loads and stores inside conditional expressions
6. no ill-typed expressions

SSA transformation plugin

This is a simple plugin that just transfers all functions into SSA form. It was moved from the bap-plugins repository.

Dead code elimination plugin

A sound analysis that will remove all unused code. This plugin is very useful, as it will remove lots of unnecessary code that are emitted by lifters. In particular, on x86 it removes flag compuations that are not used anywhere. As a result, this reduces the size of the output to 50% on x86 and makes BIL much more readable. It also highly increases the speed of interpretation. Especially, since many flag computations are quite computationally hard.

New pretty printer for bitvectors

Printers from the Z library proved to be slow, buggy, and ugly. Thus we decided to provide our own pretty-printer that will suit all the needs. A generic printer is added, that allows a user to customize the look of the textual representation of a bitvector. We also provide 9 different instantiations of the generic printer, e.g., pp_hex, pp_dec, pp_oct and pp_bin that will print a bitvector in the corresponding format. We also remove suffixes from a bitvector to make output more readable and concise. The full version is available via pp_hex_full, pp_dec_full, ... printers. We also change a default textual representation (i.e., to_string and pp) functions. The new representation now includes the signedness suffix, and moves away from using true and false for the one-bit words.

New functions for bitvectors

We added the to_int[XX]_exn family of functions, that will efficiently cast a bitvector into a corresponding OCaml type without extra allocations whenever possible. For example, Word.to_int_exn is usually an identity function w.r.t. the GC (i.e., it still has a check that value fits, and if it is, the it is an identity).

We also added the Word.unsigned function that will cast away the signedness of a bitvector.

The Unsafe module was added to the bitvector interface that provides arithmetic instructions that do not check that operands have correct widths. The module can be used for interpreting a well-typed BIL code. Moreover, these operations are included by default in the Bitvector top-level interface, thus, a Word.(a + b) will result in the unsafe (+) operator.

New pretty printer for BIL

We implemented a new pretty printer that (i) doesn't emit unnecessary parentheses anymore, and uses more concise syntax whenever it is possible. We followed the C language for the operator precedence (not OCaml). Here is the precedence table:

   +-------------------------------------------+----+
   | x[y], <cast>:<N>[x], extract:<N>:<M>[x]   | 10 |
   +-------------------------------------------+----+
   | ~x, -x                                    |  9 |
   +-------------------------------------------+----+
   | *,/,/$, %, %$                             |  8 |
   +-------------------------------------------+----+
   | +,-                                       |  7 |
   +-------------------------------------------+----+
   | <<,>>,~>>                                 |  6 |
   +-------------------------------------------+----+
   | <,>,<=,>=                                 |  5 |
   +-------------------------------------------+----+
   | =, <>                                     |  4 |
   +-------------------------------------------+----+
   | &                                         |  3 |
   +-------------------------------------------+----+
   | ^                                         |  2 |
   +-------------------------------------------+----+
   | |                                         |  1 |
   +-------------------------------------------+----+
   | let.., x with y <- z, if.., . (dot)       |  0 |
   +-------------------------------------------+----+

1. Higher precedence means that operators binds tighter.
2. Any bil statement has precedence lower than an expression

The load and store expressions are also simplifed, now it is not necessary to put the endiannes and size if an expression is byte sized.

Identifiable values for the Primus interpreter

We used the word type for values in the Primus interpreter, however, it showed that it is very hard to write a data tracking analysis without being able to identify values. For example, in the taint propagation plugin, we implemented a stack machine for tracking the taint. It is not only hard to maintain and understand, but also is inefficient. This defeats the main reason why we decided to use the word type as a value representation in the interpreter -- the efficiency.

We now represent a computation result as a pair of a word and a unique identifier. Basically the same as with the Bil.Result.t except that we are not using a variant type to represent storages and bottom values. In the Primus model, there are no such values, and everything is represented with a machine word, coined with an identifier.

To make it easier to work with the new values, we lifted most of the bitvector interface into the value interface.

New Primus interpreter

The Primus Interpreter is reimplemented and doesn't use the eval or microx code anymore (though there is still lots of code sharing since we factorized a lot of code from microx to the BIL library). The interpreter now tracks data much more closely, and provides an interface that allows code summaries, that are implemented in Lisp or in OCaml or in any other language to describe all code effect precisely. We also revisited observations that are made by the interpreter, and moved memory and environment observations into the interpreter.

New Primus Mark Visitied plugin

This plugin will mark each term that is visited (evaluated) by the Primus interpreter with the visited attribute. It is useful for tracking the coverage.

Diagnostic messages with better backtraces

There is an impedance mismatch between OCaml exceptions and the error monad. Sometimes we switch from one to another and loose the backtracing information. Now the backtraces are always stored in Or_error.t values and are printed in case of failure.

Caveats, Limitations, and Regressions

1. The normalized form is not represented in a type system, thus it maybe applied more than once. In future we are planning to add phantom types for that.

2. The dead-code elimination plugin is computationally intensive but is not cached. Thus the startup time of each binary is actually increased. We will later and the caching layer to alleviate this.

Fixes and updates for the x86 lifter

The shift operation representation was slightly incorrect, as it was using x := x instruction to represent that the value of x is unchanged. From the analysis perspective this is not entirely true, as it is an update of a variable, an unnecessary usage (that keeps DCE from removing this statement) and, in many cases, it left the right hand side left variable upper exposed, that was introducing a source of undefined values, as well as prohibited certain kind of optimizations on the interprocedural values (we were forced to treat x as an implicit input parameter of a function, where it is upper exposed).

The shift lifter also introduced unnecessary temporal variables, as well as used lots of ite. The former is removed, the latter is translated into one if statement (basically all ite were guarded by the same condition, so we can gather them, that will lead to much better CFG).

Bug fixes in ARM lifter

The ARM lifter was emitting badly typed code. Now it is fixed.

Support for tracing and other minor fixes

We added a handler for SIGINT so that gprof and other utilites, that requires a correct exit call, can work properly. We also added BAP_DEBUG=true to the Travis environment to ease the debugging on it.

TODO

Note, this is a work in progress, there are still a few minor issues that should be resolved before this branch would be ready for the merge. Here comes a list

• Mark all new functions with the @since tag
• Document all new functions
• update all lifters with the typechecking code
• remove calls to Bil.fixpoint as it is no longer necessary (in most cases)
• check that all new plugins have sufficient manpages and documentation
• check that all usages of Word.string_of_value are consistent, so that we will not break any integrations with external tools
• update README.md with nice examples of BIL. Ideally, use the well-known strcpy as an example.
• rewrite observer notifications so that flambda can inline them
• cleanup the observations, make sure that we don't have any dead observation handlers.