JT Paasch jtpaasch

Recently created

Least recently created

Recently updated

Least recently updated

jtpaasch / ps1.hs

Created September 27, 2019 13:51

6.820 Program Analysis - Problem Set 1

	-- ***************************************************

	-- 6.820 - Program Analysis - Fall 2019
	-- PROBLEM SET 1

	-- ***************************************************


	-- ---------------------------------------------------
	-- Problem 1

jtpaasch / CPDT.warmup.v

Created September 19, 2019 12:46

Annotated version of the warmup from Adam Chipala's _Certified Programming with Dependent Types_.

	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 / Standalone_primus_machine.ml

Created May 28, 2019 18:20

Example of a simple standalone Primus machine.

	(** MAKEFILE:

	build = _build
	exe = main.native

	all: clean build

	clean:
	rm -rf $(exe)
	rm -rf $(build)

jtpaasch / Dune.md

Created April 9, 2019 18:36

Notes on using `dune` for OCaml.

Dune

A first pass

A library and then an executable that uses that library.

A simple library

Create a folder called foo:

jtpaasch / Assembly_cheat_sheet.md

Created April 1, 2019 12:34

Quick reminder of all the little things I forget.

Assembly (x86_64)

Useful quick references

General:

jtpaasch / Syllogism_with_dependent_type.v

Last active April 1, 2019 12:16

Syllogisms in Coq (using classical logic, and dependent types).



	Module SigmaTry.

	Inductive D : Type :=
	\| a
	\| b
	\| c.

	Definition P (x : D) : Prop :=

jtpaasch / Z3.quickstart.md

Created February 21, 2019 21:09

Simple Z3 tutorial

Z3

The REPL

In utop:

#use "topfind";;
#require "Z3";;

jtpaasch / primus_set_mem.ml

Created February 19, 2019 22:02

Example of a Primus plugin that sets memory values before executing a subroutine.

	(*
	MAKEFILE

	plugin = primus_set_mem

	all: clean build install

	build:
	bapbuild -pkg bap-primus -tags 'warn(A)' $(plugin).plugin

jtpaasch / primus_set_regs.ml

Last active February 19, 2019 22:02

Example of a Primus component that sets register values before running a function.

	(*
	MAKEFILE:

	plugin = primus_set_regs

	all: clean build install

	build:
	bapbuild -pkg bap-primus -tags 'warn(A)' $(plugin).plugin

jtpaasch / primus_set_register_example.ml

Created February 13, 2019 13:46

A simple example of how to set registers with Primus

	(*

	plugin = primus_set_register_example

	all: clean build install

	build:
	bapbuild -pkg bap-primus -tags 'warn(A)' $(plugin).plugin

	install:

Newer Older