123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169(**************************************************************************)(* This file is part of BINSEC. *)(* *)(* Copyright (C) 2016-2024 *)(* 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). *)(* *)(**************************************************************************)includeCli.Make(structletshortname="sse"letname="Static Symbolic Execution"end)moduleEngine=structtypet=..moduleHtbl=Hashtbl.Make(structtypenonrect=tletequal=(=)lethash=Hashtbl.hashend)letengines=Basic_types.String.Htbl.create4letfactories=Htbl.create4moduleOpt=Builder.Any_opt(structtypenonrect=tletname="engine"letdoc="Use the following symbolic engine"letof_stringname=tryBasic_types.String.Htbl.findenginesnamewithNot_found->ifList.memname(Plugins.Plugins.Plugins.list())then(Plugins.Plugins.Plugins.loadname;Basic_types.String.Htbl.findenginesname)elseraiseNot_foundend)letset=Opt.setletget=Opt.getletis_set=Opt.is_setletis_default=Opt.is_defaultletget_opt=Opt.get_optletregisternameenginefactory=ifBasic_types.String.Htbl.memenginesnamethenLogger.fatal"Engine name %S has already been taken."name;(matchHtbl.findfactoriesenginewith|name',factory'whenfactory!=factory'->Logger.fatal"Trying to overwrite engine %S with %S"name'name|(exceptionNot_found)|_->());Basic_types.String.Htbl.addenginesnameengine;Htbl.addfactoriesengine(name,factory)letget_factory()=matchHtbl.findfactories(get())with|_,f->f()|exceptionNot_found->Logger.fatal"Trying to load an unregistered engine"endmoduleAlternativeEngine=Builder.False(structletname="alternative-engine"letdoc="Enable the experimental engine"end)moduleLegacyEngine=Builder.False(structletname="legacy-engine"letdoc="Use the legacy engine. Some features are not or hardly supported (e.g. \
core dump, custom arrays, etc.)."end)moduleMaxDepth=Builder.Integer(structletname="depth"letdefault=1000letdoc="Set exploration maximal depth"end)moduleTransientEnum=Builder.Integer(structletname="self-written-enum"letdefault=0letdoc="Set maximum number of forks for symbolic instruction opcodes"end)moduleJumpEnumDepth=Builder.Integer(structletname="jump-enum"letdefault=3letdoc="Set maximum number of jump targets to retrieve for dynamic jumps"end)moduleQMerge=Builder.Integer(structletname="qmerge"letdefault=0letdoc="Set maximum look ahead depth for quick merging"end)moduleKillFlagsAtReturn=Builder.No(structletname="kill-flags-at-return"letdoc="Conservatively always consider flags alive at function return"end)moduleRandomize=Builder.False(structletname="randomize"letdoc="randomize path selection"end)moduleScriptFiles=Builder.String_list(structletname="script"letdoc="set file containing initializations, directives and stubs"end)typewarnerror=Error|Warn|QuietmoduleMissingSymbol=Builder.Variant_choice_assoc(structtypet=warnerrorletname="missing-symbol"letdoc="Select how to handle function replacement when the symbol is not resolved \
from the binary"letassoc_map=[("error",Error);("warn",Warn);("quiet",Quiet)]letdefault=Errorend)moduleTimeout=Builder.Integer_option(structletname="timeout"letdoc="Sets a timeout in second for symbolic execution"end)moduleMonitor=Builder.No(structletname="screen"letdoc="Disable the monitor screen (curses)"end)typesearch_heuristics=Dfs|Bfs|NursmoduleSearch_heuristics=Builder.Variant_choice_assoc(structtypet=search_heuristicsletname="heuristics"letdoc="Use the following search heuristics"letdefault=Dfsletassoc_map=[("dfs",Dfs);("bfs",Bfs);("nurs",Nurs)]end)moduleSeed=Builder.Integer_option(structletname="seed"letdoc="Give a specific seed for random number generators"end)