ivg

(*** Turing Machines in Coq *)

(** Some preliminary types we'll use *)
CoInductive CoList (A: Type) := CONS (a:A) (t:CoList A) | NIL.

Arguments CONS [A] _ _.
Arguments NIL [A].

CoInductive Delay A := HERE (a:A) | LATER (_:Delay A).
 

ivg

(* 

Computes an expression using Primus. Showcases how to bootstrap the whole Primus machinery and how
to store and extract results of computations from the project data structure.

To compile, put this file in an empty folder and run the following commands:

$ bapbuild -pkg bap-primus peval.plugin
$ bapbundle instll peval.plugin

ivg

(extend ddtbd)
;; debugging stuff
(option primus-propagate-taint-to-attributes)
(option print-bir-attr tainted-reg)
(option print-bir-attr tainted-ptr)
(option print-bir-attr tainted-regs)
(option print-bir-attr tainted-ptrs)
(option dump bir:out.bir)

(option primus-print-obs enter-term read)

ivg

(* a simple iterator, using the for loop, note that it counts objects starting from 1. *)
let iter_combs n k f =
  let rec gen v s j =
    if j > k then f v
    else for i = s to n do
        gen (i::v) (i+1) (j+1)
      done in
  gen [] 1 1

ivg

opam-version: "2.0"
compiler: [
  "base-bigarray.base"
  "base-threads.base"
  "base-unix.base"
  "ocaml-base-compiler.4.07.0"
]
roots: [
  "bap-signatures.1.5.0"
  "base.v0.11.1"

ivg

open Core_kernel

module Ast = struct
  type ident = string [@@deriving compare, hash, sexp]

  type t =
    | Var of ident
    | Int of int
    | Let of ident * t * t
    | App of ident * t list

ivg

open Core_kernel.Std
open Bap.Std
open Or_error.Monad_infix

module Insn = Disasm_expert.Basic.Insn

module Mips = struct
  (** Defines the register map *)
  module CPU = struct
    let mem = Var.create "mem" @@ mem32_t `r8

ivg

open Core_kernel
open Bap_core_theory
open Bap.Std
open KB.Syntax
include Self()

module Word = struct
  include Bitvec_order
  include Bitvec_sexp.Functions
end

ivg

open Core_kernel
open Bap_core_theory
open Bap.Std
open KB.Syntax
include Self()

let package = "bytoy"

type name = string [@@deriving equal,sexp]
type oper = Reg of int | Imm of int [@@deriving equal,sexp]

ivg

open Core_kernel
open Bap_main
open Bap_knowledge
open Bap_core_theory

open Bap.Std
open KB.Syntax

let zero_collector = object
  inherit [Tid.Set.t] Term.visitor