Refactor simple program analysis

dde.opam

@@ -1,8 +1,8 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-synopsis: "Demand-Driven Execution (DDE)"
+synopsis: "Pure Demand Operational Semantics"
 description:
-  "Formally verified concrete and abstract interpretation based on DDE"
+  "A novel minimal-state operational semantics for higher-order functional languages"
 maintainer: ["JHU PL Lab <scott@cs.jhu.edu>"]
 authors: ["JHU PL Lab <scott@cs.jhu.edu>"]
 homepage: "https://github.com/JHU-PL-Lab/dde"

dune-project

@@ -17,9 +17,9 @@
 
 (package
  (name dde)
- (synopsis "Demand-Driven Execution (DDE)")
+ (synopsis "Pure Demand Operational Semantics")
  (description
-  "Formally verified concrete and abstract interpretation based on DDE")
+  "A novel minimal-state operational semantics for higher-order functional languages")
  (depends
   (ocaml
    (>= 4.14.1))

interpreter/src/ast.ml

@@ -255,7 +255,7 @@ let rec trans_let x e' e =
 let rec transform_let e =
   (* TODO: more cases *)
   match e with
-  | Int _ | Bool _ -> e
+  | Int _ | Bool _ | Var _ -> e
   | Function (ident, e, l) ->
       let e' = transform_let e in
       let f = Function (ident, e', l) in
@@ -296,4 +296,6 @@ let rec transform_let e =
   | And (e1, e2) -> And (transform_let e1, transform_let e2)
   | Or (e1, e2) -> Or (transform_let e1, transform_let e2)
   | Not e -> Not (transform_let e)
-  | _ -> e
+  | Record es -> Record (List.map es ~f:(fun (id, e) -> (id, transform_let e)))
+  | Projection (e, id) -> Projection (transform_let e, id)
+  | Inspection (id, e) -> Inspection (id, transform_let e)

program_analysis/display/lib.ml

@@ -7,7 +7,6 @@ open Grammar
 open Grammar.DAtom
 open Utils
 open Pa.Exns
-open Pa.Logging
 
 let rec prune_d ?(k = 1) d =
   map_d d ~f:(fun (l, d) -> (l, if k = 0 then DNil else prune_d d ~k:(k - 1)))
@@ -99,7 +98,7 @@ let rec analyze expr d s sfrag v level =
           debug (fun m -> m "Stubbed DApp");
           (dres_singleton (DStubAtom stub_key), s, sfrag))
         else (
-          debug_plain "Didn't stub DApp";
+          debug (fun m -> m "Didn't stub DApp");
           debug (fun m -> m "Key (expr): %d" (get_label expr));
           debug (fun m -> m "Key (D): %a" Pp.pp_d d);
           debug (fun m -> m "Key (S): %a" pp_s s);
@@ -142,7 +141,7 @@ let rec analyze expr d s sfrag v level =
               m "[Level %d] Stubbed DVar (%a)" level Pp.pp_expr expr);
           (dres_singleton (DStubAtom stub_key), s, sfrag))
         else (
-          debug_plain "Didn't stub DVar";
+          debug (fun m -> m "Didn't stub DVar");
           debug (fun m -> m "Key (expr): %a" Pp.pp_expr expr);
           debug (fun m -> m "Key (D): %a" Pp.pp_d d);
           debug (fun m -> m "Key (S): %a" pp_s s);
@@ -170,7 +169,7 @@ let rec analyze expr d s sfrag v level =
             (* if not (m < length_d d1) then acc
                else if m - 1 >= 0 then (
                  let l_app, d = nth_exn_d d m in
-                 debug_plain "m - 1 case";
+                 debug (fun m -> m "m - 1 case";
                  let l_app', d' = nth_exn_d d1 (m - 1) in
                  if l_app = l_app' then (
                    debug (fun m ->
@@ -190,7 +189,7 @@ let rec analyze expr d s sfrag v level =
                    | _ -> raise Unreachable)
                  else acc)
                else if matches_d d d1 then (
-                 debug_plain "m case";
+                 debug (fun m -> m "m case";
                  debug (fun m ->
                      m "[Level %d][DVar (%a)] Stitched!" level Pp.pp_expr expr);
                  debug (fun m_ -> m_ "Accessing index %d of %a" m Pp.pp_d d1);

program_analysis/simple/debug_utils.ml

@@ -0,0 +1,20 @@
+let report_runtime = ref false
+
+let parse s =
+  s |> Core.Fn.flip ( ^ ) ";;" |> Lexing.from_string
+  |> Interp.Parser.main Interp.Lexer.token
+
+let parse_analyze ?(name = "test") s =
+  s |> parse |> Lib.analyze |> fun (r, runtime) ->
+  if !report_runtime then Format.printf "%s: %f\n" name runtime;
+  r
+
+let unparse = Format.asprintf "%a" Utils.Res.pp
+
+let parse_analyze_unparse ?(name = "test") s =
+  s |> parse_analyze ~name |> unparse
+
+let pau = parse_analyze_unparse
+
+let parse_analyze_print s =
+  s |> parse_analyze |> Format.printf "==> %a\n" Utils.Res.pp

program_analysis/simple/dune

@@ -3,7 +3,7 @@
  (public_name dde.simple_pa)
  (preprocess
   (pps ppx_deriving.show ppx_let ppx_jane landmarks-ppx --auto))
- (modules lib grammar solver simplifier utils debugutils)
- (libraries hashset core z3 logs logs.fmt dde.interp dde.pa)
+ (modules lib utils simplifier debug_utils exns)
+ (libraries core logs logs.fmt dde.interp)
  (instrumentation
   (backend landmarks --auto)))

program_analysis/simple/exns.ml

@@ -0,0 +1,3 @@
+exception Unreachable
+exception BadAssert
+exception Runtime_error