jtpaasch

(*
MAKEFILE

plugin = primus_set_mem

all: clean build install

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

jtpaasch

Z3

The REPL

In utop:

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

jtpaasch

Module SigmaTry.

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

  Definition P (x : D) : Prop :=

jtpaasch

Assembly (x86_64)

Useful quick references

General:

• http://ian.seyler.me/easy_x86-64/
• http://www.sandpile.org/x86/gpr.htm
• http://www.jacobmartin.org/code/asm.html

jtpaasch

Dune

A first pass

A library and then an executable that uses that library.

A simple library

Create a folder called foo:

jtpaasch

(** MAKEFILE:

build = _build
exe = main.native

all: clean build

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

jtpaasch

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

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

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

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


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

jtpaasch

- 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

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