Short circuit when functions are syntactically equal

wp/lib/bap_wp/src/equality.mli

@@ -0,0 +1,38 @@
+open Bap.Std
+
+(* Checks for exact syntactic equality between the provided Sub.t arguments.
+    It returns the map (if it exists) from the block level tids in the first
+    sub to the second sub.
+   This means that there must exist an block-level mapping
+    between the blocks in sub 1 and
+    in sub 2 such that syntax matches. Syntax includes several things:
+   - the base of physical variable names
+   - structure including control flow and phi terms (of which there should be none)
+   - the usage of variables in the subs must match. E.g. if I have in sub 1:
+        #45 := RBP
+        mem := mem with [RSP, el]:u64 <- #45
+     and
+        #88 := RBP
+        mem := mem with [RSP, el]:u64 <- #88
+     Then these two blocks (and the entire sub.ts if they were to consist only of this)
+     would match. However, if instead we had something like:
+        #45 := RBP
+        mem := mem with [RSP, el]:u64 <- #45
+     and
+        #88 := RBP
+        mem := mem with [RSP, el]:u64 <- #90
+     then the blocks would not be syntactically equal since #45 would be expected
+     in the spot that #90 is taking.
+   - The block TIDs mentioned within jmp_ts in sub1 when run through the
+     constructed block mapping must match the corresponding TIDS
+     in the same respective jmp_t in sub2.
+*)
+val subs_to_isomorphism : Sub.t -> Sub.t -> (Tid.t Tid.Map.t) option
+
+(* Compares a sub to another sub; returns a map from tid into sub1
+   to the set of sub2 tids that are syntactically equal to in structure,
+    variables, and syntax. Does NOT check that jmp target TIDs match. Also returns
+   a map from (tid_blk_sub1, tid_blk_sub2) to the mapping between variables
+   that must be equivalent used in those subs. *)
+val compare_blocks_syntax : Sub.t -> Sub.t -> (Tid.Set.t Tid.Map.t) *
+                                              (((Var.t Var.Map.t) Tid.Map.t) Tid.Map.t)

wp/plugin/lib/analysis.ml

@@ -19,6 +19,7 @@ open Parameters
 
 include Self()
 
+module Eq = Equality
 module Comp = Compare
 module Pre = Precondition
 module Env = Environment
@@ -258,6 +259,22 @@ let single (bap_ctx : ctxt) (z3_ctx : Z3.context) (var_gen : Env.var_gen)
     Printf.printf "\nSub:\n%s\n%!" (Sub.to_string main_sub);
   { pre = pre; orig = env, main_sub; modif = env, main_sub }
 
+let check_syntax_equality (bap_ctx : ctxt)
+    (p : Params.t) (file1 : string) (file2 : string) : bool =
+  if p.syntax_equality then
+    let prog1, _ = Utils.read_program bap_ctx
+        ~loader:Utils.loader ~filepath:file1 in
+    let prog2, _ = Utils.read_program bap_ctx
+        ~loader:Utils.loader ~filepath:file2 in
+    let subs1 = Term.enum sub_t prog1 in
+    let subs2 = Term.enum sub_t prog2 in
+    let main_sub1 = Utils.find_func_err subs1 p.func in
+    let main_sub2 = Utils.find_func_err subs2 p.func in
+    match Eq.subs_to_isomorphism main_sub1 main_sub2 with
+    | Some _iso -> true
+    | None -> false
+  else false
+
 (* Runs a comparative analysis. *)
 let comparative (bap_ctx : ctxt) (z3_ctx : Z3.context) (var_gen : Env.var_gen)
     (p : Params.t) (file1 : string) (file2 : string) : combined_pre =
@@ -358,8 +375,12 @@ let run (p : Params.t) (files : string list) (bap_ctx : ctxt)
     single bap_ctx z3_ctx var_gen p file
     |> check_pre p z3_ctx
   | [file1; file2] ->
-    comparative bap_ctx z3_ctx var_gen p file1 file2
-    |> check_pre p z3_ctx
+    begin
+      match check_syntax_equality bap_ctx p file1 file2 with
+      | false ->
+        comparative bap_ctx z3_ctx var_gen p file1 file2 |> check_pre p z3_ctx
+      | true -> Ok ()
+    end
   | _ ->
     let err =
       Printf.sprintf "WP can only analyze one binary for a single analysis or \

wp/plugin/lib/parameters.ml

@@ -47,7 +47,8 @@ type t = {
   debug : string list;
   stack_base : int option;
   stack_size : int option;
-  show : string list
+  syntax_equality : bool;
+  show : string list;
 }
 
 (* Ensures the user inputted a function for analysis. *)

wp/plugin/lib/parameters.mli

@@ -50,7 +50,8 @@ type t = {
   debug : string list;
   stack_base : int option;
   stack_size : int option;
-  show : string list
+  syntax_equality : bool;
+  show : string list;
 }
 
 (** [validate flags files] ensures the user inputted the appropriate flags for

wp/plugin/tests/unit/test_wp_unit.ml

@@ -212,4 +212,12 @@ let unit_tests = [
     ~script:"run_wp_assume_unsat.sh";
   "Verifier nondent"               >: test_plugin "verifier_calls" sat
     ~script:"run_wp_nondet.sh";
+
+  "Syntactic equality: unequal"
+  >: test_plugin "syntax_equality" sat ~script:"run_wp_sat.sh";
+  "Syntactic equality: equal 1"
+  >: test_plugin "syntax_equality" unsat ~script:"run_wp_unsat_1.sh";
+  "Syntactic equality: equal 2"
+  >: test_plugin "syntax_equality" unsat ~script:"run_wp_unsat_2.sh";
+
 ]

wp/plugin/wp.ml

@@ -180,6 +180,13 @@ let stack_size = Cmd.parameter Typ.(some int) "stack-size"
     ~doc:{|Sets the size of the stack, which should be denoted in bytes. By
            default, the size of the stack is 0x800000 which is 8MB.|}
 
+let syntax_equality = Cmd.flag "syntax-equality"
+    ~doc:{| Short-circuits WP and returns UNSAT if the functions
+           are syntactically equal. Use with caution; the comparison must
+           be testing for function equality in the same sense as syntactic
+           equality. This is currently found with the mem_offset flag and
+           pointer flag enabled. Only applicable in the comparative case. |}
+
 let grammar = Cmd.(
     args
     $ func
@@ -200,6 +207,7 @@ let grammar = Cmd.(
     $ show
     $ stack_base
     $ stack_size
+    $ syntax_equality
     $ files)
 
 (* The callback run when the command is invoked from the command line. *)
@@ -222,6 +230,7 @@ let callback
     (show : string list)
     (stack_base : int option)
     (stack_size : int option)
+    (syntax_equality : bool)
     (files : string list)
     (ctxt : ctxt) =
   let params = Parameters.({
@@ -242,7 +251,8 @@ let callback
       debug = debug;
       show = show;
       stack_base = stack_base;
-      stack_size = stack_size
+      stack_size = stack_size;
+      syntax_equality = syntax_equality;
     })
   in
   Parameters.validate params files >>= fun () ->

wp/resources/sample_binaries/syntax_equality/Makefile

@@ -0,0 +1,11 @@
+BASE=main
+PROG_1=$(BASE)_1
+PROG_2=$(BASE)_2
+
+all: $(PROG_1) $(PROG_2)
+
+%: %.c
+	$(CC) -Wall -g -o $@ $<
+
+clean:
+	rm -f $(PROG_1) $(PROG_2)

wp/resources/sample_binaries/syntax_equality/main_1.c

@@ -0,0 +1,11 @@
+int deref(int *num_1) {
+    int num_2 = 12;
+    if(*num_1 > num_2){
+        return -2;
+    }
+    return 0;
+}
+
+int main(int argc, char** argv){
+        return 0;
+}

wp/resources/sample_binaries/syntax_equality/main_2.c

@@ -0,0 +1,11 @@
+int deref(int *num_1) {
+    int num_2 = 12;
+    if(*num_1 > num_2){
+        return -1;
+    }
+    return 0;
+}
+
+int main(int argc, char** argv){
+        return 0;
+}

wp/resources/sample_binaries/syntax_equality/run_wp_sat.sh

@@ -0,0 +1,18 @@
+# This tests that main_1 and main_2 are not syntactically equal to each other
+
+# Should return SAT
+
+set -x
+
+run_unsat () {
+  bap wp \
+    --func=deref \
+    --num-unroll=0 \
+    --no-byteweight \
+    --mem-offset \
+    --syntax-equality \
+    --compare-post-reg-values=R12,R13,R14,R15,RBX,RSP,RBP,RAX \
+    -- main_1 main_2
+}
+
+run_unsat

wp/resources/sample_binaries/syntax_equality/run_wp_unsat_1.sh

@@ -0,0 +1,17 @@
+# This tests that main_2 is syntactically equal to itself
+
+# Should return UNSAT
+
+set -x
+
+run_unsat () {
+  bap wp \
+    --func=deref \
+    --num-unroll=0 \
+    --no-byteweight \
+    --mem-offset \
+    --syntax-equality \
+    -- main_1 main_1
+}
+
+run_unsat

wp/resources/sample_binaries/syntax_equality/run_wp_unsat_2.sh

@@ -0,0 +1,17 @@
+# This tests that main_2 is syntactically equal to itself
+
+# Should return UNSAT
+
+set -x
+
+run_unsat () {
+  bap wp \
+    --func=deref \
+    --num-unroll=0 \
+    --no-byteweight \
+    --mem-offset \
+    --syntax-equality \
+    -- main_2 main_2
+}
+
+run_unsat