Skip to content

Instantly share code, notes, and snippets.

Avatar

Philip Zucker philzook58

View GitHub Profile
@philzook58
philzook58 / tc.sql
Last active March 13, 2023 04:34
Transitive closure
View tc.sql
CREATE TABLE tc(a INTEGER, b INTEGER, PRIMARY KEY (a,b));
INSERT OR IGNORE INTO tc(a,b)
VALUES (1,2),(2,3),(3,4);
-- repeat this query many times for naive iteration
-- path(x,z) :- path(x,y), path(y,z).
INSERT OR IGNORE INTO tc SELECT DISTINCT tc0.a, tc1.b -- the head of the rule gives the insert and select fields
FROM tc as tc0, tc as tc1
WHERE tc0.b = tc1.a; -- The body of the rule gives FROM and WHERE
@philzook58
philzook58 / README.md
Created August 18, 2022 14:45
Weakest precondition in pure smtlib2 using reflection and define-fun-rec
View README.md

Computing weakest precondition of Imp programs directly in Z3. Requires reflection of smtlib expressions into expression datatypes and representing the variable store as an array. In principle, smtlib is it's own macro system.

Typically people use python or some other language to generate smtlib. Boogie and Why3 are frameworks that generate smtlib (among other things) from imperative code. We can remove one level of indirection by directly programming in Z3. There are so many other good abstractions that smtlib is just barely able to express in this style.

@philzook58
philzook58 / comm_assoc.py
Created April 10, 2022 02:14
Z3 on uninterpreted commutative
View comm_assoc.py
from z3 import *
Num = DeclareSort("Num")
add = Function("add", Num, Num, Num)
num = Function("num", IntSort(), Num)
from functools import reduce
import random
print(reduce(add, [num(n) for n in range(10)]))
x,y,z = Consts("x y z", Num)
View scopedUnionfind.md

Scoped union find

Max has put forward that we need different union finds floating around indexed in some way

A more complex union find structure seems like it could be useful. We might want a fully non destructive union find. Another option is a "scoped union find". Scopes form a forest. Deeper scopes get the subsequent unions of their ancestor scopes, but not vice versa. Scopes form a partially ordered set.

Options of multiple related union finds:

  1. The fillaitre conchon persistent union find has an angle where you really only have one union find active at a time.
  2. Using functional maps to implement union find rather than imperative arrays or refs. You don't get path compression? How important is that really? ln(n) vs inverse_ack(n) both feel close to constant.
  3. just copy entire union find every time you need a new one. Updates to higher union finds don't immediately propagate to lower ones for good or bad
@philzook58
philzook58 / README.md
Created March 4, 2022 17:18
souffle egglog 2
View README.md

Compile the library. I got the various build arguments from souffle-compile. You can also run this in interpreter mode.

../../souffle/build/src/souffle add2.dl -lunionfind -o out -j4
time ./out -j4
@philzook58
philzook58 / EquivalenceRelation.h
Last active March 4, 2022 20:17
souffle findNode functor
View EquivalenceRelation.h
yada yada ayda
/**
* Returns unionfind parent of Node
* @param x
*/
value_type findNode(value_type x) const {
return sds.findNode(x);
}
@philzook58
philzook58 / dune
Last active January 6, 2022 00:52
primus lisp programmatic loading in bap
View dune
(executable
(name main)
;(modes byte js)
(flags -linkall -g)
; with dune build main.bc.js --release
; gets us to the Sys flushed error.
(js_of_ocaml (flags --toplevel --dynlink +toplevel.js +dynlink.js --disable inline --pretty --source-map-inline
--file /home/philip/.opam/bapjs/lib/bap/bil.plugin
--file /home/philip/.opam/bapjs/lib/bap/primus_lisp.plugin
--file /home/philip/Documents/ocaml/bapjs2/staticload/test.lisp
@philzook58
philzook58 / README.md
Last active January 1, 2022 22:56
js_of_ocaml custom directory
View README.md
dune build main.bc.js --release
node _build/default/main.bc.js

Returns

$node _build/default/main.bc.js
/home/philip/Documents/ocaml/bapjs2/jsoo_crash/_build/default/main.bc.js:3937
 {r += exn[1][1];
@philzook58
philzook58 / README.md
Last active December 31, 2021 13:21
Bap Stack overflow error in js_of_ocaml
View README.md

Build with dune build main.bc.js --release Demonstrates stack overflow on dynlinking the bap_c library.

Troubleshooting is difficult. Unfortunately the overflow error is being caught and translated in a way that obscures the original cause. To find what I believe is an accurate stack trace do the following: Go into _build/default/main.bc.js. Add Error.stackTraceLimit = Infinity; to the top. Grep for RangeError. Add in console.log(e.stack); into the exception handler like so

     {if(e instanceof Array)return e;
      if
       (joo_global_object.RangeError
 &&
@philzook58
philzook58 / bapjs.ml
Created November 5, 2021 03:55
Attempting to js_of_ocaml bap
View bapjs.ml
(*
ocamlfind ocamlc -package bap -package core_kernel -linkpkg -linkall baptest.ml
js_of_ocaml +dynlink.js +toplevel.js +zarith_stubs_js/runtime.js +zarith_stubs_js/biginteger.js \
+base/base_internalhash_types/runtime.js +base/runtime.js +time_now/runtime.js +bin_prot/runtime.js \
+ppx_expect/collector/runtime.js +base_bigstring/runtime.js +core_kernel/strftime.js +core_kernel/runtime.js \
+bigstringaf/runtime.js --linkall --extern-fs --toplevel a.out
*)
open Core_kernel
open Bap.Std