diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..523064d --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,33 @@ +name: Builds, tests & co + +on: + pull_request: + push: + +permissions: read-all + +jobs: + build: + strategy: + fail-fast: false + matrix: + os: + - macos-latest + - ubuntu-latest + + runs-on: ${{ matrix.os }} + + steps: + - name: Checkout tree + uses: actions/checkout@v4 + + - name: Set-up OCaml + uses: ocaml/setup-ocaml@v2 + with: + ocaml-compiler: "ocaml-variants.5.1.1+effect-syntax" + + - run: opam install . --deps-only --with-test + + - run: opam exec -- dune build + + - run: opam exec -- dune runtest diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..70449f0 --- /dev/null +++ b/.gitignore @@ -0,0 +1,89 @@ +# Created by https://www.toptal.com/developers/gitignore/api/ocaml,vim,macos +# Edit at https://www.toptal.com/developers/gitignore?templates=ocaml,vim,macos + +### macOS ### +# General +.DS_Store +.AppleDouble +.LSOverride + +# Icon must end with two \r +Icon + +# Thumbnails +._* + +# Files that might appear in the root of a volume +.DocumentRevisions-V100 +.fseventsd +.Spotlight-V100 +.TemporaryItems +.Trashes +.VolumeIcon.icns +.com.apple.timemachine.donotpresent + +# Directories potentially created on remote AFP share +.AppleDB +.AppleDesktop +Network Trash Folder +Temporary Items +.apdisk + +### macOS Patch ### +# iCloud generated files +*.icloud + +### OCaml ### +*.annot +*.cmo +*.cma +*.cmi +*.a +*.o +*.cmx +*.cmxs +*.cmxa + +# ocamlbuild working directory +_build/ + +# ocamlbuild targets +*.byte +*.native + +# oasis generated files +setup.data +setup.log + +# Merlin configuring file for Vim and Emacs +.merlin + +# Dune generated files +*.install + +# Local OPAM switch +_opam/ + +### Vim ### +# Swap +[._]*.s[a-v][a-z] +!*.svg # comment out if you don't need vector files +[._]*.sw[a-p] +[._]s[a-rt-v][a-z] +[._]ss[a-gi-z] +[._]sw[a-p] + +# Session +Session.vim +Sessionx.vim + +# Temporary +.netrwhist +*~ +# Auto-generated tag files +tags +# Persistent undo +[._]*.un~ + +# End of https://www.toptal.com/developers/gitignore/api/ocaml,vim,macos +n diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 0000000..87c1145 --- /dev/null +++ b/.ocamlformat @@ -0,0 +1,3 @@ +profile = default +version = 0.26.2 +wrap-comments = true diff --git a/bin/dune b/bin/dune new file mode 100644 index 0000000..b7dbb23 --- /dev/null +++ b/bin/dune @@ -0,0 +1,4 @@ +(executable + (public_name react_trace) + (name main) + (libraries react_trace)) diff --git a/bin/main.ml b/bin/main.ml new file mode 100644 index 0000000..7bf6048 --- /dev/null +++ b/bin/main.ml @@ -0,0 +1 @@ +let () = print_endline "Hello, World!" diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..06a01de --- /dev/null +++ b/dune-project @@ -0,0 +1,32 @@ +(lang dune 3.15) + +(name react_trace) + +(generate_opam_files true) + +(source + (github React-Analysis/ReacttRace)) + +(authors "Jay Lee") + +(maintainers "Jay Lee") + +(license LICENSE) + +; (documentation https://url/to/documentation) + +(package + (name react_trace) + (synopsis "React Analyzer") + (description "ReacttRace is a tool for analyzing React programs.") + (depends + ocaml + dune + (ocaml-variants (= 5.1.1+effect-syntax)) + base + logs + stdio) + (tags + (React "Static Analysis"))) + +; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project diff --git a/lib/batched_queue.ml b/lib/batched_queue.ml new file mode 100644 index 0000000..0552437 --- /dev/null +++ b/lib/batched_queue.ml @@ -0,0 +1,26 @@ +open! Base + +type 'a t = { f : 'a list; r : 'a list } + +exception Empty_queue + +let empty = { f = []; r = [] } +let is_empty = function { f = []; _ } -> true | _ -> false + +let enqueue q x = + match q with + | { f = []; _ } -> { f = [ x ]; r = [] } + | { f; r } -> { f; r = x :: r } + +let front = function + | { f = []; _ } -> raise Empty_queue + | { f = h :: _; _ } -> h + +let dequeue = function + | { f = []; _ } -> raise Empty_queue + | { f = [ _ ]; r } -> { f = List.rev r; r = [] } + | { f = _ :: t; r } -> { f = t; r } + +let size { f; r } = List.(length f + length r) +let to_list { f; r } = f @ List.rev r +let fold q = List.fold (to_list q) diff --git a/lib/domains.ml b/lib/domains.ml new file mode 100644 index 0000000..512abde --- /dev/null +++ b/lib/domains.ml @@ -0,0 +1,83 @@ +open! Base +open Syntax + +module Env = struct + type 'a t = 'a Id.Map.t + + let empty = Id.Map.empty + let lookup env ~id = Map.find env id + let extend env ~id ~value = Map.set env ~key:id ~data:value +end + +module Store = struct + type 'a t = 'a Label.Map.t + + let empty = Label.Map.empty + let lookup store ~label = Map.find_exn store label + let update store ~label ~value = Map.set store ~key:label ~data:value +end + +module Tree_path = struct + module T = Int + include T + + module Map = struct + open Map + include M (T) + + let empty = empty (module T) + end +end + +module Job_q = Batched_queue + +type value = + | Unit + | Int of int + | View_spec of view_spec list + | Clos of clos + | Set_clos of set_clos + | Comp_clos of comp_clos + | Comp_thunk of comp_thunk + +and clos = { param : Id.t; body : hook_free Expr.t; env : env } +and set_clos = { label : Label.t; path : path } +and comp_clos = { comp : Prog.comp; env : env } +and comp_thunk = { comp : Prog.comp; env : env; arg : value } +and view_spec = Vs_null | Vs_int of int | Vs_comp of comp_thunk +and env = value Env.t +and phase = P_init | P_update | P_retry | P_effect +and node_ctx = { decision : decision; st_store : st_store; tree_mem : tree_mem } +and decision = Idle | Retry | Update +and st_store = (value * job_q) Store.t +and job_q = clos Job_q.t + +and part_view = { + view_spec : view_spec; + decision : decision; + st_store : st_store; + eff_q : job_q; +} + +and tree = + | Leaf of tree_val + | Node of { part_view : part_view; children : path list } + +and tree_val = Leaf_null | Leaf_int of int +and tree_mem = tree option Tree_path.Map.t +and path = Tree_path.t + +let empty_env : env = Env.empty +let empty_st_store : st_store = Store.empty +let empty_tree_mem : tree_mem = Tree_path.Map.empty +let empty_setq : job_q = Job_q.empty +let empty_effq : job_q = Job_q.empty + +let equal v1 v2 = + match (v1, v2) with + | Unit, Unit -> true + | Int i1, Int i2 -> i1 = i2 + | _, _ -> false + +let ( = ) = equal +let ( <> ) v1 v2 = not (equal v1 v2) diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000..5639527 --- /dev/null +++ b/lib/dune @@ -0,0 +1,3 @@ +(library + (name react_trace) + (libraries base logs stdio)) diff --git a/lib/interp.ml b/lib/interp.ml new file mode 100644 index 0000000..1fc9dd8 --- /dev/null +++ b/lib/interp.ml @@ -0,0 +1,127 @@ +open! Base +open Stdlib.Effect +open Syntax +open Domains + +type _ eff += Rd_env : env eff | In_env : env -> (('b -> 'a) -> 'b -> 'a) eff + +type _ eff += + | Lookup_st : Label.t -> (value * job_q) eff + | Update_st : (Label.t * (value * job_q)) -> unit eff + +type _ eff += + | Part_view_set_dec : path * Label.t * decision -> unit eff + | Part_view_enq_set : path * Label.t * clos -> unit eff + +type _ eff += Set_dec : decision -> unit eff +type _ eff += Rd_phase : phase eff +type _ eff += Rd_path : path eff +type _ eff += Enq_eff : clos -> unit eff + +exception Unbound_var of string +exception Type_error +exception Invalid_phase + +let rec eval : type a. a Expr.t -> value = function + | Const (Unit ()) -> Unit + | Const (Int i) -> Int i + | Var x -> ( + let env = perform Rd_env in + match Map.find env x with Some v -> v | None -> raise (Unbound_var x)) + | View es -> + let vss = + List.fold es ~init:[] ~f:(fun vss e -> + let vs = + match eval e with + | Unit -> Vs_null + | Int i -> Vs_int i + | Comp_thunk t -> Vs_comp t + | _ -> raise Type_error + in + vs :: vss) + in + View_spec vss + | Cond { pred; con; alt } -> ( + match eval pred with + | Int 0 -> eval alt + | Int _ -> eval con + | _ -> raise Type_error) + | Fn { param; body } -> Clos { param; body; env = perform Rd_env } + | App { fn; arg } -> ( + match eval fn with + | Clos { param; body; env } -> + let env = Env.extend env ~id:param ~value:(eval arg) in + perform (In_env env) eval body + | Comp_clos { comp; env } -> Comp_thunk { comp; env; arg = eval arg } + | Set_clos { label; path } -> + let clos = + (* Argument to the setter should be a setting thunk *) + match eval arg with Clos c -> c | _ -> raise Type_error + in + + let self_path = perform Rd_path in + if Tree_path.(path = self_path) then ( + (* Set self's state *) + perform + (Set_dec + (match perform Rd_phase with P_effect -> Update | _ -> Retry)); + + let v, q = perform (Lookup_st label) in + perform (Update_st (label, (v, Job_q.enqueue q clos))); + Unit) + else ( + (* Set other's state *) + perform (Part_view_set_dec (path, label, Update)); + perform (Part_view_enq_set (path, label, clos)); + Unit) + | _ -> raise Type_error) + | Let { id; bound; body } -> + let value = eval bound in + let env = Env.extend (perform Rd_env) ~id ~value in + perform (In_env env) eval body + | Stt { label; stt; set; init; body } -> ( + let path = perform Rd_path in + match perform Rd_phase with + | P_init -> + let v = eval init in + perform (Update_st (label, (v, empty_setq))); + let env = + perform Rd_env + |> Env.extend ~id:stt ~value:v + |> Env.extend ~id:set ~value:(Set_clos { label; path }) + in + perform (In_env env) eval body + | P_update | P_retry -> + let v_prev, q = perform (Lookup_st label) in + (* Run the setting thunks in the set queue *) + let v_curr = + Job_q.fold q ~init:v_prev ~f:(fun value { param; body; env } -> + let env = Env.extend env ~id:param ~value in + perform (In_env env) eval body) + in + if v_prev <> v_curr then perform (Set_dec Update); + perform (Update_st (label, (v_curr, Job_q.empty))); + let env = + perform Rd_env + |> Env.extend ~id:stt ~value:v_curr + |> Env.extend ~id:set ~value:(Set_clos { label; path }) + in + perform (In_env env) eval body + | P_effect -> raise Invalid_phase) + | Eff e -> ( + match perform Rd_phase with + | P_effect -> raise Invalid_phase + | _ -> + perform (Enq_eff { param = Id.unit; body = e; env = perform Rd_env }); + Unit) + | Seq (e1, e2) -> + eval e1 |> ignore; + eval e2 + | Bin_op { op; left; right } -> ( + let v1 = eval left in + let v2 = eval right in + match (op, v1, v2) with + | Plus, Int i1, Int i2 -> Int (i1 + i2) + | Minus, Int i1, Int i2 -> Int (i1 - i2) + | Times, Int i1, Int i2 -> Int (i1 * i2) + | _, _, _ -> raise Type_error) diff --git a/lib/syntax.ml b/lib/syntax.ml new file mode 100644 index 0000000..3fe87b7 --- /dev/null +++ b/lib/syntax.ml @@ -0,0 +1,60 @@ +open! Base + +module Id = struct + module T = String + include T + + module Map = struct + open Map + include M (T) + + let empty = empty (module T) + end + + let unit = "()" +end + +module Label = struct + module T = Int + include T + + module Map = struct + open Map + include M (T) + + let empty = empty (module T) + end +end + +type hook_free = private Hook_free +type hook_full = private Hook_full + +module Expr = struct + type _ t = + | Const : const -> _ t + | Var : Id.t -> _ t + | View : hook_free t list -> _ t + | Cond : { pred : hook_free t; con : hook_free t; alt : hook_free t } -> _ t + | Fn : { param : Id.t; body : hook_free t } -> _ t + | App : { fn : hook_free t; arg : hook_free t } -> _ t + | Let : { id : Id.t; bound : hook_free t; body : _ t } -> _ t + | Stt : { + label : Label.t; + stt : Id.t; + set : Id.t; + init : hook_free t; + body : hook_full t; + } + -> hook_full t + | Eff : hook_free t -> hook_full t + | Seq : 'a t * 'a t -> 'a t + | Bin_op : { op : bin_op; left : hook_free t; right : hook_free t } -> _ t + + and const = Unit of unit | Int of int + and bin_op = Plus | Minus | Times +end + +module Prog = struct + type t = Expr of hook_free Expr.t | Comp of (comp * t) + and comp = { name : Id.t; param : Id.t; body : hook_full Expr.t } +end diff --git a/react_trace.opam b/react_trace.opam new file mode 100644 index 0000000..af55292 --- /dev/null +++ b/react_trace.opam @@ -0,0 +1,34 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "React Analyzer" +description: "ReacttRace is a tool for analyzing React programs." +maintainer: ["Jay Lee"] +authors: ["Jay Lee"] +license: "LICENSE" +tags: ["React" "Static Analysis"] +homepage: "https://github.com/React-Analysis/ReacttRace" +bug-reports: "https://github.com/React-Analysis/ReacttRace/issues" +depends: [ + "ocaml" + "dune" {>= "3.15"} + "ocaml-variants" {= "5.1.1+effect-syntax"} + "base" + "logs" + "stdio" + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/React-Analysis/ReacttRace.git" diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..7574c10 --- /dev/null +++ b/test/dune @@ -0,0 +1,2 @@ +(test + (name test_react_trace)) diff --git a/test/test_react_trace.ml b/test/test_react_trace.ml new file mode 100644 index 0000000..e69de29