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];
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];
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
&&
(* | |
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 |
#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; |
import operator | |
from z3 import * | |
def lift(z3assert): | |
def res(s): | |
s.push() | |
s.add(z3assert) | |
if s.is_good(): | |
yield | |
s.pop() |
(*| | |
A data structure that I've been more and more interested in recently is the disjoint set datastructure or union-find. | |
https://en.wikipedia.org/wiki/Disjoint-set_data_structure It's used in egraphs, unification, prolog, and graph connectivity. | |
I realized a cute representation that is easy to use and prover stuff about, although very inefficient compared to the usual version of disjoint set. It uses a simple functional representation based off the observation that the preimages of a function form disjoint sets. This representation is somewhat analogous to using functions to represent Maps in Coq like in Software Foundations. https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html | |
The nice thing about this is that it really avoids any termination stickiness. Termination of the `find_root` operation of a union find in an explicit array or tree is not at all obvious and requires side proof or a refined type. | |
The termination ultimately comes from the fact that you used a finite number of unions to cons |
struct IntDisjointMap | |
parents::Vector{Int64} | |
values::Vector{Any} | |
merge_fun | |
end | |
IntDisjointMap(merge_fun) = IntDisjointMap(Vector{Int64}[], [], merge_fun) | |
Base.length(x::IntDisjointMap) = length(x.parents) |
use egg::{*, rewrite as rw}; | |
use wasm_bindgen::prelude::*; | |
use std::time::Duration; | |
define_language! { | |
enum CatLanguage { | |
// string variant with no children | |
"id" = IdMorph(Id), | |
"om" = OTimesM([Id; 2]), | |
"oo" = OTimesO([Id; 2]), |
This is a simple script to convert Metatheory.jl https://github.com/0x0f0f0f/Metatheory.jl theories into an Egg https://egraphs-good.github.io/ query for comparison.
Get a rust toolchain https://rustup.rs/
Make a new project
cargo new my_project
cd my_project
using Pkg | |
Pkg.activate("metatheory") | |
Pkg.add(url="https://github.com/0x0f0f0f/Metatheory.jl.git") | |
using Metatheory | |
using Metatheory.EGraphs | |
cat_theory = @theory begin | |
hom(hom(f, ob(a), ob(b)) ⋅ hom(id(ob(b)), ob(b), ob(b)), ob(a), ob(b)) == hom(f, ob(a), ob(b)) | |
hom(hom(id(ob(a)), ob(a), ob(a)) ⋅ hom(f, ob(a), ob(b)), ob(a), ob(b)) == hom(f, ob(a), ob(b)) | |
hom(hom(f, ob(a), ob(b)) ⋅ hom(hom(g, ob(b), ob(c)) ⋅ hom(h, ob(c), ob(d)), ob(b), ob(d)), ob(a), ob(d)) == hom(hom(hom(f, ob(a), ob(b)) ⋅ hom(g, ob(b), ob(c)), ob(a), ob(c)) ⋅ hom(h, ob(c), ob(d)), ob(a), ob(d)) |