fixes and improves label handling in the IR theory (#1333)

For the context, since the Ghidra PR the semantics of the [blk]
operation in Core Theory was refined and corresponding theories were
updated. Before #1326 all theories were just ignoring the labels
passed to the [blk] operator. The reason for that was that the [blk]
operation serves two purposes. It enables concatenation of data and
control flow effects. And it attaches a label to that sequence so that
it could be referenced elsewhere. Before #1326 it was only used for
the first purpose, i.e., to merge data and control effects into the
single effect. But for Ghidra we needed an ability to create
labels (as ghidra is relying on Branch/Cbranch) instructions
everywhere, even to express the intra-instruction logic, not real
control flow.

Now, the theories have to take into account the label passed to the
blk operation, when they produce their denotations, unless the label is
`Label.null`. If the label is `Label.null` then the operation is
denotes just a sequence of data and control flow effects. Moreover,
denotations are allowed to coalesce several blocks together. But if
the label is non-null then the denotation has to preserve it.

Before this PR the BIR theory wasn't fully respecting the passed
labels and was sometimes optimizing them away, for example, when the
label was attached to an empty denotation. This PR takes care of
keeping the passed labels and at the same time preserving the minimal
form of the generated IR. Of course assuming that lifters are using
the `blk` operation correctly, i.e., that they are not passing
non-null labels to blocks that they do not plan to invoke later.

In other words, if you have a lifter that uses the `blk` operation you
need to update it and pass `Theory.Label.null` there instead of the
fresh label. This will have the same semantics as it had
before. Passing non-null label now has a different semantics.

Author: ivg

lib/bap_core_theory/bap_core_theory.mli

@@ -2373,7 +2373,18 @@ module Theory : sig
     (** [seq x y] performs effect [x], after that perform effect [y].  *)
     val seq : 'a eff -> 'a eff -> 'a eff
 
-    (** [blk lbl data ctrl] a labeled sequence of effects. *)
+    (** [blk lbl data ctrl] an optionally labeled sequence of effects.
+
+        If [lbl] is [Label.null] then the block is unlabeled. If it is
+        not [Label.null] then the denotations will preserve the label
+        and assume that this [blk] is referenced from some other
+        blocks.
+
+        @since 2.4.0 the [blk] operator accepts (and welcomes)
+        [Label.null] as the label in cases when the block is not
+        really expected to be called from anywhere else.
+
+    *)
     val blk : label -> data eff -> ctrl eff -> unit eff
 
 

plugins/bil/bil_ir.ml

@@ -6,11 +6,13 @@ open Bap_knowledge
 open Bap_core_theory
 
 open Knowledge.Syntax
+open KB.Let
 
 include Self()
 
 type blk = {
   name : Theory.Label.t;
+  keep : bool;
   defs : def term list;
   jmps : jmp term list;
 } [@@deriving bin_io]
@@ -74,18 +76,6 @@ let pp_cfg ppf ir =
 
 let inspect cfg = Sexp.Atom (asprintf "%a" pp_cfg cfg)
 
-let relink label {entry; blks} =
-  if is_null entry then {
-    entry = label;
-    blks = [{name=label; defs=[]; jmps=[]}]
-  } else {
-    entry = label;
-    blks = List.map blks ~f:(fun blk ->
-        if Theory.Label.equal blk.name entry then {
-          blk with name = entry;
-        } else blk)
-  }
-
 let domain = KB.Domain.flat ~inspect "graph"
     ~empty:{entry=null; blks=[]}
     ~equal:(fun x y -> Theory.Label.equal x.entry y.entry)
@@ -102,10 +92,21 @@ let graph =
 
 let slot = graph
 
+
+(*
+   Invariants:
+   1. all non-empty denotations have a non-empty list of blocks
+   1.1 is_null entry <=> (blks = [])
+   2. if the denotation is non-empty then the list of blocks
+      has a block with the name equal to entry.
+   3. explicitly labeled blocks keep their names.
+
+
+  *)
 module IR = struct
   include Theory.Empty
   let ret = Knowledge.return
-  let blk tid = {name=tid; defs=[]; jmps=[]}
+  let blk ?(keep=true) tid = {name=tid; defs=[]; jmps=[]; keep}
 
   let def = (fun x -> x.defs), (fun x d -> {x with defs = d})
   let jmp = (fun x -> x.jmps), (fun x d -> match x.jmps with
@@ -135,9 +136,36 @@ module IR = struct
   let data cfg = ret cfg
   let ctrl cfg = ret cfg
 
-  let set v x =
+  let target =
     KB.Object.scoped Theory.Program.cls @@ fun lbl ->
-    Theory.Label.target lbl >>= fun t ->
+    Theory.Label.target lbl
+
+
+  let goto ?(is_call=false) ?cnd ~tid dst =
+    if is_call
+    then Jmp.reify ?cnd ~tid ~alt:(Jmp.resolved dst) ()
+    else Jmp.reify ?cnd ~tid ~dst:(Jmp.resolved dst) ()
+
+  let relink label {entry; blks} =
+    if is_null entry then KB.return {
+        entry = label;
+        blks = [{name=label; keep=true; defs=[]; jmps=[]}]
+      } else
+      let+ blks = List.fold_map blks ~init:`Unbound ~f:(fun r blk ->
+          if Theory.Label.equal blk.name entry
+          then if blk.keep then `Relink blk.name, blk
+            else `Relinked, {blk with name = label; keep=true}
+          else r,blk) |> function
+                  | `Relinked,blks -> KB.return blks
+                  | `Relink dst, blks ->
+                    let+ tid = fresh in
+                    blks @ [blk label ++ goto ~tid dst]
+                  | `Unbound,[] -> assert false
+                  | `Unbound,_ -> assert false      in
+      {entry = label; blks}
+
+  let set v x =
+    target >>= fun t ->
     if Theory.Target.has_roles t [Theory.Role.Register.constant] v
     then !!empty
     else
@@ -146,14 +174,14 @@ module IR = struct
       fresh >>= fun tid ->
       data {
         entry;
-        blks = [{name=entry; jmps=[]; defs=[Def.reify ~tid v x]}]
+        blks = [{
+            name=entry;
+            keep=false;
+            jmps=[];
+            defs=[Def.reify ~tid v x]
+          }]
       }
 
-  let goto ?(is_call=false) ?cnd ~tid dst =
-    if is_call
-    then Jmp.reify ?cnd ~tid ~alt:(Jmp.resolved dst) ()
-    else Jmp.reify ?cnd ~tid ~dst:(Jmp.resolved dst) ()
-
   (** reifies a [while (<cnd>) <body>] loop to
 
       {v
@@ -177,13 +205,14 @@ module IR = struct
   let repeat cnd body =
     cnd >>= fun cnd ->
     body >>| reify >>= function
-    | {blks=[]} ->
+    | {blks=[]} ->               (* empty denotation *)
       fresh >>= fun head ->
       fresh >>= fun tid ->
       data {
         entry = head;
         blks = [{
             name = head;
+            keep = true;
             defs = [];
             jmps = [goto ~cnd ~tid head]}]}
     | {entry=loop; blks=b::blks} ->
@@ -273,28 +302,28 @@ module IR = struct
     fresh >>= fun tid ->
     ctrl {
       entry;
-      blks = [blk entry ++ Jmp.reify ~tid ~dst:(Jmp.indirect dst) ()]
+      blks = [blk ~keep:false entry ++ Jmp.reify ~tid ~dst:(Jmp.indirect dst) ()]
     }
 
   let appgraphs fst snd =
     if is_empty fst then ret snd else
     if is_empty snd then ret fst
     else match fst, snd with
       | _,{blks=[]} | {blks=[]}, _ -> assert false
-      | {entry; blks={jmps=[]} as x :: xs},{blks=[y]} -> ret {
+      | {entry; blks={jmps=[]} as x :: xs},{blks=[{keep=false} as y]} ->
+        ret {
           entry;
           blks = {x with defs = y.defs @ x.defs; jmps = y.jmps} :: xs
         }
-      | {entry; blks=x::xs}, {entry=snd; blks=y::ys} ->
+      | {entry; blks=x::xs}, {entry=esnd; blks=y::ys} ->
         fresh >>= fun tid -> ret {
           entry;
           blks =
             y ::
-            x ++ goto ~tid snd ::
+            x ++ goto ~tid esnd ::
             List.rev_append xs ys
         }
 
-
   let seq fst snd =
     fst >>-> fun fst ->
     snd >>-> fun snd ->
@@ -306,16 +335,15 @@ module IR = struct
     KB.collect Theory.Label.is_subroutine dst >>= fun is_call ->
     ctrl {
       entry;
-      blks = [blk entry ++ goto ?is_call ~tid dst]
+      blks = [blk ~keep:false entry ++ goto ?is_call ~tid dst]
     }
 
   let blk label defs jmps =
     defs >>-> fun defs ->
     jmps >>-> fun jmps ->
     appgraphs defs jmps >>-> fun res ->
-    ret @@
-    if is_null label then res
-    else relink label res
+    if is_null label then ret res
+    else relink label res >>= ret
 
   let goto = do_goto
 end