adds traps for memory and division operations

Division by zero as well as faulty memory operations may terminate the
Primus Machine. Previously we were just terminating it with a specific
exception. However, this exceptions should actually be represented by
an CPU/ABI-specific interrupt or trap. The proposed implementation
provides a mechanism that allows:

- trap the exception and translate it to a machine specific
  interrupt;

- ignore or fix it;

- catch it on a low-level.

The mechanism is based on the same idea as in the Linker that used the
primus_unresolved_handler to trap unresolved names. For each trap we
provide a corresponding observation, that could be used to install the
trap. The trap itself, is a special name, that could be linked (either
on a permanent basis, or from the observation). If the trap hanlder is
assigned, then it is invoked. Concrete behavior depends on a
particular trap, e.g.,

- for linker trap - the hanlder is invoked instead of the missing code;
- for the division by zero - if the handler returns
  then the result is undefined;
- for memory fault - the trap should fix the problem or terminate.

We also introduce the Pagefault exception, to represent memory
traps. We keep segfault as a non-maskable (non-preventable)
exception.

In addition, we have provided several new operations in the Linker
interface:
- unlink: for code unlinking, useful for removing traps
- lookup: useful for restoring other's traps

As a showcase, we also reimplemented some parts of the promiscuous
mode. Now we use the pagefault trap to prevent segmentation
faults. Also the fixing is more efficient as instead of mapping one
byte pages, we are mapping pages with size of up to 4k.

Besides others, this commit will also provide a fix for #839.

lib/bap_primus/bap_primus_interpreter.ml

@@ -61,6 +61,15 @@ let pc_change,pc_changed =
 let halting,will_halt =
   Observation.provide ~inspect:sexp_of_unit "halting"
 
+let division_by_zero,will_divide_by_zero =
+  Observation.provide ~inspect:sexp_of_unit "division-by-zero"
+
+let segfault, will_segfault =
+  Observation.provide ~inspect:sexp_of_word "segfault"
+
+let pagefault,page_fail =
+  Observation.provide ~inspect:sexp_of_word "pagefault"
+
 let interrupt,will_interrupt =
   Observation.provide ~inspect:sexp_of_int "interrupt"
 
@@ -177,18 +186,26 @@ let state = Bap_primus_machine.State.declare
          curr = Top {me=prog; up=Nil};
        })
 
-
 type exn += Halt
+type exn += Division_by_zero
+type exn += Segmentation_fault of addr
 type exn += Runtime_error of string
 
 let () =
   Exn.add_printer (function
       | Runtime_error msg ->
         Some (sprintf "Bap_primus runtime error: %s" msg)
       | Halt -> Some "Halt"
+      | Segmentation_fault x ->
+        Some (asprintf "Segmentation fault at %a" Addr.pp_hex x)
+      | Division_by_zero -> Some "Division by zero"
       | _ -> None)
 
 
+let division_by_zero_handler = "__primus_division_by_zero_handler"
+let pagefault_handler =  "__primus_pagefault_hanlder"
+
+
 module Make (Machine : Machine) = struct
   open Machine.Syntax
 
@@ -226,12 +243,24 @@ module Make (Machine : Machine) = struct
     Env.get v >>= fun r ->
     !!on_read (v,r) >>| fun () -> r
 
-  let binop op x y =
-    try
+
+  let call_when_provided name =
+    Code.is_linked (`symbol name) >>= fun provided ->
+    if provided then Code.exec (`symbol name) >>| fun () -> true
+    else Machine.return false
+
+  let binop op x y = match op with
+    | Bil.DIVIDE | Bil.SDIVIDE
+    | Bil.MOD | Bil.SMOD
+      when Word.is_zero y.value ->
+      !!will_divide_by_zero () >>= fun () ->
+      call_when_provided division_by_zero_handler >>= fun called ->
+      if called
+      then undefined (Type.Imm (Word.bitwidth x.value))
+      else Machine.raise Division_by_zero
+    | _ ->
       value (Bil.Apply.binop op x.value y.value) >>= fun r ->
       !!on_binop ((op,x,y),r) >>| fun () -> r
-    with Division_by_zero -> failf "Division by zero" ()
-
 
   let unop op x =
     value (Bil.Apply.unop op x.value) >>= fun r ->
@@ -253,14 +282,25 @@ module Make (Machine : Machine) = struct
     value c >>= fun r ->
     !!on_const r >>| fun () -> r
 
+  let trapped_memory_access access =
+    Machine.catch access (function
+        | Bap_primus_memory.Pagefault a ->
+          !!page_fail a >>= fun () ->
+          call_when_provided pagefault_handler >>= fun trapped ->
+          if trapped then access
+          else
+            !!will_segfault a >>= fun () ->
+            Machine.raise (Segmentation_fault a)
+        | exn -> Machine.raise exn)
+
   let load_byte a =
     !!on_loading a >>= fun () ->
-    Memory.get a.value >>= fun r ->
+    trapped_memory_access (Memory.get a.value) >>= fun r ->
     !!on_loaded (a,r) >>| fun () -> r
 
   let store_byte a x =
     !!on_storing a >>= fun () ->
-    Memory.set a.value x >>= fun () ->
+    trapped_memory_access (Memory.set a.value x) >>= fun () ->
     !!on_stored (a,x)
 
   let rec eval_exp x =

lib/bap_primus/bap_primus_interpreter.mli

@@ -5,6 +5,9 @@ open Bap_primus_types
 val pc_change : addr observation
 val halting : unit observation
 val interrupt : int observation
+val division_by_zero : unit observation
+val segfault : addr observation
+val pagefault : addr observation
 
 val loading : value observation
 val loaded : (value * value) observation
@@ -54,6 +57,12 @@ val leave_jmp : jmp term observation
 
 
 type exn += Halt
+type exn += Division_by_zero
+type exn += Segmentation_fault of addr
+
+val division_by_zero_handler : string
+val pagefault_handler : string
+
 
 module Make (Machine : Machine) : sig
   type 'a m = 'a Machine.t

lib/bap_primus/bap_primus_linker.ml

@@ -43,7 +43,8 @@ let empty = {
   alias = Int.Map.empty;
 }
 
-let unresolved_handler = `symbol "__primus_linker_unresolved_call"
+
+let unresolved_handler = "__primus_linker_unresolved_call"
 
 include struct
   open Sexp
@@ -59,6 +60,10 @@ include struct
     List (Atom dst :: sexp_of_args args)
 end
 
+let unbound_name,needs_unbound =
+  Bap_primus_observation.provide ~inspect:sexp_of_name
+    "linker-unbound"
+
 module Trace = struct
   module Observation = Bap_primus_observation
   let exec,will_exec = Observation.provide
@@ -123,7 +128,6 @@ module Make(Machine : Machine) = struct
     Machine.Local.get state >>| code_of_name name >>| Option.is_some
 
   let do_fail name =
-    Machine.Observation.make will_fail name >>= fun () ->
     Machine.Local.get state >>= fun s ->
     match resolve_name s name with
     | Some s -> linker_error (`symbol s)
@@ -135,8 +139,9 @@ module Make(Machine : Machine) = struct
     Code.exec
 
   let fail name =
+    Machine.Observation.make will_fail name >>= fun () ->
     Machine.Local.get state >>= fun s ->
-    match code_of_name unresolved_handler s with
+    match code_of_name (`symbol unresolved_handler) s with
     | None -> do_fail name
     | Some code -> run name code
 
@@ -159,8 +164,26 @@ module Make(Machine : Machine) = struct
           } in
         {codes; terms; names; addrs; alias})
 
+
+  let unlink name =
+    Machine.Local.get state >>= fun s ->
+    match id_of_name name s with
+    | None -> Machine.return ()
+    | Some id ->
+      let cleanup = Map.filter ~f:(fun id' -> id <> id') in
+      Machine.Local.put state {
+        codes = Map.remove s.codes id;
+        alias = Map.remove s.alias id;
+        terms = cleanup s.terms;
+        names = cleanup s.names;
+        addrs = cleanup s.addrs;
+      }
+
+  let lookup name =
+    Machine.Local.get state >>| code_of_name name
+
   let exec name =
-    Machine.Local.get state >>| code_of_name name >>= function
+    lookup name >>= function
     | None -> fail name
     | Some code -> run name code
 

lib/bap_primus/bap_primus_linker.mli

@@ -13,6 +13,10 @@ type exn += Unbound_name of name
 
 val exec : name observation
 val will_exec : name statement
+val unresolved : name observation
+
+val unresolved_handler : string
+
 module Trace : sig
   val call : (string * value list) observation
   val call_entered : (string * value list) statement
@@ -25,6 +29,7 @@ end
 
 type code = (module Code)
 
+
 module Name : Regular.S with type t = name
 
 module Make(Machine : Machine) : sig
@@ -36,6 +41,9 @@ module Make(Machine : Machine) : sig
     ?tid:tid ->
     code -> unit m
 
+  val lookup : name -> code option m
+  val unlink : name -> unit m
+
   val exec : name -> unit m
 
   val is_linked : name -> bool m

lib/bap_primus/bap_primus_memory.ml

@@ -10,11 +10,11 @@ module Random  = Bap_primus_random
 module Generator = Bap_primus_generator
 open Bap_primus_sexp
 
-type exn += Segmentation_fault of addr
+type exn += Pagefault of addr
 
 let () = Exn.add_printer (function
-    | Segmentation_fault here ->
-      Some (asprintf "Segmentation fault at %a"
+    | Pagefault here ->
+      Some (asprintf "Page fault at %a"
               Addr.pp_hex here)
     | _ -> None)
 
@@ -101,10 +101,10 @@ module Make(Machine : Machine) = struct
     Machine.Local.get state >>= fun s ->
     Machine.Local.put state (f s)
 
-  let segfault addr = Machine.raise (Segmentation_fault addr)
+  let pagefault addr = Machine.raise (Pagefault addr)
 
   let read addr {values;layers} = match find_layer addr layers with
-    | None -> segfault addr
+    | None -> pagefault addr
     | Some layer -> match Map.find values addr with
       | Some v -> Machine.return v
       | None -> match layer.mem with
@@ -117,8 +117,8 @@ module Make(Machine : Machine) = struct
 
   let write addr value {values;layers} =
     match find_layer addr layers with
-    | None -> segfault addr
-    | Some {perms={readonly=true}} -> segfault addr
+    | None -> pagefault addr
+    | Some {perms={readonly=true}} -> pagefault addr
     | Some _ -> Machine.return {
         layers;
         values = Map.add values ~key:addr ~data:value;

lib/bap_primus/bap_primus_memory.mli

@@ -3,7 +3,7 @@ open Bap_primus_types
 
 module Generator = Bap_primus_generator
 
-type exn += Segmentation_fault of addr
+type exn += Pagefault of addr
 
 module Make(Machine : Machine) : sig
 

plugins/primus_promiscuous/primus_promiscuous_main.ml

@@ -76,6 +76,18 @@ let assumptions blk =
         | Bil.Int _ -> assns, (neg assns) :: assms
         | _ -> failwith "Not in TCF") |> snd
 
+
+module TrapPageFault(Machine : Primus.Machine.S) = struct
+  module Code = Primus.Linker.Make(Machine)
+  let exec =
+    Code.unlink (`symbol Primus.Interpreter.pagefault_handler)
+end
+
+module DoNothing(Machine : Primus.Machine.S) = struct
+  let exec = Machine.return ()
+end
+
+
 module Main(Machine : Primus.Machine.S) = struct
   open Machine.Syntax
   module Eval = Primus.Interpreter.Make(Machine)
@@ -157,20 +169,30 @@ module Main(Machine : Primus.Machine.S) = struct
     | _ -> Machine.return ()
 
 
-  let map addr =
-    Mem.allocate ~generator:Primus.Generator.Random.Seeded.byte addr 1
+  let default_page_size = 4096
+  let default_generator = Primus.Generator.Random.Seeded.byte
+
+  let map_page already_mapped addr =
+    let rec map len =
+      let last = Addr.nsucc addr (len - 1) in
+      already_mapped last >>= function
+      | true -> map (len / 2)
+      | false ->
+        Mem.allocate ~generator:default_generator addr len in
+    map default_page_size
+
+  let trap () =
+    Linker.link ~name:Primus.Interpreter.pagefault_handler
+      (module TrapPageFault)
 
-  let make_loadable value =
-    let addr = Primus.Value.to_word value in
-    Mem.is_mapped addr >>= function
-    | false -> map addr
-    | true -> Machine.return ()
+  let pagefault x =
+    Mem.is_mapped x >>= function
+    | false -> map_page Mem.is_mapped x >>= trap
+    | true ->
+      Mem.is_writable x >>= function
+      | false -> map_page Mem.is_writable x >>= trap
+      | true -> Machine.return ()
 
-  let make_writable value =
-    let addr = Primus.Value.to_word value in
-    Mem.is_writable addr >>= function
-    | false -> map addr
-    | true -> Machine.return ()
 
   let mark_visited blk =
     Machine.Global.update state ~f:(fun t -> {
@@ -190,10 +212,18 @@ module Main(Machine : Primus.Machine.S) = struct
     Machine.Seq.iter ~f:(fun var ->
         Env.add var (Primus.Generator.static 0))
 
+  let ignore_division_by_zero =
+    Linker.link ~name:Primus.Interpreter.division_by_zero_handler
+      (module DoNothing)
+
+  let ignore_unresolved_nmaes =
+    Linker.link ~name:Primus.Linker.unresolved_handler
+      (module DoNothing)
+
   let init () = Machine.sequence [
       setup_vars;
-      Primus.Interpreter.loading >>> make_loadable;
-      Primus.Interpreter.storing >>> make_writable;
+      ignore_division_by_zero;
+      Primus.Interpreter.pagefault >>> pagefault;
       Primus.Interpreter.leave_pos >>> step;
       Primus.Interpreter.leave_blk >>> mark_visited;
     ]