Skip to content

Short circuit when functions are syntactically equal #259

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Short circuit when functions are syntactically equal #259

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
8b24d4e
start of syntactic equality test
DieracDelta Oct 21, 2020
1222a09
refactoring
DieracDelta Oct 21, 2020
b306dc3
Working complete syntax comparison
DieracDelta Oct 26, 2020
ec9c3c0
Added flag and map comparison.
DieracDelta Oct 28, 2020
e1454cd
Added documentation
DieracDelta Oct 28, 2020
28be67a
Added tests and more types
DieracDelta Oct 28, 2020
6eb4132
Rebasing onto master
DieracDelta Oct 28, 2020
6ddaedc
Phil's suggested improvements
DieracDelta Nov 6, 2020
89036ab
Some refactoring
DieracDelta Nov 11, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 22 additions & 2 deletions wp/plugin/lib/analysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ open Parameters

include Self()

module Eq = Equality
module Comp = Compare
module Pre = Precondition
module Env = Environment
Expand Down Expand Up @@ -258,6 +259,21 @@ 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 =
(* TODO replace with param flag *)
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
Eq.exist_isomorphism main_sub1 main_sub2
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 =
Expand Down Expand Up @@ -358,8 +374,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 \
Expand Down
Loading