1. Carl Pulley
  2. libbap

Commits

Carl Pulley  committed 6b678da

Added in map from bap CFG to python.
Started to add in map from solver model to python

  • Participants
  • Parent commits 686be7e
  • Branches master

Comments (0)

Files changed (4)

File ocaml/bap.ml

View file
 
 let _ = Callback.register "string_of_exn" Printexc.to_string
 
+type py_cfg
+external node_to_python: Cfg.AST.G.t -> Cfg.AST.G.V.t -> py_cfg -> py_cfg = "node_to_python"
+external edge_to_python: Cfg.AST.G.E.t -> py_cfg -> py_cfg = "edge_to_python"
+
+let _ = Callback.register "fold_nodes" (fun g -> Cfg.AST.G.fold_vertex (node_to_python g) g)
+
+let _ = Callback.register "fold_edges" (Cfg.AST.G.fold_edges_e edge_to_python)
+
+let _ = Callback.register "node_hash" Cfg.AST.G.V.hash
+
+let _ = Callback.register "node_label" Cfg.AST.G.V.label
+
+let _ = Callback.register "node_stmts" Cfg.AST.get_stmts
+
+let _ = Callback.register "edge_source" (fun e -> Cfg.AST.G.V.hash(Cfg.AST.G.E.src e))
+
+let _ = Callback.register "edge_target" (fun e -> Cfg.AST.G.V.hash(Cfg.AST.G.E.dst e))
+
+let _ = Callback.register "edge_label" Cfg.AST.G.E.label
+
 let str_to_arch = function
   | "x86" -> Libbfd.Bfd_arch_i386
   | "arm" -> Libbfd.Bfd_arch_arm
 
 let _ = Callback.register "bap_to_string" (fun p -> exception_wrapper(fun () -> bap_to_string p))
 
-let rec apply_cmd cmd_opts prog_term =
+let rec apply_cmd cmd_opts (prog_term, model) =
   let cmd_check cmd_type cmd = 
     if Array.length(cmd) > 0 then
       cmd_type = cmd.(0)
   in
   let common_cmds = BatList.take_while (cmd_check cmd_type) cmd_opts in
   let remaining_cmds = BatList.drop_while (cmd_check cmd_type) cmd_opts in
-  let new_prog_term =
+  let new_prog_term, model =
     if cmd_type = "iltrans" then
-      Iltrans.apply_cmd common_cmds prog_term
+      (Iltrans.apply_cmd common_cmds prog_term, model)
     else if cmd_type = "topredicate" then
       let ast_term = match prog_term with
         | Iltrans.Ast ast_term -> ast_term
         | Iltrans.Ssa _ -> failwith "Need to convert static single assignment (SSA) term into an abstract syntax tree (AST) term"
         | Iltrans.AstCfg _ -> failwith "Need to convert control-flow graph (CFG) term into an abstract syntax tree (AST) term"
       in
-        Iltrans.Ast (Topredicate.apply_cmd common_cmds ast_term)
+      let term, model = Topredicate.apply_cmd common_cmds ast_term in
+        (Iltrans.Ast term, model)
     else if cmd_type = "codegen" then
       let astcfg_term = match prog_term with
         | Iltrans.Ast ast_term -> Cfg_ast.of_prog ast_term
         | Iltrans.Ssa _ -> failwith "Need to convert static single assignment (SSA) term into an abstract syntax tree (AST) or AST control-flow graph (ASTCFG) term"
         | Iltrans.AstCfg astcfg_term -> astcfg_term
       in
-        Iltrans.AstCfg (Codegen.apply_cmd common_cmds astcfg_term)
+        (Iltrans.AstCfg (Codegen.apply_cmd common_cmds astcfg_term), model)
     else
       failwith (cmd_type ^ " is not a recognised command type")
   in
     if remaining_cmds = [] then
-      new_prog_term
+      (new_prog_term, model)
     else
-      apply_cmd remaining_cmds new_prog_term
+      apply_cmd remaining_cmds (new_prog_term, model)
 
 let _ = Callback.register "apply_cmd" (fun cmd_opts ast_term -> 
   let filtered_cmds = List.filter (fun cmd -> Array.length cmd >= 2 && cmd.(0) <> "control") cmd_opts in
-  let result = if List.length filtered_cmds = 0 then Iltrans.Ast ast_term else exception_wrapper(fun () -> apply_cmd filtered_cmds (Iltrans.Ast ast_term)) in
+  let result = if List.length filtered_cmds = 0 then (Iltrans.Ast ast_term, None) else exception_wrapper(fun () -> apply_cmd filtered_cmds (Iltrans.Ast ast_term, None)) in
     flush_all();
-    if List.mem [| "control"; "-return" |] cmd_opts then Some result else None
+    if List.mem [| "control"; "-return" |] cmd_opts then
+      Some result
+    else
+      None
 )

File ocaml/topredicate.ml

View file
         let () = p#ast_exp wp in
           p#close
     );
-    (match state.stpout with
+    (match state.pstpout with
       | None -> ()
       | Some oc ->
         let () = print_endline "Printing predicate as SMT formula" in
+        let foralls = List.map (Memory2array.coerce_rvar_state m2a_state) foralls in 
+        let pp = (((!Solver.solver)#printer) :> Formulap.fppf) in
+        let p = pp oc in
+          p#forall foralls;
+          p#ast_exp wp;
+          p#close
+    );
+    (match state.stpout with
+      | None -> 
+        (ast_term, None)
+      | Some oc ->
+        let () = print_endline "Printing predicate as SMT formula" in
         let foralls = List.map (Memory2array.coerce_rvar_state ~scope m2a_state) foralls in 
         let pp = (((!Solver.solver)#printer) :> Formulap.fppf) in
         let p = pp oc in
                  ; match r with 
                    | Smtexec.SmtError _ -> 
                       failwith "Solver error" 
+                   | Smtexec.Invalid model -> 
+                      (ast_term, Some model)
                    | _ -> 
-                      ()
+                      (ast_term, None)
                 )
+          ) else (
+            (ast_term, None)
           )
-    );
-    (match state.pstpout with
-      | None -> ()
-      | Some oc ->
-        let () = print_endline "Printing predicate as SMT formula" in
-        let foralls = List.map (Memory2array.coerce_rvar_state m2a_state) foralls in 
-        let pp = (((!Solver.solver)#printer) :> Formulap.fppf) in
-        let p = pp oc in
-          p#forall foralls;
-          p#ast_exp wp;
-          p#close
-    );
-    ast_term
+    )

File python/commands/__init__.py

View file
 
 def return_term():
   """
-  Return BAP term:
+  Return BAP term and solver model (or None if there's no model):
     -AST parse tree, if term is abstract syntax tree (AST)
     -CFG graph term, if term is control flow graph (CFG)
     -SSA graph term, if term is static single assignment (SSA)

File src/libbap.c

View file
   CAMLreturnT(PyObject*, result);
 }
 
+PyObject* bbid_to_python(value bbid) {
+  PyObject* result;
+
+  CAMLparam1(bbid);
+  CAMLlocal1(bb);
+
+  if (Is_long(bbid) && Long_val(bbid) == 0) {
+    // BB_Entry
+    result = PyString_FromString("bb_entry");
+  } else if (Is_long(bbid) && Long_val(bbid) == 1) {
+    // BB_Exit
+    result = PyString_FromString("bb_exit");
+  } else if (Is_long(bbid) && Long_val(bbid) == 2) {
+    // BB_Indirect
+    result = PyString_FromString("bb_indirect");
+  } else if (Is_long(bbid) && Long_val(bbid) == 3) {
+    // BB_Error
+    result = PyString_FromString("bb_error");
+  } else if (Is_block(bbid) && Tag_val(bbid) == 0 && Wosize_val(bbid) == 1) {
+    // BB of int
+    bb = Field(bbid, 0);
+    result = Py_BuildValue("{si}", "bb", Int_val(bb));
+  } else {
+    PyErr_SetString(PyExc_TypeError, "bbid_to_python: unexpected Cfg.bbid datatype value");
+
+    CAMLreturnT(PyObject*, NULL);
+  }
+
+  CAMLreturnT(PyObject*, result);
+}
+
+PyObject* node_to_python(value cfg, value node, PyObject* py_nodes) {
+  PyObject* py_stmts;
+  PyObject* py_label;
+  PyObject* py_node;
+
+  CAMLparam1(node);
+  CAMLlocal3(stmts, label, hash);
+
+  stmts = caml_callback2(*caml_named_value("node_stmts"), cfg, node);
+  label = caml_callback(*caml_named_value("node_label"), node);
+  hash = caml_callback(*caml_named_value("node_hash"), node);
+  py_stmts = ast_to_python(stmts);
+  py_label = bbid_to_python(label);
+  py_node = Py_BuildValue("{sisOsO}", "hash", Int_val(hash), "label", py_label, "stmts", py_stmts);
+  if (!PyErr_Occurred() && PyList_Append(py_nodes, py_node) == 0) {
+    CAMLreturnT(PyObject*, py_nodes);
+  } else {
+    // Deal with Python exception
+    CAMLreturnT(PyObject*, NULL);
+  }
+}
+
+PyObject* edge_to_python(value edge, PyObject* py_edges) {
+  PyObject* py_label;
+  PyObject* py_edge;
+
+  CAMLparam1(edge);
+  CAMLlocal3(label, source, target);
+
+  label = caml_callback(*caml_named_value("edge_label"), edge);
+  source = caml_callback(*caml_named_value("edge_source"), edge);
+  target = caml_callback(*caml_named_value("edge_target"), edge);
+  if (Is_block(label)) {
+    // label == Some of bool
+    if (Bool_val(Field(label, 0)) == Val_true) {
+      py_label = Py_True;
+    } else {
+      py_label = Py_False;
+    }
+    py_edge = Py_BuildValue("{sisisO}", "source", Int_val(source), "target", Int_val(target), "label", py_label);
+  } else {
+    // label == None
+    py_edge = Py_BuildValue("{sisi}", "source", Int_val(source), "target", Int_val(target));
+  }
+  if (!PyErr_Occurred() && PyList_Append(py_edges, py_edge) == 0) {
+    CAMLreturnT(PyObject*, py_edges);
+  } else {
+    // Deal with Python exception
+    CAMLreturnT(PyObject*, NULL);
+  }
+}
+
 PyObject* cfg_to_python(value cfg) {
   // Graph(Ast.stmt list)
-  // TODO:
+  PyObject* py_nodes;
+  PyObject* py_edges;
+  PyObject* result;
+
+  CAMLparam1(cfg);
+  CAMLlocal2(nodes, edges);
+
+  py_nodes = PyList_New(0);
+  nodes = caml_callback2(*caml_named_value("fold_nodes"), cfg, py_nodes);
+
+  py_edges = PyList_New(0);
+  edges = caml_callback2(*caml_named_value("fold_edges"), cfg, py_edges);
+
+  result = Py_BuildValue("{sOsO}", "nodes", py_nodes, "edges", py_edges);
+  CAMLreturnT(PyObject*, result);
 }
 
 //PyObject* ssa_to_python(value ssa) {
   CAMLparam1(prog_term);
   CAMLlocal1(item);
 
-  if (Is_block(prog_term) && Wosize_val(prog_term) == 1 && Tag_val(prog_term) == 0) {
+  if (Is_block(prog_term) && Tag_val(prog_term) == 0 && Wosize_val(prog_term) == 1) {
     // Ast of Ast.program
     item = Field(prog_term, 0);
 
     CAMLreturnT(PyObject*, ast_to_python(item));
-  } else if (Is_block(prog_term) && Wosize_val(prog_term) == 1 && Tag_val(prog_term) == 1) {
+  } else if (Is_block(prog_term) && Tag_val(prog_term) == 1 && Wosize_val(prog_term) == 1) {
     // AstCfg of Cfg.AST.G.t
     item = Field(prog_term, 0);
     CAMLreturnT(PyObject*, cfg_to_python(item));
-//  } else if (Is_block(prog_term) && Wosize_val(prog_term) == 1 && Tag_val(prog_term) == 2) {
+//  } else if (Is_block(prog_term) && Tag_val(prog_term) == 2 && Wosize_val(prog_term) == 1) {
 //    // Ssa of Cfg.SSA.G.t
 //    item = Field(prog_term, 0);
 //    CAMLreturnT(PyObject*, ssa_to_python(item));
   }
 }
 
+PyObject* model_to_python(value model) {
+  // model: (string * big_int) list option
+  PyObject* py_model;
+  PyObject* py_key;
+  PyObject* py_val;
+
+  CAMLparam1(model);
+  CAMLlocal4(interp, maplet, key, val);
+
+  if (Is_block(model)) {
+    // model == Some interp
+    py_model = PyDict_New();
+    interp = Field(model, 0);
+    while(!Is_long(interp)) {
+      // interp == Cons maplet interp
+      printf("here\n");
+      maplet = Field(interp, 0);
+      key = Field(maplet, 0);
+      py_key = PyString_FromString(String_val(key));
+      printf("key: %s\n", PyString_AsString(PyObject_Str(py_key)));
+      val = Field(maplet, 1);
+      py_val = big_int_to_python(val);
+      printf("value: %s\n", PyString_AsString(PyObject_Str(py_val)));
+      if (!PyErr_Occurred() && PyDict_SetItem(py_model, py_key, py_val) == 0) {
+        interp = Field(interp, 1);
+      } else {
+        // Deal with Python exception
+        Py_CLEAR(py_model);
+        CAMLreturnT(PyObject*, NULL);
+      }
+    }
+    // interp == Nil
+  } else {
+    // model == None
+    py_model = Py_None;
+  }
+
+  CAMLreturnT(PyObject*, py_model);
+}
+
 static PyObject* BAP_call(BAP* self, PyObject* args, PyObject* kwargs) {
   PyObject* cmds;
   Py_ssize_t num_cmds, cmd_size, i, j;
   PyObject* cmd;
   PyObject* cmd_str;
+  PyObject* py_term;
+  PyObject* py_model;
+  PyObject* py_result;
 
   if (self->term == NULL) {
     PyErr_SetString(PyExc_TypeError, "__call__: need to __init__ object (currently we encapsulate a null BAP term)");
   }
 
   if (Is_block(result)) {
-    // Some of Iltrans.prog
-    CAMLreturnT(PyObject*, bap_to_python(Field(result, 0)));
+    // Some of Iltrans.prog * Smtexec.model
+    item = Field(result, 0);
+    py_term = bap_to_python(Field(item, 0));
+    py_model = model_to_python(Field(item, 1));
+    py_result = Py_BuildValue("(OO)", py_term, py_model);
+    CAMLreturnT(PyObject*, py_result);
   } else {
     // None
     CAMLreturnT(PyObject*, Py_None);