Partitioning

Summary

This MR adds a partitioning combiner that helps in developing trace and state partitioning abstract domains.

Details

The signature of partitioning domains is defined in analyzer/framework/sig/abstraction/partitioning.ml:

module type PARTITIONING =
sig
  type t

  val name : string
  val checks : check list

  val print : Format.formatter -> t -> unit
  val compare : t -> t -> int

  val init : t
  val add  : marker -> t -> t
  val exec : stmt -> ('a, t) man -> 'a flow -> 'a post option
  val eval : expr -> ('a, t) man -> 'a flow -> 'a eval option
  val ask  : ('a, 'r) query -> ('a, t) man -> 'a flow -> ('a, 'r) cases option
end

The framework combines a partitioning domain P with an underlying abstract domain D by creating a map from P.t to D.t. The type P.t of partitions keys should define a complete order P.compare. This implies that there is no join/widening defined for partitions keys, so they need to be finite.

Markers

Markers are used by domains to indicate particular points during a trace. For example, the intraproc iterator for Universal uses markers to distinguish between the two branches of an if statement. To do so, it declares a new marker:

type marker += M_if of bool * expr

let () = register_marker {
    marker_print = (fun next fmt -> function
        | M_if(true, cond) ->
          Format.fprintf fmt "if (%a)" pp_expr cond
        | M_if(false, cond) ->
          Format.fprintf fmt "if (!%a)" pp_expr cond
        | m ->
          next fmt m
      );
    marker_compare = (fun next m1 m2 ->
        match m1, m2 with
        | M_if(branch1, cond1), M_if(branch2, cond2) ->
          Compare.pair Bool.compare compare_expr
            (branch1, cond1) (branch2, cond2)
        | _ ->
          next m1 m2
      );
    marker_name = (fun next -> function
        | M_if _ -> "if"
        | m -> next m
      );
  }

When executing an S_if statement, and before executing a branch, it executes the statement S_add_marker:

    | S_if(cond, s1, s2) ->
      assume cond man flow
        ~fthen:(fun flow ->
            man.exec (mk_add_marker (M_if(true, cond)) stmt.srange) flow >>%
            man.exec s1)
        ~felse:(fun flow ->
            man.exec (mk_add_marker (M_if(false, cond)) stmt.srange) flow >>%
            man.exec s2)
      |> OptionExt.return

This statement is handled by the partitioning combiner. It calls the function P.add of the partitioning domain that can change the partitioning key if necessary.

An example is given in the TailMarkers partitioning domain. This domain keeps the last k markers of the traces, where k is parameter set with the option -tail-markers. The type of this domain is:

type t = marker list

and the function add is as follows:

let add marker p =
  (* No marker is preserved *)
  if !opt_max_length = 0 then [] else
  (* Limit not reached => add the marker *)
  if List.length p < !opt_max_length then
    marker :: p
  (* Limit reached => remove the oldest marker and add the new one *)
  else
    marker :: (List.rev p |> List.tl |> List.rev)

Markers have names, that can be used in the option -marker <name1> -marker <name2> to enable the selected markers. By default, all markers are enables. Currently, there are three markers:

1. if for the branches of the S_if statement.
2. switch for the cases of the S_c_switch statement.
3. stub-case for the cases of stubs.

State Partitioning

An example of state partitioning is given in the IntVar partitioning domain. This domain partition the states w.r.t. to the values of a numeric variable. The numeric variable is set with the option -state-partition-int-var <var>:<value1>,<value2>,....

The type of the domain is:

type t = v option (* None is used when the variable is not in the environment *)
and  v =
  | Equal of Z.t  (* The variable is equal to this value *)
  | Other         (* The variable has a value outside of the partitioning set *)

This domain doesn't use markers since it is a state abstraction. Instead, it defines an exec function for tracking variable addition/removal and modification. Consider the case of assignment, which is handled by the function exec_and_partitiong:

let exec_and_partition stmt v man flow =
  (* Execute the statement in the underlying domain *)
  man.exec stmt flow ~route:(Below name) >>% fun flow ->
  let range = stmt.srange in
  let var = mk_var v range in
  (* Get environments where the variable [v] is equal to one of the target values *)
  let eq_cases =
    !opt_target_values |> List.fold_left
      (fun acc n ->
         (* Condition: v = target *)
         let cond = eq var (mk_z n range) range in
         (* New partition *)
         let p' = Some (Equal n) in
         let post =
           man.exec (mk_assume cond range) flow >>% fun flow ->
           set_env T_cur p' man flow
         in
         if sat man post then post :: acc else acc
      ) []
  in
  (* Get environments where the variable [v] is not equal to any of the target values *)
  let ne_case =
    (* Construct the conjunction [v != v1 and v != v2 and ...] *)
    let cond =
      !opt_target_values |> List.tl |> List.fold_left
        (fun acc n ->
           log_and acc (ne var (mk_z n range) range) range
        ) (ne (mk_var v range) (mk_z (List.hd !opt_target_values) range) range)
    in
    (* New partition *)
    let p' = Some Other in
    let post =
      man.exec (mk_assume cond range) flow >>% fun flow ->
      set_env T_cur p' man flow
    in
    if sat man post then [post] else []
  in
  Cases.join_list (eq_cases @ ne_case) ~empty:(fun () -> Cases.empty flow)

Note that the manager given to the domain has the type ('a, t) man. It allows the domain to set its partitioning key, like classic domains set their abstract element.

Results

Below are some benchmarks comparing master on Coreutils and Juliet.

Benchmark

Cell+Interval

Cell+Interval+StringLength

Cell+Interval+StringLength+PackRelation

Tail=0

Tail=1

Tail=2

Tail=1

Tail=2

Tail=1

Tail=2

Time

Alarms

Assumptions

Time

Alarms

Assumptions

Time

Alarms

Assumptions

Time

Alarms

Assumptions

Time

Alarms

Assumptions

Time

Alarms

Assumptions

Time

Alarms

Assumptions

Coreutils

+1s

0

0

+5s

+17/-113

-18

+25s

+19/-133

-22

+10s

+18/-107

-18

+50s

+20/-121

-22

+30s

+26/-96

-18

+148s

+20/-124

-22

Juliet

+0.148s

+0/-2029

-0

+0.150s

+0/-2047

-0

Breaking Changes

Effects

Effects trees can't be used for partitioning, because they are represented as binary trees (which was sufficient previously as all combiners are binary). This MR uses Effects maps instead, which are maps from domains paths to effects. A domain path is a list of domain accessors, which are extensible types defined by combiners to identify their arguments.

For example, binary combiners (such as compose and switch) use left and right accessors. The partitioning domain use partition(p), where p is a partitioning key.

Environment accessors

A domain under a partitioning abstraction can no longer use man.get : 'a -> t to get its abstract element, because it can have several ones. The new accessors use cases to solve this problem:

type ('a, 't) man = {
  ...
  
  get : token -> 'a flow -> ('a, 't) cases;  
  set : token -> 't -> 'a flow -> 'a post;
}

So, to get its abstract element, a domain needs to call:

man.get T_cur flow >>$ fun a flow ->
...

instead of:

let a = man.get cur in
...

Initialization

Because man.set returns now an 'a post value, the signature of the init function has been changed to:

val init : program -> ('a, t) man -> 'a flow -> 'a post option

instead of:

val init : program -> ('a, t) man -> 'a flow -> 'a flow