Short circuit when functions are syntactically equal #259

DieracDelta · 2020-10-28T19:51:19Z

This PR adds in a check for syntactic equality (enabled with --syntax-equality ). Example usage may be seen in run_wp_*.sh scripts in the syntax_equality test folder. This PR closes #211, and is a first step towards the ideas in #254. Specifically,
equality.ml exports an exist_isomorphism function. This function checks if there's a mapping between the two sub.t functions that preserves syntax structure, use of virtual variables (virtual variables may go by different names but must be used in all the same places), and control flow.

I've documented the code in equality.ml and equality.mli. I'm also including the results I posted to the slack for the run on grammatech. On average, only running the syntax check takes 8 seconds on my laptop. I found 65 syntactically equal functions on grammatech. When running CBAT, I got:

On the master branch cbat without any special flags: 36 SATS, 3 UNKNOWN, 26 UNSAT
On the master branch cbat with mem-offset and pointer flag on all registers: 0 SAT, 7 UNKNOWN, and 58 UNSAT

So overall, the results that CBAT finishes within the timeout of 1000s turn out to match with this syntax check. It's not clear to me how to test the UNKNOWNs further.

This first plot is function (on the x axis) vs # syntactically idental blocks / total blocks in the sub. These are encouraging numbers performance improvements in #254 .

This second plot is time in seconds on the x axis vs # statements (def_t, jmp_t) on the y axis. The green dots are the run for syntactically equal functions (of which there are 65); the red dots are master branch cbat without any special flags. @philzook58 mentioned that this is big savings if there are a lot of long functions that are syntactically identical in the binary.

philzook58 · 2020-11-04T20:50:28Z

We may want equality.ml in bap_wp not plugin.

philzook58 · 2020-11-04T20:51:18Z

wp/plugin/lib/equality.ml

+(* some of these pattern matchings are massive; we don't want fragile warnings *)
+[@@@warning "-4"]
+
+module H = Bap.Std.Graphs.Ir


Is there a logic to these names? What is H? Maybe Ir would be a better choice if it doesn't clash with anything

hmm not really. I'll swap it out for something a bit more descriptive (Ir if I can).

You can, I think module names shadow in OCaml (sometimes you need to be careful).

philzook58 · 2020-11-04T20:52:02Z

wp/plugin/lib/equality.ml

+module BFS = Graph.Traverse.Bfs (J)
+module TidSet = Tid.Set
+
+module TidMap = Tid.Map


Stylistically, I don't think you're saving much with these shorthands.

philzook58 · 2020-11-04T20:57:01Z

wp/plugin/lib/equality.ml

+type varToVarMap = Var.t VarMap.t
+
+(* Replaces the real variables with indices with only their base *)
+let rec strip_indices (e : Exp.t) : Exp.t =


I think this could be expressed more succinctly using the mapper interface. I think this is mapping Var.base over Var constructors and that's it? http://binaryanalysisplatform.github.io/bap/api/odoc/bap/Bap/Std/Exp/class-mapper/index.html

philzook58 · 2020-11-04T21:07:16Z

wp/plugin/lib/equality.ml

+    (cfg2 : Bap.Std.Graphs.Ir.t) : ((blk term) TidMap.t) * ((blk term) TidMap.t) =
+  let acc = fun ele tid_map ->
+    let tid = Term.tid (get_label ele) in
+    TidMap.change tid_map tid ~f:(fun _ -> Some (get_label ele)) in


http://binaryanalysisplatform.github.io/bap/api/odoc/bap/Bap/Std/Tid/Map/index.html#val-update TidMap.update seems more appropriate

philzook58 · 2020-11-04T21:12:28Z

wp/plugin/lib/equality.mli

+     constructed block mapping must match the corresponding TIDS
+     in the same respective jmp_t in sub2.
+*)
+val exist_isomorphism : Sub.t -> Sub.t -> bool


Something to consider, I can see it either way. Since you find an isomorphism, it seems it might be useful to expose it via returning iso option rather than bool

Also: why isn't exists? Or even better, get_iso?

philzook58 · 2020-11-04T21:15:17Z

wp/plugin/lib/equality.ml

+
+(* Iterate through all reachable nodes in each cfg
+ *  and generate a map from tid to blk.*)
+let get_node_maps


Since the two cfgs and maps are built entirely independently, couldn't one make a get_node_map : Ir.t -> blk TidMap.t function that you call twice instead?

philzook58 · 2020-11-04T21:24:30Z

wp/plugin/lib/equality.ml

+module VarSet = Var.Set
+module TidTupleMap = Map.Make(struct type t = Tid.t * Tid.t [@@deriving sexp, compare] end)
+
+type varToVarMap = Var.t VarMap.t


I would prefer you not define this type synonym. Var.t VarMap.t is clearer and more self explanatory than varToVarMap

(also, var is an alias to Var.t if that helps)

philzook58 · 2020-11-04T21:27:54Z

wp/plugin/lib/equality.ml

+   a map from (tid_blk_sub1, tid_blk_sub2) to the mapping between variables
+   used in those subs. *)
+let compare_blocks (sub1: Sub.t) (sub2 : Sub.t) :
+  (TidSet.t TidMap.t) * (varToVarMap TidTupleMap.t) =


I have a suspicion that it would be better to use ((Var.t Var.Map.t) Tid.Map.t) Tid.Map.t rather than varToVarMap TidTupleMap.t. Essentially, currying the tid keys in that dictionary

philzook58 · 2020-11-04T21:31:37Z

wp/plugin/lib/equality.ml

+  let blk_varmap = TidTupleMap.empty in
+  let evaluator = (fun (node1 : Bap.Std.Graphs.Ir.Node.t) (blk_map, blk_varmap) ->
+      let blk1 = get_label node1 in
+      let tid1 = Term.tid (get_label node1) in


could be blk1 instead of repeating (get_label node1)

DieracDelta · 2020-11-06T15:20:52Z

Thanks for the suggestions! I've made corresponding changes.

I agree--returning the mapping allows for more flexibility. I think the currying suggestion is clever--it makes exposing functions with aliased types easier to include in the mli file. Specifically, this lets me also expose compare_blocks_syntax. This function returns the syntactically equal (up to TID) blocks. Seems useful for #254 .

This mapper interface is awesome. I'm wondering if there's an easy way to use it to rewrite sub_exp in a cleaner fashion that doesn't involve fragile pattern matching. The issue is we need to carry around the information from both subs at the same time, and return something different if the subs don't match. This creates differing type signatures for the declared functions.

Also, I'm making liberal use of >>= and >>|. I could use let syntax instead if that's clearer. Seems like the let syntax is used in bildb, but the inline operators are used in wp. I'm not sure what's preferred here.

I'm testing the changes by running them on grammatech. I'll post again when I've got results. EDIT: has the same behavior as before (marks 65 of the functions as syntactically equal).

codyroux · 2020-11-06T22:40:52Z

There's no real norm between using monadic lets and >>=s, though Ivan prefers the latter, and his opinion has some weight.

Apparently, using the ppx versions of let bindings is deprecated, instead using the (newish) feature that allows defining new let-like keywords.

I'd suggest just using the combinators for now.

philzook58 · 2020-11-11T20:06:25Z

wp/lib/bap_wp/src/equality.ml

+           | None ->
+             blk_map, blk_varmap) in
+      let blk_map, blk_varmap = BFS.fold inner_evaluator (blk_map, blk_varmap) cfg2 in
+      blk_map, blk_varmap) in


Put this tuple in parens

philzook58 · 2020-11-11T20:11:20Z

wp/lib/bap_wp/src/equality.ml

+(* Compares everything about a block EXCEPT tids, which will be done later. *)
+let compare_block (blk1 : blk term) (blk2 : blk term) map =
+  compare_defs (Term.enum def_t blk1 |> Sequence.to_list)
+    (Term.enum def_t blk2 |> Sequence.to_list) map >>=


Do we need to convert to lists?

philzook58 · 2020-11-11T20:27:44Z

wp/lib/bap_wp/src/equality.ml

+(* Maps all virtual variables from e1 to their analagous variable within vmap;
+   if a variable not in vmap, is added to vmap from e2.
+   Returns None if cannot map variables because subs do not match in structure *)
+let rec sub_exp (vmap : Var.t Var.Map.t)


I'd separate this out into two functions. One that performs substitution and one that compare_exp

philzook58 · 2020-11-11T20:33:23Z

wp/lib/bap_wp/src/equality.ml

+  let cfg1, cfg2 = Sub.to_cfg sub1, Sub.to_cfg sub2 in
+  let tid_to_blk1, tid_to_blk2 = get_node_map cfg1, get_node_map cfg2 in
+  let tid_map, var_maps = compare_blocks_syntax sub1 sub2 in
+  let used_set = Tid.Set.empty in


Move into get_isomorphism

philzook58 · 2020-11-11T20:45:14Z

wp/lib/bap_wp/src/equality.ml

+    (tid_to_blk1 : (blk term) Tid.Map.t) (tid_to_blk2 : (blk term) Tid.Map.t)
+    (var_maps : ((Var.t Var.Map.t) Tid.Map.t) Tid.Map.t) (merged_map : Var.t Var.Map.t) :
+  (Tid.t Tid.Map.t) option  =
+  let node = List.hd node_stack in


This is a fold over the node_list I think

DieracDelta requested a review from philzook58 October 28, 2020 19:52

DieracDelta added 7 commits October 28, 2020 15:54

start of syntactic equality test

8b24d4e

refactoring

1222a09

Working complete syntax comparison

b306dc3

Added flag and map comparison.

ec9c3c0

Added documentation

e1454cd

Added tests and more types

28be67a

Rebasing onto master

6eb4132

DieracDelta force-pushed the jrestivo/syntactic_equality branch from 1885f01 to 6eb4132 Compare October 28, 2020 20:00

DieracDelta requested a review from fortunac October 28, 2020 20:03

philzook58 reviewed Nov 4, 2020

View reviewed changes

Phil's suggested improvements

6ddaedc

Some refactoring

89036ab

philzook58 reviewed Nov 11, 2020

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Short circuit when functions are syntactically equal #259

Short circuit when functions are syntactically equal #259

DieracDelta commented Oct 28, 2020

philzook58 commented Nov 4, 2020

philzook58 Nov 4, 2020 •

edited

Loading

DieracDelta Nov 4, 2020

codyroux Nov 6, 2020

philzook58 Nov 4, 2020

philzook58 Nov 4, 2020 •

edited

Loading

philzook58 Nov 4, 2020

philzook58 Nov 4, 2020

codyroux Nov 6, 2020

philzook58 Nov 4, 2020

philzook58 Nov 4, 2020

codyroux Aug 6, 2021

philzook58 Nov 4, 2020

codyroux Nov 6, 2020

philzook58 Nov 4, 2020

DieracDelta commented Nov 6, 2020 •

edited

Loading

codyroux commented Nov 6, 2020

philzook58 Nov 11, 2020

philzook58 Nov 11, 2020

philzook58 Nov 11, 2020

philzook58 Nov 11, 2020

philzook58 Nov 11, 2020

Short circuit when functions are syntactically equal #259

Are you sure you want to change the base?

Short circuit when functions are syntactically equal #259

Conversation

DieracDelta commented Oct 28, 2020

philzook58 commented Nov 4, 2020

philzook58 Nov 4, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

philzook58 Nov 4, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

DieracDelta commented Nov 6, 2020 • edited Loading

codyroux commented Nov 6, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

philzook58 Nov 4, 2020 •

edited

Loading

philzook58 Nov 4, 2020 •

edited

Loading

DieracDelta commented Nov 6, 2020 •

edited

Loading