philzook58

import operator
from z3 import *

def lift(z3assert):
    def res(s):
        s.push()
        s.add(z3assert)
        if s.is_good():
            yield
        s.pop()

philzook58

#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <time.h>

#define FLAG_BUFFER 128
#define MAX_SYM_LEN 4

typedef struct Stonks {
	int shares;

philzook58

(*
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

philzook58

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

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

(*|

I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on a cross country slog.

There are a number of factors to this. 
* I could use Z3's python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq.
* Z3 can actually be used to declaratively state problems and automatically calculate solutions to them with very little user help, which gives it a lot more "Wow" factor.
* Coq is a tool that requires significantly more background to even comprehend what the hell it is. I still think many aspects of it are tota

philzook58

(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

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

yada yada ayda

/**
     * Returns unionfind parent of Node
     * @param x
     */
    value_type findNode(value_type x) const {
        return sds.findNode(x);
    }

philzook58

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