Staging
v0.8.1
v0.8.1
sse_options.ml
(**************************************************************************)
(* This file is part of BINSEC. *)
(* *)
(* Copyright (C) 2016-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
include Cli.Make (struct
let shortname = "sse"
let name = "Static Symbolic Execution"
end)
module MaxDepth = Builder.Integer (struct
let name = "depth"
let default = 1000
let doc = "Set exploration maximal depth"
end)
module JumpEnumDepth = Builder.Integer (struct
let name = "jump-enum"
let default = 3
let doc = "Set maximum number of jump targets to retrieve for dynamic jumps"
end)
module KeepGoing = Builder.False (struct
let name = "keep-going"
let doc = "Ignore errors returned by the SMT solver. Default is to abort."
end)
module Randomize = Builder.False (struct
let name = "randomize"
let doc = "randomize path selection"
end)
module SMT_dir = Builder.String_option (struct
let name = "smt-dir"
let doc = "set directory to cache smt scripts"
end)
module AddressTraceFile = Builder.String_option (struct
let name = "address-trace-file"
let doc = "set file for adress trace export"
end)
module AvoidAddresses = Builder.String_set (struct
let name = "no-explore"
let doc = "set addresses where sse should stop"
end)
module GoalAddresses = Builder.String_set (struct
let name = "explore"
let doc = "set addresses where sse should try to go"
end)
module LoadSections = Builder.String_set (struct
let name = "load-sections"
let doc = "Sections to load in initial memory (may be overridden by -memory)"
end)
module LoadROSections = Builder.False (struct
let name = "load-ro-sections"
let doc =
"Load the content of all read-only sections (see also -sse-load-sections)"
end)
module MemoryFile = Builder.String_option (struct
let name = "memory"
let doc = "set file containing the initial (concrete) memory state"
end)
module ScriptFiles = Builder.String_list (struct
let name = "script"
let doc = "set file containing initializations, directives and stubs"
end)
module Comment = Builder.False (struct
let name = "comment"
let doc =
"Add comments indicating the origin of the formulas in generated scripts"
end)
module Timeout = Builder.Float (struct
let name = "timeout"
let doc = "Sets a timeout for symbolic execution"
let default = infinity
end)
module Address_counter = struct
type t = { address : Virtual_address.t; counter : int }
let of_string s =
match String.split_on_char ':' s with
| [ address; counter ] ->
{
address = Virtual_address.of_string address;
counter = int_of_string counter;
}
| _ -> assert false
let decr c = { c with counter = c.counter - 1 }
let check_and_decr c = if c.counter > 0 then Some (decr c) else None
end
module Visit_address_counter = Builder.Variant_list (struct
include Address_counter
let name = "visit-until"
let doc =
"Specify a the maximum number of times [n] an address [vaddr] is visited \
by SE (format: <vaddr>:<n>)"
end)
type search_heuristics = Dfs | Bfs | Nurs
module Search_heuristics = Builder.Variant_choice_assoc (struct
type t = search_heuristics
let name = "heuristics"
let doc = "Use the following search heuristics"
let default = Dfs
let assoc_map = [ ("dfs", Dfs); ("bfs", Bfs); ("nurs", Nurs) ]
end)
module Solver_call_frequency = Builder.Integer (struct
let name = "solver-call-frequency"
let default = 1
let doc = "Call the solver every <n> times"
end)
module Seed = Builder.Integer_option (struct
let name = "seed"
let doc = "Give a specific seed for random number generators"
end)
module Directives = Builder.Any (struct
type t = Directive.t list
let name = "directives"
let doc = "Set SSE directive"
let default = []
let to_string _ = "no directives"
let of_string s =
let lexbuf = Lexing.from_string s in
Parser.directives Lexer.token lexbuf
end)
module Dot_filename_out = Builder.String_option (struct
let name = "cfg-o"
let doc = "Output CFG in this file"
end)
module SMT_log_directory = Builder.String (struct
let name = "smt-dump-dir"
let doc = "Set directory where unsolved SMT scripts are dumped"
let default = "binsec_smtdump"
end)