Skip to content

Instantly share code, notes, and snippets.

View my_bap_loader.ml
module Loader = struct
let empty_with_program filename prog =
let arch = `unknown and code = Memmap.empty and data = Memmap.empty in
Project.Input.create arch filename ~code ~data
~finish:(fun proj -> Project.with_program proj prog)
let load filename =
let prog = Program.create () in (* empty prog for now *)
empty_with_program filename prog
@jtpaasch
jtpaasch / SimpleMonadFunctorApplicativeExample.hs
Created Apr 3, 2020
Nice little example of monads, functors, and applicatives, from https://stackoverflow.com/a/47932927
View SimpleMonadFunctorApplicativeExample.hs
- Otherwise you can't do the Applicative instance.
import Control.Applicative
-- Simple function
foo :: String -> String
foo x = do
x ++ "!!!"
-- Helper for printing Monads
@jtpaasch
jtpaasch / ps1.hs
Created Sep 27, 2019
6.820 Program Analysis - Problem Set 1
View ps1.hs
-- ***************************************************
-- 6.820 - Program Analysis - Fall 2019
-- PROBLEM SET 1
-- ***************************************************
-- ---------------------------------------------------
-- Problem 1
@jtpaasch
jtpaasch / CPDT.warmup.v
Created Sep 19, 2019
Annotated version of the warmup from Adam Chipala's _Certified Programming with Dependent Types_.
View CPDT.warmup.v
Require Import String.
(* Examples by Adam Chlipala *)
(** * Warm-up: natural numbers *)
Inductive nat := O | S (n : nat).
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
@jtpaasch
jtpaasch / Standalone_primus_machine.ml
Created May 28, 2019
Example of a simple standalone Primus machine.
View Standalone_primus_machine.ml
(** MAKEFILE:
build = _build
exe = main.native
all: clean build
clean:
rm -rf $(exe)
rm -rf $(build)
@jtpaasch
jtpaasch / Dune.md
Created Apr 9, 2019
Notes on using `dune` for OCaml.
View Dune.md

Dune

A first pass

A library and then an executable that uses that library.

A simple library

Create a folder called foo:

@jtpaasch
jtpaasch / Syllogism_with_dependent_type.v
Last active Apr 1, 2019
Syllogisms in Coq (using classical logic, and dependent types).
View Syllogism_with_dependent_type.v
Module SigmaTry.
Inductive D : Type :=
| a
| b
| c.
Definition P (x : D) : Prop :=
View Z3.quickstart.md

Z3

The REPL

In utop:

#use "topfind";;
#require "Z3";;
@jtpaasch
jtpaasch / primus_set_mem.ml
Created Feb 19, 2019
Example of a Primus plugin that sets memory values before executing a subroutine.
View primus_set_mem.ml
(*
MAKEFILE
plugin = primus_set_mem
all: clean build install
build:
bapbuild -pkg bap-primus -tags 'warn(A)' $(plugin).plugin
You can’t perform that action at this time.