Module Bap_wp.Bil_to_bir

This module provides utilities to translate from a BIL Bil.t expression to a BIR subroutine, for which we can then invoke Precondition.visit_sub to get the weakest precondition.

This enables using the clean BIL embedded DSL syntax, e.g.

Bil.([
    v := src lsr i32 1;
    r := src;
    s := i32 31;
    while_ (var v <> i32 0) [
      r := var r lsl i32 1;
      r := var r lor (var v land i32 1);
      v := var v lsr i32 1;
      s := var s - i32 1;
    ];
    dst := var r lsl var s;
  ]) |> bil_to_sub

As in the BAP documentation, to build subroutines.