-
Notifications
You must be signed in to change notification settings - Fork 14
/
output.ml
118 lines (98 loc) · 4.16 KB
/
output.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
(***************************************************************************)
(* *)
(* Copyright (C) 2018/2019 The Charles Stark Draper Laboratory, Inc. *)
(* *)
(* This file is provided under the license found in the LICENSE file in *)
(* the top-level directory of this project. *)
(* *)
(* This work is funded in part by ONR/NAWC Contract N6833518C0107. Its *)
(* content does not necessarily reflect the position or policy of the US *)
(* Government and no official endorsement should be inferred. *)
(* *)
(***************************************************************************)
open !Core_kernel
open Bap.Std
include Self()
module Expr = Z3.Expr
module Arith = Z3.Arithmetic
module BV = Z3.BitVector
module Bool = Z3.Boolean
module Array = Z3.Z3Array
module Env = Environment
module Constr = Constraint
(** Implements {!Model}. *)
open Core_kernel
open Bap.Std
exception NoValue of string
let no_value_msg e m =
let e_str = Z3.Expr.to_string e in
let m_str = Z3.Model.to_string m in
Printf.sprintf "No value for symbol '%s' found in model: %s" e_str m_str
let word_of_str s w =
let w_str = Printf.sprintf "%s:%du" s w in
Word.of_string w_str
let z3_val_of e m =
match Z3.Model.eval m e true with
| Some v -> v
| None -> raise (NoValue (no_value_msg e m))
let word_of_z3_bv bv =
let bits = Z3.BitVector.get_size (Z3.Expr.get_sort bv) in
let s = Z3.Expr.to_string bv in
word_of_str (String.substr_replace_first s ~pattern:"#" ~with_:"0") bits
let val_for_reg r m env =
let reg_var = Var.create r (Type.imm 64) in
let reg_value, _ = Environment.get_var env reg_var in
let v = z3_val_of reg_value m in
word_of_z3_bv v
let strip_final_digits s =
let s' = List.rev (String.to_list s) in
let rec pop_digits l =
match l with
| [] -> l
| x :: xs ->
begin
match x with
| '0' .. '9' -> pop_digits xs
| _ -> l
end
in
let s'' = List.rev (pop_digits s') in
String.of_char_list s''
let reg_names m =
m |>
Z3.Model.get_decls |>
List.map ~f:Z3.FuncDecl.get_name |>
List.map ~f:Z3.Symbol.to_string |>
List.filter ~f:(fun s -> String.is_substring_at s ~pos:0 ~substring:"R") |>
List.map ~f:strip_final_digits
let print_result (solver : Z3.Solver.solver) (status : Z3.Solver.status)
(goals: Constr.t) (ctx : Z3.context) : unit =
match status with
| Z3.Solver.UNSATISFIABLE -> Format.printf "\nUNSAT!\n%!"
| Z3.Solver.UNKNOWN -> Format.printf "\nUNKNOWN!\n%!"
| Z3.Solver.SATISFIABLE ->
Format.printf "\nSAT!\n%!";
let model = Z3.Solver.get_model solver
|> Option.value_exn ?here:None ?error:None ?message:None in
Format.printf "\nModel:\n%s\n%!" (Z3.Model.to_string model);
let refuted_goals = Constr.get_refuted_goals goals solver ctx in
Format.printf "\nRefuted goals:\n%!";
Seq.iter refuted_goals ~f:(fun g ->
Format.printf "%s\n%!" (Constr.refuted_goal_to_string g model))
(** [output_gdb] is similar to [print_result] except chews on the model and outputs a gdb script with a
breakpoint at the subroutine and fills the appropriate registers *)
let output_gdb (solver : Z3.Solver.solver) (status : Z3.Solver.status)
(env : Env.t) ~func:(func : string) ~filename:(gdb_filename : string) : unit =
match status with
| Z3.Solver.SATISFIABLE ->
let model = Z3.Solver.get_model solver
|> Option.value_exn ?here:None ?error:None ?message:None in
let regs = reg_names model in
Out_channel.with_file gdb_filename ~f:(fun t ->
Printf.fprintf t "break *%s\n" func; (* The "*" is necessary to break before some slight setup *)
Printf.fprintf t "start\n";
List.iter regs ~f:(fun r ->
let w = val_for_reg r model env in
let s = Format.asprintf "set $%s = %a \n" (String.lowercase r) Bap.Std.Word.pp_hex w in
Printf.fprintf t "%s" s))
| _ -> ()