Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Refactor simple program analysis
Browse files Browse the repository at this point in the history
robertzhidealx committed Dec 25, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent 628eb83 commit 50af9b7
Showing 23 changed files with 10,895 additions and 1,196 deletions.
4 changes: 2 additions & 2 deletions dde.opam
Original file line number Diff line number Diff line change
@@ -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 <[email protected]>"]
authors: ["JHU PL Lab <[email protected]>"]
homepage: "https://github.com/JHU-PL-Lab/dde"
4 changes: 2 additions & 2 deletions dune-project
Original file line number Diff line number Diff line change
@@ -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))
6 changes: 4 additions & 2 deletions interpreter/src/ast.ml
Original file line number Diff line number Diff line change
@@ -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)
10,196 changes: 10,196 additions & 0 deletions logs

Large diffs are not rendered by default.

9 changes: 4 additions & 5 deletions program_analysis/display/lib.ml
Original file line number Diff line number Diff line change
@@ -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);
20 changes: 20 additions & 0 deletions program_analysis/simple/debug_utils.ml
Original file line number Diff line number Diff line change
@@ -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
20 changes: 0 additions & 20 deletions program_analysis/simple/debugutils.ml

This file was deleted.

4 changes: 2 additions & 2 deletions program_analysis/simple/dune
Original file line number Diff line number Diff line change
@@ -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)))
3 changes: 3 additions & 0 deletions program_analysis/simple/exns.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
exception Unreachable
exception BadAssert
exception Runtime_error
173 changes: 0 additions & 173 deletions program_analysis/simple/grammar.ml

This file was deleted.

Loading

0 comments on commit 50af9b7

Please sign in to comment.