Permalink
Browse files

Final 1.3 update (#688)

* makes main state global and few bug fixes

The main change is that now there is only one main state in the
machine (aka project), not a separate copy per machine.

This commit also fixes leave-{blk,sub} events and adds several new
observations, such as exn-raised, that occurs every time a machine
switches to an exceptional control flow.

The commit also adds few common method to the monad interface.

* adds attributes to bitvectors

Now it is possible to attach arbitrary values to a bitvector.

* names the input interface of the Regular functor

* wip

* wip

* wip

* wip

* wip

* wip - now it compiles at least

* ensures normalization and well-typedness

also fixes a bug in Eval.binop.

* fixes a bug in arm lifter

This bug leads to a type error, as a result of a byte load and a half
word load is stored in a 32 bit variable.

* published Exp.normalization function.

* fixes a bug in type checker and exp normalizer

a type checker didn't held correctly shifts
and the normalizer didn't properly recurse

* do not force constant folding

allow a backend to choose whether to propagate consts or not.

* so far force the normalization in the exp

this is temporal cludge.

* removes exp normalization

BIR becomes unreadable. We will apply normalization when needed.

Later, we may add a memoization or stuff like that.

* sets BAP_DEBUG to true

this enables better diagnostics of compilation and configuration errors
on travis.

* adds primus mark visted plugin

the plugin will mark all terms that were visited by Primus with the
visited attribute.

* a precedence sensitive exp pretty printer

Should do this long ago, but finally found some time. No more
unnecessary parentheses!

Note: operator precedences follow the C language, not OCaml.

   +-------------------------------------------+----+
   | x[y], <cast>:<N>[x], extract:<N>:<M>[x]   | 10 |
   +-------------------------------------------+----+
   | ~x, -x                                    |  9 |
   +-------------------------------------------+----+
   | *,/,/$, %, %$                             |  8 |
   +-------------------------------------------+----+
   | +,-                                       |  7 |
   +-------------------------------------------+----+
   | <<,>>,~>>                                 |  6 |
   +-------------------------------------------+----+
   | <,>,<=,>=                                 |  5 |
   +-------------------------------------------+----+
   | =, <>                                     |  4 |
   +-------------------------------------------+----+
   | &                                         |  3 |
   +-------------------------------------------+----+
   | ^                                         |  2 |
   +-------------------------------------------+----+
   | |                                         |  1 |
   +-------------------------------------------+----+
   | let.., x with y <- z, if.., . (dot)       |  0 |
   +-------------------------------------------+----+

1) Higher precedence means that operators binds tighter.
2) Any bil statement has precedence lower than an expression.

* fixes simplifier, adds cast simplification

1. at some branches the simplified didn't recurce
2. if a cast casts to the same type it is removed

* apply constant folding by default

* fixes the Bitvector.unsigned function

it was wrong.

* removes unnecessary optimizations from the IR.lift

* adds ssa and dead-code-elimination plugins

The ssa just translates a program into the SSA form
The dead-code-elimination is a conservative deadcode elimination
plugin, that helps alot with x86 binaries by removing tons of unused
flags calcualations.

* makes string_of_value more consistent

The string_of_value function now emits the `0x` prefix for hexnumbers,
unless instructed explicitly with the `prefix:false` flag.

The reason for this change is to enable a consitent handling of signed
and unsinged, negative and positive values.

* publishes Exp.substitute function

long time ago we forgot to make it public.

* enhances dead-code elimination plugin

1. Now it will run until a fix point is reached
2. A simple constant propagation is added, so that more virtuals are
removed

* renames mem32 and mem64 in x86 lifter to mem

there is no need to have two different names for memory.

* fixes and enhances lifted representation of shifts

1. The original implementation emited the following code

```
    flag := flag
```
   to denote an unchanged flag. The code was problematic for both static
   and dynamic analysis. Static analysis treated this as a used before
   defined variable and treated flag as a free variable in the eclosing
   definition. The dynamic analysis treated `flag` as an undefined
   variable with all the consequences.

   The new implementation uses the `if` statement and changes flag only
   if it is necessary. Moreover, instead of using multiple if/then/else
   expressions, all assignment are gathered under one big if statement,
   that leads to a more simple CFG representation.

2. The original implementation emited a temporary variable that holds a
   number of bits to which the destination should be shifted. There is
   no need for such variable (it is never changed). Moreover, the
   value of this variable is usually (if not always) a constant, so it
   is better to inline it directly in expressions. It looks like that
   this is the case of a common error -  delegating OCaml computation to
   BIL. In our case this problem is solved by constant propagation.

* applies simplification to assoc operations

If in operator is associative and expression is left recursive, then
recurse to the right in hope to meet constants there. In particular,
this will simplify `x + 1 + 1 + 1` to `x + 3`.

* few optimizations and refactoring in old tainter

1. do not store values with just empty sets of values
2. special handling for the one byte storage
3. remove a key from the taint set if it is set to empty

* normalizes and simplifies expression before eval

* switches propagator to a sparse storage

* removes unused code

* calls exit if bap is interupted by Ctrl-C

so that profiler will work, as well as other at exit handlers.

* implements new Bitvector pretty printer

and rolls back the [Word.string_of_value] behavior.

The pretty printing function was totally rewritten from scratch, as
Z.format and other Z printing functions are broken. Now we have a
generic printer that suits all tastes, as well as 9 preinstantiated
pretty printers.

We also changed the bitvector default string representation. The new
representation doesn't used [true] or [false] for the [1] and [0] (this
is binary analysis anyway), and doesn't loose the signedness
information.

* docs update and few renamings

Updated bap.mli with a documentation for new functions.
Also, renamed Image.Scheme.reference to Image.Scheme.relocation.

* updated testsuite

* fix dash/underscore issue

* automates documentation generation

Now it is enough just to type `make doc` and everything will work out of
box, if a correct version of OCaml is used, i.e., 4.03. The Makefile
recipe will pull the latest version of argot (git is required) and use
it to build the documentation. BAP should be installed either from the
source tree, or from opam, doesn't matter.

* updates Primus docs

also removes some unnecessary stuff from it.

* adds monads interfaces

* updates monads docs

* cleans and documents the monads library

I've removed few unnecessary funciton, e.g., `State.modify` and also
fixed the type of the call/cc function.

* removes extra blank lines from bap.mli

* adds type checker to backends

also fixes few bugs that were found as a result

1) a zero width word was created (should be a one bit width)
2) a bug in the typechecker that led to a stackoverflow

So far no more type errors

* removes unnecessary calls to Bil.fixpoint

* adds missing manpages

also added parameters to the primus loader.

* typo in the docs

* gone crazy and rewrote the taint propagation plugin

because my last update to primus broke it(((

* makes oasy little bit less hungry

* dispatches linker unresolved calls to a lisp stub

The __primus_linker_unresolved_call function is called in case if a
linker can resolved a call.

Also adds the `pc` method to the interpreter interface and publish it
as a primitive `get-current-program-counter`.

* fixes a bug in random number generation

not actually in the random number generator, but rather in a casting it
to a word.

* don't fail the whole program on a division by zero

just fail the machine.

* enhances the run plugin with the multi-entry mode

Now we can specify a list of entry points, or a magic `all-subroutines`
to start execution in parallel from all specified entry points. If no
specified, then all subroutine terms marked with the `entry_point`
attribute are entered.

* flushes output from primus after each character

* adds a Primus component that ensures termination

The primus-limit plugin will terminate a machine after a certain amount
of computations has happened.
  • Loading branch information...
ivg authored and gitoleg committed Aug 24, 2017
1 parent 528151c commit 817eac81deeca01749dd6df3f6899f24bdd25cfb
Showing with 11,005 additions and 6,833 deletions.
  1. +1 −1 .travis.yml
  2. +1 −0 Makefile
  3. +10 −7 bapdoc.ml
  4. +14 −3 doc/Makefile
  5. +1 −1 lib/arm/arm_cond.ml
  6. +2 −5 lib/arm/arm_lifter.ml
  7. +2 −1 lib/arm/arm_mem.ml
  8. +1 −1 lib/arm/arm_mem_shift.ml
  9. +1 −1 lib/arm/arm_shift.ml
  10. +5,830 −5,296 lib/bap/bap.mli
  11. +1 −1 lib/bap/bap_project.ml
  12. +1 −2 lib/bap_disasm/bap_disasm_brancher.ml
  13. +17 −2 lib/bap_disasm/bap_disasm_target_factory.ml
  14. +2 −1 lib/bap_dwarf/dwarf_input.ml
  15. +1 −1 lib/bap_elf/elf_parse.ml
  16. +6 −4 lib/bap_image/bap_image.ml
  17. +5 −1 lib/bap_image/bap_image.mli
  18. +1 −1 lib/bap_image/bap_table.ml
  19. +1 −1 lib/bap_llvm/bap_llvm_ogre_samples.ml
  20. +1 −0 lib/bap_primus/bap_primus.ml
  21. +676 −230 lib/bap_primus/bap_primus.mli
  22. +12 −36 lib/bap_primus/bap_primus_env.ml
  23. +2 −7 lib/bap_primus/bap_primus_env.mli
  24. +244 −77 lib/bap_primus/bap_primus_interpreter.ml
  25. +39 −5 lib/bap_primus/bap_primus_interpreter.mli
  26. +40 −10 lib/bap_primus/bap_primus_linker.ml
  27. +7 −1 lib/bap_primus/bap_primus_linker.mli
  28. +124 −102 lib/bap_primus/bap_primus_lisp.ml
  29. +2 −2 lib/bap_primus/bap_primus_lisp.mli
  30. +15 −6 lib/bap_primus/bap_primus_machine.ml
  31. +1 −0 lib/bap_primus/bap_primus_machine.mli
  32. +23 −34 lib/bap_primus/bap_primus_memory.ml
  33. +6 −8 lib/bap_primus/bap_primus_memory.mli
  34. +7 −8 lib/bap_primus/bap_primus_observation.ml
  35. +8 −7 lib/bap_primus/bap_primus_pos.ml
  36. +10 −6 lib/bap_primus/bap_primus_sexp.ml
  37. +8 −3 lib/bap_primus/bap_primus_types.ml
  38. +121 −0 lib/bap_primus/bap_primus_value.ml
  39. +76 −0 lib/bap_primus/bap_primus_value.mli
  40. +1 −40 lib/bap_sema/bap_sema_lift.ml
  41. +17 −9 lib/bap_sema/bap_sema_taint.ml
  42. +2 −2 lib/bap_types/bap_bil_adt.ml
  43. +2 −0 lib/bap_types/bap_bili.ml
  44. +2 −0 lib/bap_types/bap_bili.mli
  45. +107 −42 lib/bap_types/bap_bitvector.ml
  46. +24 −1 lib/bap_types/bap_bitvector.mli
  47. +34 −102 lib/bap_types/bap_eval.ml
  48. +124 −91 lib/bap_types/bap_exp.ml
  49. +7 −0 lib/bap_types/bap_exp.mli
  50. +5 −0 lib/bap_types/bap_expi.ml
  51. +2 −0 lib/bap_types/bap_expi.mli
  52. +832 −89 lib/bap_types/bap_helpers.ml
  53. +46 −23 lib/bap_types/bap_helpers.mli
  54. +1 −1 lib/bap_types/bap_ir.ml
  55. +1 −1 lib/bap_types/bap_ir_graph.ml
  56. +9 −0 lib/bap_types/bap_monad.ml
  57. +10 −3 lib/bap_types/bap_type_error.ml
  58. +9 −0 lib/bap_types/bap_type_error.mli
  59. +28 −10 lib/bap_types/bap_types.ml
  60. +0 −1 lib/bap_types/bap_value.ml
  61. +1 −1 lib/beagle/beagle_prey.ml
  62. +1,245 −40 lib/monads/monads.mli
  63. +14 −7 lib/monads/monads_monad.ml
  64. +2 −0 lib/monads/monads_monoid.mli
  65. +12 −7 lib/monads/monads_types.ml
  66. +2 −2 lib/ogre/ogre.ml
  67. +10 −8 lib/regular/regular.mli
  68. +9 −0 lib/regular/regular_regular.ml
  69. +10 −7 lib/regular/regular_regular.mli
  70. +1 −1 lib/x86_cpu/x86_env.ml
  71. +2 −2 lib_test/bap_project/test_project.ml
  72. +19 −10 lib_test/bap_types/test_bitvector.ml
  73. +14 −0 oasis/dead-code-elimination
  74. +1 −1 oasis/frontc-parser
  75. +2 −1 oasis/primus
  76. +21 −1 oasis/primus-support
  77. +14 −0 oasis/ssa
  78. +1 −1 oasis/x86
  79. +8 −0 opam/opam
  80. +22 −1 plugins/arm/arm_main.ml
  81. +8 −7 plugins/beagle/beagle_main.ml
  82. +9 −3 plugins/byteweight/byteweight_main.ml
  83. +128 −0 plugins/dead_code_elimination/dead_code_elimination_main.ml
  84. +2 −1 plugins/emit_ida_script/emit_ida_script_main.ml
  85. +2 −2 plugins/phoenix/phoenix_printing.ml
  86. +2 −2 plugins/primus_exploring/primus_exploring_main.ml
  87. +20 −11 plugins/primus_greedy/primus_greedy_main.ml
  88. +2 −0 plugins/primus_limit/.merlin
  89. +95 −0 plugins/primus_limit/primus_limit_main.ml
  90. +1 −0 plugins/primus_lisp/lisp/posix.lisp
  91. +3 −0 plugins/primus_lisp/lisp/primus.lisp
  92. +31 −20 plugins/primus_lisp/primus_lisp_primitives.ml
  93. +7 −4 plugins/primus_loader/primus_loader_basic.ml
  94. +38 −5 plugins/primus_loader/primus_loader_main.ml
  95. +2 −0 plugins/primus_mark_visited/.merlin
  96. +53 −0 plugins/primus_mark_visited/primus_mark_visited_main.ml
  97. +2 −2 plugins/primus_print/primus_print_main.ml
  98. +26 −4 plugins/primus_promiscuous/primus_promiscuous_main.ml
  99. +285 −257 plugins/primus_propagate_taint/primus_propagate_taint_main.ml
  100. +52 −0 plugins/primus_propagate_taint/primus_propagate_taint_main.mli
  101. +13 −1 plugins/primus_x86/primus_x86_main.ml
  102. +2 −2 plugins/print/print_main.ml
  103. +2 −0 plugins/propagate_taint/propagator.ml
  104. +1 −1 plugins/relocatable/rel_brancher.ml
  105. +15 −40 plugins/relocatable/relocatable_main.ml
  106. +97 −35 plugins/run/run_main.ml
  107. +18 −0 plugins/ssa/ssa_main.ml
  108. +18 −1 plugins/x86/x86_backend.ml
  109. +65 −53 plugins/x86/x86_lifter.ml
  110. +7 −1 plugins/x86/x86_utils.ml
  111. +1 −1 src/bap_byteweight_main.ml
  112. +4 −2 src/bap_main.ml
  113. +1 −1 testsuite
View
@@ -37,7 +37,7 @@ addons:
- opam
env:
global:
- OPAMYES=true PACKAGE=bap TESTS=false BAP_RUN_TEST=true BAP_RUN_CHECK=true OPAM_SWITCH=$OCAML_VERSION
- OPAMYES=true PACKAGE=bap BAP_DEBUG=true TESTS=false BAP_RUN_TEST=true BAP_RUN_CHECK=true OPAM_SWITCH=$OCAML_VERSION
matrix:
- OCAML_VERSION=4.02
- OCAML_VERSION=4.03
View
@@ -9,6 +9,7 @@ build: setup.ml
.PHONY: doc
doc:
@ocamlbuild -pkg bap bapdoc.native
make -C doc
all:
View
@@ -8,10 +8,6 @@
*)
#use "topfind";;
#require "findlib";;
#require "bap";;
open Core_kernel.Std
open Bap_plugins.Std
@@ -55,6 +51,11 @@ let libraries = [
];
]
let std_libraries = [
"Bap"; "Core_kernel"; "Regular"; "Graphlib"; "Future"; "Monads";
"Bap_primus"
]
let frontends = [
"bap", "bap main frontend";
"bap-mc", "machine code playground";
@@ -242,6 +243,8 @@ let plugins =
let plugins_index =
sprintf "\n\n{2 Plugins}\n%s" plugins
let hides = String.concat ~sep:"," std_libraries
let argot = if Dynlink.is_native then "argot.cmxs" else "argot.cmo"
let render modules =
let intro,out = Filename.open_temp_file "intro" ".txt" in
@@ -256,10 +259,10 @@ let render modules =
"-html";
"-colorize-code";
"-short-paths";
"-i /home/ivg/.opam/devel/lib/argot";
"-g argot.cmo";
"-i"; Pkg.dir "argot";
"-g"; argot;
"-short-functors";
"-hide Bap.Std,Core_kernel.Std,Regular.Std,Graphlib.Std,Future.Std,Monads.Std,Bap_primus.Std";
"-hide"; hides;
"-passopt -search-frame";
"-passopt -search";
"-passopt -full-text";
View
@@ -1,3 +1,14 @@
.PHONY: doc
doc:
@ocaml ../bapdoc.ml 2>bapdoc.log
.PHONY: doc argot
doc: argot
../bapdoc.native 2>bapdoc.log
argot:
git clone https://github.com/ivg/argot.git
cd argot; git checkout 1.2-devel
cd argot && sh configure
make -C argot all
make -C argot install
rm -rf argot
View
@@ -27,7 +27,7 @@ let of_int_exn = function
let create w =
let open Or_error in
Word.to_int w >>= fun w ->
try_with (fun () -> of_int_exn w)
try_with ~backtrace:true (fun () -> of_int_exn w)
include Regular.Make(struct
type t = cond [@@deriving bin_io, compare, sexp]
View
@@ -1038,10 +1038,7 @@ let arm_ops_exn ops () =
~error:(Error.create "unsupported operand" op Op.sexp_of_t )
(Arm_op.create op))
let arm_ops ops = try_with (arm_ops_exn ops)
let arm_ops ops = try_with ~backtrace:true (arm_ops_exn ops)
module CPU = struct
include Arm_env
@@ -1125,4 +1122,4 @@ let insn_exn mem insn : bil Or_error.t =
let lift mem insn =
try insn_exn mem insn >>| resolve_pc mem with
| Lifting_failed msg -> errorf "%s:%s" (Basic.Insn.name insn) msg
| exn -> of_exn exn
| exn -> of_exn ~backtrace:`Get exn
View
@@ -52,7 +52,8 @@ let lift_r ~(dst1 : Var.t) ?(dst2 : Var.t option) ~(base : Var.t)
let load m n = Bil.(load m n LittleEndian typ) in
let temp = match size with
| B | H -> tmp reg32_t
| B -> tmp reg8_t
| H -> tmp reg16_t
| _ -> dst1 in
let four = Bil.int (Word.of_int 4 ~width:32) in
View
@@ -44,7 +44,7 @@ let lift_r_op ~dest1 ?dest2 ?shift ~base ~offset mode sign size operation =
| `Imm w ->
let width = Word.bitwidth w in
let _1 = Word.one 32 in
let min_32 = Word.Int_exn.(_1 lsl Word.of_int 31 ~width) in
let min_32 = Word.(_1 lsl Word.of_int 31 ~width) in
if Word.(w = min_32)
then Bil.(int Word.(zero width))
else Bil.(int w) in
View
@@ -47,7 +47,7 @@ let shift_c ~src shift_type ~shift t =
let ret1 = Bil.(src lsr e1) in
let carryin = Bil.(cast unsigned bits (var Env.cf) lsl (bits_e - e1)) in
let shifted = Bil.(ret1 lor carryin) in
let carry = nth_bit Bil.(int (Word.zero 0)) src in
let carry = nth_bit Bil.(int (Word.zero 1)) src in
shifted, carry
let r_shift ~src shift_type ~shift t =
Oops, something went wrong.

0 comments on commit 817eac8

Please sign in to comment.