From ebb51eba132f68454233a977eda24db8d39d5394 Mon Sep 17 00:00:00 2001 From: Robert Zhang Date: Wed, 1 Nov 2023 14:21:55 -0400 Subject: [PATCH] Remove FbDK boilerplate + general refactoring --- dde.opam | 2 + dune-project | 6 +- interpreter/src/debugutils.ml | 14 +- interpreter/src/dune | 10 +- interpreter/src/fbdk.ml | 9 - interpreter/src/fbdk.mli | 119 --- interpreter/src/{interp.ml => lib.ml} | 0 interpreter/src/main.ml | 67 +- interpreter/src/options.ml | 1 - interpreter/src/pp.ml | 8 +- interpreter/src/type.ml | 20 - interpreter/tests/dune | 2 +- interpreter/tests/utils.ml | 8 +- program_analysis/display/dune | 2 +- program_analysis/display/lib.ml | 11 +- program_analysis/reworked/lib.ml | 689 ------------------ program_analysis/reworked/simplifier.ml | 40 - program_analysis/reworked/utils.ml | 531 -------------- .../{reworked => simple}/debugutils.ml | 5 +- program_analysis/{reworked => simple}/dune | 6 +- .../{reworked => simple}/grammar.ml | 31 +- program_analysis/simple/lib.ml | 566 ++++++++++++++ program_analysis/simple/simplifier.ml | 59 ++ .../{reworked => simple}/solver.ml | 0 program_analysis/simple/utils.ml | 82 +++ program_analysis/src/debugutils.ml | 5 +- program_analysis/src/dune | 10 +- program_analysis/src/exns.ml | 3 + program_analysis/src/grammar.ml | 6 +- program_analysis/src/lib.ml | 76 +- program_analysis/src/logging.ml | 9 + program_analysis/src/main.ml | 4 +- program_analysis/src/simplifier.ml | 65 +- program_analysis/src/solver.ml | 2 +- program_analysis/src/utils.ml | 11 +- program_analysis/tests/dune | 6 +- program_analysis/tests/test_cases.ml | 2 +- program_analysis/tests/tests.ml | 205 +++--- program_analysis/tests/utils.ml | 35 +- 39 files changed, 1011 insertions(+), 1716 deletions(-) delete mode 100644 interpreter/src/fbdk.ml delete mode 100644 interpreter/src/fbdk.mli rename interpreter/src/{interp.ml => lib.ml} (100%) delete mode 100644 interpreter/src/options.ml delete mode 100644 interpreter/src/type.ml delete mode 100644 program_analysis/reworked/lib.ml delete mode 100644 program_analysis/reworked/simplifier.ml delete mode 100644 program_analysis/reworked/utils.ml rename program_analysis/{reworked => simple}/debugutils.ml (78%) rename program_analysis/{reworked => simple}/dune (63%) rename program_analysis/{reworked => simple}/grammar.ml (86%) create mode 100644 program_analysis/simple/lib.ml create mode 100644 program_analysis/simple/simplifier.ml rename program_analysis/{reworked => simple}/solver.ml (100%) create mode 100644 program_analysis/simple/utils.ml create mode 100644 program_analysis/src/exns.ml create mode 100644 program_analysis/src/logging.ml diff --git a/dde.opam b/dde.opam index da0112d..5a29774 100644 --- a/dde.opam +++ b/dde.opam @@ -22,6 +22,8 @@ depends: [ "core_bench" {>= "0.15.0"} "core_unix" {>= "0.15.2"} "hashset" {>= "1.0.0"} + "fmt" {>= "0.9.0"} + "landmarks" {>= "1.4"} "odoc" {with-doc} ] build: [ diff --git a/dune-project b/dune-project index d0ab9df..a9672b5 100644 --- a/dune-project +++ b/dune-project @@ -48,4 +48,8 @@ (core_unix (>= 0.15.2)) (hashset - (>= 1.0.0)))) + (>= 1.0.0)) + (fmt + (>= 0.9.0)) + (landmarks + (>= 1.4)))) diff --git a/interpreter/src/debugutils.ml b/interpreter/src/debugutils.ml index 1b08f74..e1f4f80 100644 --- a/interpreter/src/debugutils.ml +++ b/interpreter/src/debugutils.ml @@ -2,28 +2,28 @@ let is_debug_mode = ref false let should_simplify = ref false -let eval = Fbdk.Interpreter.eval +let eval = Lib.eval let parse s = let lexbuf = Lexing.from_string (s ^ ";;") in - Fbdk.Parser.main Fbdk.Lexer.token lexbuf + Parser.main Lexer.token lexbuf -let unparse v = Format.asprintf "%a" Fbdk.Pp.pp_result_value v +let unparse v = Format.asprintf "%a" Pp.pp_result_value v let parse_eval s = - Fbdk.Interpreter.eval (parse s) ~is_debug_mode:!is_debug_mode + Lib.eval (parse s) ~is_debug_mode:!is_debug_mode ~should_simplify:!should_simplify let parse_eval_unparse s = unparse - @@ Fbdk.Interpreter.eval (parse s) ~is_debug_mode:!is_debug_mode + @@ Lib.eval (parse s) ~is_debug_mode:!is_debug_mode ~should_simplify:!should_simplify let peu = parse_eval_unparse let parse_eval_print s = - Format.printf "==> %a\n" Fbdk.Pp.pp_result_value - (Fbdk.Interpreter.eval (parse s) ~is_debug_mode:!is_debug_mode + Format.printf "==> %a\n" Pp.pp_result_value + (Lib.eval (parse s) ~is_debug_mode:!is_debug_mode ~should_simplify:!should_simplify) (* let pp s = s |> parse |> unparse |> print_string |> print_newline *) diff --git a/interpreter/src/dune b/interpreter/src/dune index 44e8caa..f0eec2e 100644 --- a/interpreter/src/dune +++ b/interpreter/src/dune @@ -1,11 +1,11 @@ (library - (name interpreter) - (public_name dde.interpreter) + (name interp) + (public_name dde.interp) (preprocess (pps ppx_deriving.show bisect_ppx ppx_jane)) (instrumentation (backend bisect_ppx --bisect-file _build/bisect)) - (modules fbdk debugutils ast type interp lexer options parser pp) + (modules lexer parser ast lib pp debugutils) (libraries core hashcons)) (ocamllex @@ -18,11 +18,11 @@ (name main) (modes byte) (modules main) - (libraries interpreter)) + (libraries interp)) (toplevel (name toplevel) - (libraries utop interpreter)) + (libraries utop interp)) (alias (name distributables) diff --git a/interpreter/src/fbdk.ml b/interpreter/src/fbdk.ml deleted file mode 100644 index 28c9a44..0000000 --- a/interpreter/src/fbdk.ml +++ /dev/null @@ -1,9 +0,0 @@ -let name = "DDE" - -module Parser = Parser -module Lexer = Lexer -module Ast = Ast -module Pp = Pp -module Options = Options -module Interpreter = Interp -module Typechecker = Type diff --git a/interpreter/src/fbdk.mli b/interpreter/src/fbdk.mli deleted file mode 100644 index 435a9cc..0000000 --- a/interpreter/src/fbdk.mli +++ /dev/null @@ -1,119 +0,0 @@ -val name : string - -module Ast : sig - type ident = Ast.ident = Ident of string - - type expr = - | Int of int - | Bool of bool - | Function of ident * expr * int - | Var of ident * int - | Appl of expr * expr * int - | Plus of expr * expr - | Minus of expr * expr - | Mult of expr * expr - | Equal of expr * expr - | And of expr * expr - | Or of expr * expr - | Ge of expr * expr - | Gt of expr * expr - | Le of expr * expr - | Lt of expr * expr - | Not of expr - | If of expr * expr * expr * int - | Let of ident * expr * expr * int - | LetAssert of ident * expr * expr - | Record of (ident * expr) list - | Projection of expr * ident - | Inspection of ident * expr - - type sigma = int list - - type op_result_value = - | PlusOp of result_value * result_value - | MinusOp of result_value * result_value - | MultOp of result_value * result_value - | EqOp of result_value * result_value - | AndOp of result_value * result_value - | OrOp of result_value * result_value - | GeOp of result_value * result_value - | GtOp of result_value * result_value - | LeOp of result_value * result_value - | LtOp of result_value * result_value - | NotOp of result_value - - and result_value = - | IntResult of int - | BoolResult of bool - | FunResult of { f : expr; l : int; sigma : int list } - | OpResult of op_result_value - | RecordResult of (ident * result_value) list - - type res_val_fv = - | IntResFv of int - | BoolResFv of bool - | VarResFv of ident - | PlusResFv of res_val_fv * res_val_fv - | MinusResOpFv of res_val_fv * res_val_fv - | EqResFv of res_val_fv * res_val_fv - | AndResFv of res_val_fv * res_val_fv - | OrResFv of res_val_fv * res_val_fv - | GeResFv of res_val_fv * res_val_fv - | GtResFv of res_val_fv * res_val_fv - | LeResFv of res_val_fv * res_val_fv - | LtResFv of res_val_fv * res_val_fv - | NotResFv of res_val_fv - (* TODO: not even needed? *) - | FunResFv - | RecResFv of (ident * res_val_fv) list - | ProjResFv of res_val_fv * ident - | InspResFv - - type fbtype = Ast.fbtype = TArrow of fbtype * fbtype | TVar of string - - val show_expr : expr -> string - val pp_expr : Format.formatter -> expr -> unit [@@ocaml.toplevel_printer] - val show_fbtype : fbtype -> string - val pp_fbtype : Format.formatter -> fbtype -> unit [@@ocaml.toplevel_printer] -end - -module Parser : sig - type token - - val main : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ast.expr -end - -module Lexer : sig - val token : Lexing.lexbuf -> Parser.token -end - -module Typechecker : sig - (* This exception is used to allow a language to dynamically signal that it *) - (* does not have a typechecker. If it is raised, it should be raised by a *) - (* Typechecker module's typecheck function. *) - exception TypecheckerNotImplementedException - - val typecheck : Ast.expr -> Ast.fbtype - val typecheck_default_enabled : bool -end - -module Interpreter : sig - val eval : - ?should_cache:bool -> - is_debug_mode:bool -> - should_simplify:bool -> - Ast.expr -> - Ast.result_value -end - -module Pp : sig - val show_expr : Ast.expr -> string - val pp_expr : Format.formatter -> Ast.expr -> unit - val pp_result_value : Format.formatter -> Ast.result_value -> unit - val show_fbtype : Ast.fbtype -> string - val pp_fbtype : Format.formatter -> Ast.fbtype -> unit -end - -module Options : sig - val options : (Arg.key * Arg.spec * Arg.doc) list -end diff --git a/interpreter/src/interp.ml b/interpreter/src/lib.ml similarity index 100% rename from interpreter/src/interp.ml rename to interpreter/src/lib.ml diff --git a/interpreter/src/main.ml b/interpreter/src/main.ml index 3c0d756..6dec853 100644 --- a/interpreter/src/main.ml +++ b/interpreter/src/main.ml @@ -1,4 +1,4 @@ -open Interpreter +open Interp let toplevel_loop typechecking_enabled show_types is_debug_mode should_simplify = @@ -19,33 +19,18 @@ let toplevel_loop typechecking_enabled show_types is_debug_mode should_simplify let safe_parse () = try let lexbuf = Lexing.from_channel stdin in - Some (Fbdk.Parser.main Fbdk.Lexer.token lexbuf) + Some (Parser.main Lexer.token lexbuf) with | Exit -> exit 0 | ex -> print_exception ex; None in - (* Type check if enabled and return the result. The result is a false *) - (* only if it is enabled and type checking throws an exception (fails) *) - let safe_typecheck ast = - try - if typechecking_enabled then ( - let exprtype = Fbdk.Typechecker.typecheck ast in - if show_types then Format.printf " : %a\n" Fbdk.Pp.pp_fbtype exprtype; - true) - else true - with - | Fbdk.Typechecker.TypecheckerNotImplementedException -> true - | ex -> - print_exception ex; - false - in (* Interpret and print. Exceptions are caught and reported. But the toploop is not aborted *) let safe_interpret_and_print ast = try - let result = Fbdk.Interpreter.eval ast ~is_debug_mode ~should_simplify in - Format.printf "==> %a\n" Fbdk.Pp.pp_result_value result + let result = Lib.eval ast ~is_debug_mode ~should_simplify in + Format.printf "==> %a\n" Pp.pp_result_value result with ex -> print_exception ex in Format.printf "\t(typechecker %s)\n\n" @@ -58,50 +43,50 @@ let toplevel_loop typechecking_enabled show_types is_debug_mode should_simplify match parse_result with | None -> () | Some ast -> - if safe_typecheck ast then safe_interpret_and_print ast else (); + safe_interpret_and_print ast; Format.print_flush () done let run_file filename is_debug_mode should_simplify = let fin = open_in filename in let lexbuf = Lexing.from_channel fin in - let ast = Fbdk.Parser.main Fbdk.Lexer.token lexbuf in - let result = Fbdk.Interpreter.eval ast ~is_debug_mode ~should_simplify in - Format.printf "%a\n" Fbdk.Pp.pp_result_value result; + let ast = Parser.main Lexer.token lexbuf in + let result = Lib.eval ast ~is_debug_mode ~should_simplify in + Format.printf "%a\n" Pp.pp_result_value result; Format.print_flush () let main () = let filename = ref "" in let toplevel = ref true in let version = ref false in - let no_typechecking = ref (not Fbdk.Typechecker.typecheck_default_enabled) in + let no_typechecking = ref false in + (* let no_typechecking = ref (not Fbdk.Typechecker.typecheck_default_enabled) in *) let no_type_display = ref false in let show_exception_stack_trace = ref false in let is_debug_mode = ref false in let should_simplify = ref false in Arg.parse - ([ - ("--typecheck", Arg.Clear no_typechecking, "enable typechecking"); - ("--no-typecheck", Arg.Set no_typechecking, "disable typechecking"); - ("--hide-types", Arg.Set no_type_display, "disable displaying of types"); - ( "--show-backtrace", - Arg.Set show_exception_stack_trace, - "Enable the display of exception stack traces" ); - ( "--debug", - Arg.Set is_debug_mode, - "output debug information from evaluation" ); - ( "--simplify", - Arg.Set should_simplify, - "eagerly simplify (substitute free variables, perform function \ - application, etc.)result" ); - ] - @ Fbdk.Options.options) + [ + ("--typecheck", Arg.Clear no_typechecking, "enable typechecking"); + ("--no-typecheck", Arg.Set no_typechecking, "disable typechecking"); + ("--hide-types", Arg.Set no_type_display, "disable displaying of types"); + ( "--show-backtrace", + Arg.Set show_exception_stack_trace, + "Enable the display of exception stack traces" ); + ( "--debug", + Arg.Set is_debug_mode, + "output debug information from evaluation" ); + ( "--simplify", + Arg.Set should_simplify, + "eagerly simplify (substitute free variables, perform function \ + application, etc.)result" ); + ] (function | fname -> filename := fname; version := false; toplevel := false) - ("Usage: " ^ Fbdk.name ^ " [ options ] [ filename ]\noptions:"); + "Usage: Interp [ options ] [ filename ]\noptions:"; Printexc.record_backtrace !show_exception_stack_trace; diff --git a/interpreter/src/options.ml b/interpreter/src/options.ml deleted file mode 100644 index d619ee9..0000000 --- a/interpreter/src/options.ml +++ /dev/null @@ -1 +0,0 @@ -let options = [] diff --git a/interpreter/src/pp.ml b/interpreter/src/pp.ml index 82b30dd..3a6c09d 100644 --- a/interpreter/src/pp.ml +++ b/interpreter/src/pp.ml @@ -12,7 +12,7 @@ let is_compound_expr = function Var _ -> false | _ -> true let rec pp_expr fmt = function | Int i -> ff fmt "%d" i | Bool b -> ff fmt "%b" b - | Function (Ident i, x, l) -> ff fmt "@[fun %s ->@;<1 4>%a@]" i pp_expr x + | Function (Ident i, x, l) -> ff fmt "@[fun %s ->@;<0 2>%a@]" i pp_expr x | Var (Ident x, l) -> ff fmt "%s" x | Appl (e1, e2, _) -> let is_compound_exprL = function @@ -36,7 +36,7 @@ let rec pp_expr fmt = function | Lt (e1, e2) -> ff fmt "(%a < %a)" pp_expr e1 pp_expr e2 | Not e1 -> ff fmt "(not %a)" pp_expr e1 | If (e1, e2, e3, _) -> - ff fmt "@[if %a then@;<1 4>%a@;<1 0>else@;<1 4>%a@]" pp_expr e1 + ff fmt "@[if %a then@;<1 2>%a@;<1 0>else@;<1 2>%a@]" pp_expr e1 pp_expr e2 pp_expr e3 | Let (Ident i, e1, e2, _) -> ff fmt "@[let %s =@;<1 4>%a@;<1 0>in@;<1 4>%a@]" i pp_expr e1 pp_expr @@ -102,6 +102,4 @@ let rec pp_res_val_fv fmt = function | BoolResFv b -> ff fmt "%b" b | VarResFv (Ident x) -> ff fmt "%s" x | GeResFv (v1, v2) -> ff fmt "%a > %a" pp_res_val_fv v1 pp_res_val_fv v2 - | v -> - (* Format.printf "%a" Ast.pp_res_val_fv v *) - () + | _ -> () diff --git a/interpreter/src/type.ml b/interpreter/src/type.ml deleted file mode 100644 index 58819d5..0000000 --- a/interpreter/src/type.ml +++ /dev/null @@ -1,20 +0,0 @@ -[@@@coverage off] - -open Ast - -exception TypecheckerNotImplementedException - -(* - * If you would like typechecking to be enabled by your interpreter by default, - * then change the following value to true. Whether or not typechecking is - * enabled by default, you can explicitly enable it or disable it using - * command-line arguments. - *) -let typecheck_default_enabled = false - -(* - * Replace this with your typechecker code. Your code should not throw the - * following exception; if you need to raise an exception, create your own - * exception type here. - *) -let typecheck e = raise TypecheckerNotImplementedException diff --git a/interpreter/tests/dune b/interpreter/tests/dune index 2bda139..363704f 100644 --- a/interpreter/tests/dune +++ b/interpreter/tests/dune @@ -5,7 +5,7 @@ ounit2 core_bench core_unix.command_unix - dde.interpreter + dde.interp dde.dinterp fbdk.fb fbdk.fbenv)) diff --git a/interpreter/tests/utils.ml b/interpreter/tests/utils.ml index b11c875..962f2d7 100644 --- a/interpreter/tests/utils.ml +++ b/interpreter/tests/utils.ml @@ -1,4 +1,4 @@ -open Interpreter +open Interp exception Unreachable @@ -58,12 +58,12 @@ let dde_to_fbenv (v : Ast.result_value) : Fbenvast.expr = let dde_eval_fb s = Lexing.from_string s |> Parser.main Lexer.token - |> Interp.eval ~is_debug_mode:false ~should_simplify:true + |> Lib.eval ~is_debug_mode:false ~should_simplify:true |> dde_to_fb let dde_eval_fbenv s = Lexing.from_string s |> Parser.main Lexer.token - |> Interp.eval ~is_debug_mode:false ~should_simplify:true + |> Lib.eval ~is_debug_mode:false ~should_simplify:true |> dde_to_fbenv let dde_parse s = @@ -82,5 +82,5 @@ let assert_unequal e1 e2 = OUnit2.assert_equal ~cmp:(fun a b -> a <> b) e1 e2 let peu ?(should_simplify = false) s = s |> Core.Fn.flip ( ^ ) ";;" |> Lexing.from_string |> Parser.main Lexer.token - |> Interp.eval ~is_debug_mode:false ~should_simplify + |> Lib.eval ~is_debug_mode:false ~should_simplify |> Format.asprintf "%a" Pp.pp_result_value diff --git a/program_analysis/display/dune b/program_analysis/display/dune index dd4e92f..1224b7b 100644 --- a/program_analysis/display/dune +++ b/program_analysis/display/dune @@ -8,7 +8,7 @@ (instrumentation (backend landmarks --auto)) (modules lib grammar debugutils utils simplifier) - (libraries dde.dinterp core logs logs.fmt core_unix)) + (libraries core logs logs.fmt core_unix dde.dinterp dde.pa)) ; (executable ; (name main) diff --git a/program_analysis/display/lib.ml b/program_analysis/display/lib.ml index 349fca9..d81d201 100644 --- a/program_analysis/display/lib.ml +++ b/program_analysis/display/lib.ml @@ -6,15 +6,8 @@ open Dinterp.Interp open Grammar open Grammar.DAtom open Utils - -exception Unreachable -exception Runtime_error - -let gen_logs = ref false -let debug_plain msg = if !gen_logs then debug (fun m -> m msg) -let debug msg = if !gen_logs then debug msg -let info_plain msg = if !gen_logs then info msg -let info msg = if !gen_logs then info msg +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))) diff --git a/program_analysis/reworked/lib.ml b/program_analysis/reworked/lib.ml deleted file mode 100644 index 1af88b2..0000000 --- a/program_analysis/reworked/lib.ml +++ /dev/null @@ -1,689 +0,0 @@ -open Core -open Logs -open Option.Let_syntax -open Interpreter.Ast -open Grammar -open Utils -open Solver -open Simplifier - -exception Unreachable -exception BadAssert -exception Runtime_error - -let empty_choice_set = Set.empty (module Choice) - -(* controls whether to generate logs: - "logs" in _build/default/program_analysis/tests *) -let gen_logs = ref false -let debug_plain msg = if !gen_logs then debug (fun m -> m msg) -let debug msg = if !gen_logs then debug msg -let info_plain msg = if !gen_logs then info msg -let info msg = if !gen_logs then info msg - -(* maximum recursion depth ever reached by execution so far *) -let max_d = ref 0 - -let rec eval_assert_aux e = - match e with - | Int i -> IntResFv i - | Bool b -> BoolResFv b - | Plus (e1, e2) - | Minus (e1, e2) - | Equal (e1, e2) - | Ge (e1, e2) - | Gt (e1, e2) - | Le (e1, e2) - | Lt (e1, e2) -> ( - match (eval_assert_aux e1, eval_assert_aux e2) with - | IntResFv i1, IntResFv i2 -> ( - match e with - | Plus _ -> IntResFv (i1 + i2) - | Minus _ -> IntResFv (i1 - i2) - | Equal _ -> BoolResFv (i1 = i2) - | Ge _ -> BoolResFv (i1 >= i2) - | Gt _ -> BoolResFv (i1 > i2) - | Le _ -> BoolResFv (i1 <= i2) - | Lt _ -> BoolResFv (i1 < i2) - | _ -> raise Unreachable) - | _ -> raise Unreachable) - | And (e1, e2) | Or (e1, e2) -> ( - match (eval_assert_aux e1, eval_assert_aux e2) with - | BoolResFv b1, BoolResFv b2 -> ( - match e with - | And _ -> BoolResFv (b1 && b2) - | Or _ -> BoolResFv (b1 || b2) - | _ -> raise Unreachable) - | _ -> raise Unreachable) - | Not e -> ( - match eval_assert_aux e with - | BoolResFv b -> BoolResFv (not b) - | _ -> raise Unreachable) - | _ -> - Format.printf "%a" Interpreter.Pp.pp_expr e; - raise BadAssert - -(** only allows the following forms: - - arbitrary variable-free arithmetic - - - - not - - *) -let eval_assert e id = - match e with - | Bool b -> BoolResFv b - | Var (id', _) when Stdlib.(id = id') -> VarResFv id' - | Equal (e1, e2) | Ge (e1, e2) | Gt (e1, e2) | Le (e1, e2) | Lt (e1, e2) -> ( - match e1 with - | Var (id', _) when Stdlib.(id = id') -> ( - let v1 = VarResFv id' in - let v2 = eval_assert_aux e2 in - match e with - | Equal _ -> EqResFv (v1, v2) - | Ge _ -> GeResFv (v1, v2) - | Gt _ -> GtResFv (v1, v2) - | Le _ -> LeResFv (v1, v2) - | Lt _ -> LtResFv (v1, v2) - | _ -> raise Unreachable) - | Projection (e1, x) -> failwith "Not supported" - | _ -> ( - let v1, v2 = (eval_assert_aux e1, eval_assert_aux e2) in - match (v1, v2) with - | IntResFv i1, IntResFv i2 -> ( - match e with - | Equal _ -> BoolResFv (i1 = i2) - | Ge _ -> BoolResFv (i1 >= i2) - | Gt _ -> BoolResFv (i1 > i2) - | Le _ -> BoolResFv (i1 <= i2) - | Lt _ -> BoolResFv (i1 < i2) - | _ -> raise Unreachable) - | _ -> raise BadAssert)) - (* TODO: support And/Or (low priority) *) - | Not e' -> ( - match e' with - | Var (id', _) when Stdlib.(id = id') -> NotResFv (VarResFv id') - | _ -> eval_assert_aux e') - | _ -> raise BadAssert - -let log_v_set = Set.iter ~f:(fun st -> debug (fun m -> m "%s" (NewSt.show st))) - -let rec fold_res_app ~init ~f l sigma d = - List.fold ~init ~f:(fun ((acc_r, acc_s) as acc) a -> - debug (fun m -> - m "[Level %d] [Appl] Evaluating 1 possible function being applied:" d); - debug (fun m -> m "%a" pp_atom a); - (* debug (fun m -> m "%a" Grammar.pp_atom a); *) - match a with - | FunAtom (Function (_, e1, _), _, _) -> f acc e1 - | _ -> - debug (fun m -> m "Not a function, skipping: %a" pp_atom a); - (acc_r, acc_s)) - -let rec fold_res_var ~init ~f expr sigma d r = - List.fold r ~init ~f:(fun ((acc_r, acc_s) as acc) a -> - debug (fun m -> m "r1 length: %d" (List.length r)); - debug (fun m -> m "[Level %d] Visiting 1 possible function for e1:" d); - debug (fun m -> m "%a" pp_atom a); - (* debug (fun m -> m "%a" Grammar.pp_atom a); *) - match a with - | FunAtom (Function (Ident x1, _, l1), _, sigma1) -> f acc x1 l1 sigma1 - | _ -> - debug (fun m -> m "Not a function, skipping: %a" pp_atom a); - (acc_r, acc_s)) - -let rec exists_stub r label = - List.exists r ~f:(function - | FunAtom _ | IntAllAtom | IntAtom _ | BoolAtom _ -> false - | LabelStubAtom st -> St.(label = St.Lstate st) - | ExprStubAtom st -> St.(label = St.Estate st) - | RecordAtom entries -> - List.exists entries ~f:(fun (_, r) -> exists_stub r label) - | ProjectionAtom (r, _) | InspectionAtom (_, r) -> exists_stub r label - | _ as a -> - Format.printf "%a" pp_atom a; - failwith "unimplemented") - -let elim_stub r label = - if exists_stub r label then - (* Format.printf "elim_stub: %a\n" pp_res r; *) - (* Format.printf "label: %a\n" St.pp label; *) - let bases = - List.filter_map r ~f:(fun a -> - match a with - | RecordAtom _ when not (exists_stub [ a ] label) -> Some a - | ProjectionAtom (([ RecordAtom es ] as r), Ident key) - when not (exists_stub r label) -> ( - match - List.find es ~f:(fun (Ident key', _) -> String.(key = key')) - with - | Some (_, [ a ]) -> Some a - | _ -> raise Runtime_error) - | FunAtom _ -> Some a - | _ -> None) - in - let r' = - List.concat_map r ~f:(function - | ProjectionAtom ([ ExprStubAtom st ], Ident key) - when St.(label = Estate st) -> - List.concat_map bases ~f:(fun base -> - match base with - | RecordAtom es -> ( - match - List.find es ~f:(fun (Ident key', _) -> - String.(key = key')) - with - | Some (_, r) -> r - | None -> - [] - (* Format.printf "base: %a\n" pp_atom base; - raise Runtime_error *)) - | _ -> raise Runtime_error) - (* fun x -> x | stub *) - | ExprStubAtom st when St.(label = Estate st) -> [] - | a -> - (* Format.printf "%a\n" pp_atom a; *) - [ a ]) - in - (* Format.printf "result: %a\n" pp_res r'; *) - r' - else r - -let cache = Hashtbl.create (module Cache_key) - -let rec analyze_aux_step ?(should_cache = true) d expr sigma pi s v v' = - if d > !max_d then max_d := d; - debug_plain "Began recursive call to execution"; - debug (fun m -> m "Max depth so far is: %d" !max_d); - debug (fun m -> m "expr: %a" Interpreter.Pp.pp_expr expr); - debug (fun m -> m "sigma: %s" (show_sigma sigma)); - let cache_key = (expr, sigma, v) in - (* let cache_key = (expr, sigma, v') in *) - match Hashtbl.find cache cache_key with - | Some r when should_cache -> - debug (fun m -> m "Cache hit: %a" pp_res r); - (r, s) - | _ -> - let r, s' = - match expr with - | Int i -> ([ IntAllAtom ], s) - | Bool b -> ([ BoolAtom b ], s) - | Function (_, _, l) -> ([ FunAtom (expr, l, sigma) ], s) - | Appl (e, _, l) -> - let d = d + 1 in - info (fun m -> - m "[Level %d] =========== Appl (%a) ============" d - Interpreter.Pp.pp_expr expr); - (* debug (fun m -> m "%a" Interpreter.Ast.pp_expr expr); *) - debug (fun m -> m "sigma: %s" (show_sigma sigma)); - let cycle_label = (l, sigma) in - let sigma' = l :: sigma in - let pruned_sigma' = prune_sigma sigma' in - debug (fun m -> m "sigma_pruned': %s" (show_sigma pruned_sigma')); - let st = (l, sigma, s) in - let st' = (l, sigma) in - (* let st = (l, pruned_sigma', s) in *) - let lst = NewSt.Lstate st in - let lst' = St.Lstate st' in - (* debug (fun m -> m "State: %s" (NewSt.show lst)); *) - (* debug_plain "v_set:"; - log_v_set v; *) - (* TODO: try two-pass mechanism again *) - if Set.mem v lst then ( - debug_plain "Stubbed"; - (* Format.printf "Stubbed\n"; *) - (* debug (fun m -> - m "sigma: %s | take: %s" (show_sigma sigma) - (show_sigma (sigma))); *) - info (fun m -> - m "[Level %d] *********** Appl (%a) ************" d - Interpreter.Pp.pp_expr expr); - ([ LabelStubAtom cycle_label ], s)) - else ( - (* Application *) - debug_plain "Didn't stub"; - debug (fun m -> - m "Evaluating function being applied: %a" - Interpreter.Pp.pp_expr e); - debug (fun m -> - m "Evaluating function being applied: %a" - Interpreter.Ast.pp_expr e); - let new_v = Set.add v lst in - let new_v' = Set.add v' lst' in - (* we don't remember whatever this subtree visited *) - let r1, s1 = - analyze_aux_step ~should_cache d e sigma pi s new_v new_v' - in - (* let r1 = simplify r1 in *) - debug (fun m -> m "r1 length: %d" (List.length r1)); - let new_s = Set.add s1 pruned_sigma' in - let r2, s2 = - fold_res_app ~init:(empty_choice_set, new_s) l sigma d r1 - ~f:(fun (acc_r, acc_s) e1 -> - debug (fun m -> - m "[Appl] Evaluating body of function being applied: %a" - Interpreter.Pp.pp_expr e1); - let ri, si = - analyze_aux_step ~should_cache d e1 pruned_sigma' pi new_s - new_v new_v' - in - (List.fold ri ~init:acc_r ~f:Set.add, Set.union acc_s si)) - in - let r2 = Set.elements r2 in - debug (fun m -> m "r2: %a" pp_res r2); - let r2 = elim_stub r2 (St.Lstate cycle_label) in - info (fun m -> - m "[Level %d] *********** Appl (%a) ************" d - Interpreter.Pp.pp_expr expr); - (r2, s2)) - | Var (Ident x, l) -> - let d = d + 1 in - info (fun m -> - m "[Level %d] =========== Var (%s, %d) ============" d x l); - let cycle_label = (expr, sigma) in - let st = (expr, sigma, s) in - let st' = (expr, sigma) in - let est = NewSt.Estate st in - let est' = St.Estate st' in - let new_v = Set.add v est in - let new_v' = Set.add v' est' in - (* debug (fun m -> m "State: %s" (Grammar.NewSt.show est)); *) - (* debug_plain "v_set:"; - log_v_set v; *) - if Set.mem v est then ( - (* Var Stub *) - debug (fun m -> m "Stubbed: %s" x); - (* Format.printf "Stubbed: %s\n" x; *) - info (fun m -> - m "[Level %d] *********** Var (%s, %d) ************" d x l); - ([ ExprStubAtom cycle_label ], s)) - else ( - debug_plain "Didn't stub"; - match get_myfun l with - | Some (Function (Ident x1, _, l_myfun)) -> - if String.(x = x1) then ( - (* Var Local *) - info (fun m -> - m - "[Level %d] =========== Var Local (%s, %d) \ - ============" - d x l); - debug (fun m -> m "sigma: %s" (show_sigma sigma)); - let s_hd, s_tl = (List.hd_exn sigma, List.tl_exn sigma) in - match get_myexpr s_hd with - | Appl (_, e2, l') -> - let r1, s1 = - debug_plain "Begin stitching stacks"; - (* debug_plain "S set:"; - debug (fun m -> m "%s" (show_set s)); - debug (fun m -> - m "Head of candidate fragments must be: %d" l'); - debug (fun m -> - m - "Tail of candidate fragments must start with: \ - %s" - (show_sigma s_tl)); *) - (* enumerate all matching stacks in the set *) - Set.fold s ~init:(empty_choice_set, s) - ~f:(fun (acc_r, acc_s) sigma_i -> - let sigma_i_hd, sigma_i_tl = - (List.hd_exn sigma_i, List.tl_exn sigma_i) - in - (* the fact that we can prune away "bad" stacks like this - makes DDE for program analysis superior *) - if sigma_i_hd = l' && starts_with sigma_i_tl s_tl - then ( - debug (fun m -> - m - "[Level %d] Stitched! Evaluating Appl \ - argument, using stitched stack %s:" - d (show_sigma sigma_i_tl)); - debug (fun m -> - m "%a" Interpreter.Pp.pp_expr e2); - (* debug (fun m -> - m "%a" Interpreter.Ast.pp_expr e2); *) - (* stitch the stack to gain more precision *) - let ri, si = - analyze_aux_step ~should_cache d e2 sigma_i_tl - pi s new_v new_v' - in - ( List.fold ri ~init:acc_r ~f:Set.add, - Set.union acc_s si )) - else (acc_r, acc_s)) - in - info (fun m -> - m - "[Level %d] *********** Var Local (%s, %d) \ - ************" - d x l); - info (fun m -> - m "[Level %d] *********** Var (%s, %d) ************" - d x l); - let r1 = Set.elements r1 in - debug (fun m -> m "r1: %a" pp_res r1); - let r1 = elim_stub r1 (St.Estate cycle_label) in - (r1, s1) - | _ -> raise Unreachable [@coverage off]) - else ( - (* Var Non-Local *) - info (fun m -> - m - "[Level %d] =========== Var Non-Local (%s, %d) \ - ============" - d x l); - debug (fun m -> m "sigma: %s" (show_sigma sigma)); - debug_plain "Reading Appl at front of sigma"; - match get_myexpr (List.hd_exn sigma) with - | Appl (e1, _, l2) -> - debug_plain "[Var Non-Local] Didn't stub e1"; - debug_plain "Function being applied at front of sigma:"; - debug (fun m -> m "%a" Interpreter.Pp.pp_expr e1); - debug (fun m -> m "%a" Interpreter.Ast.pp_expr e1); - let s_tl = List.tl_exn sigma in - debug_plain "Begin stitching stacks"; - (* debug_plain "S set:"; - debug (fun m -> m "%s" (show_set s)); - debug (fun m -> - m "Head of candidate fragments must be: %d" l2); - debug (fun m -> - m "Tail of candidate fragments must start with: %s" - (show_sigma s_tl)); *) - (* enumerate all matching stacks in the set *) - let r1, s1 = - Set.fold s ~init:(empty_choice_set, s) - ~f:(fun (acc_r, acc_s) si -> - let si_hd, si_tl = - (List.hd_exn si, List.tl_exn si) - in - if Stdlib.(si_hd = l2) && starts_with si_tl s_tl - then ( - debug (fun m -> - m - "[Level %d] Stitched! Evaluating \ - function being applied at front of \ - sigma, using stitched stack %s" - d (show_sigma si_tl)); - (* stitch the stack to gain more precision *) - (* let new_v = - Set.add v (NewSt.Estate (e1, si_tl, s)) - in *) - let r0, s0 = - analyze_aux_step ~should_cache d e1 si_tl pi s - v v' - in - ( List.fold r0 ~init:acc_r ~f:Set.add, - Set.union acc_s s0 )) - else (acc_r, acc_s)) - in - let r1 = Set.elements r1 in - (* let r1 = simplify r1 in *) - (* let new_st = (expr, sigma, s1) in - let new_v = Set.add v (NewSt.Estate new_st) in *) - debug_plain - "Found all stitched stacks and evaluated e1, begin \ - relabeling variables"; - let r2, s2 = - fold_res_var ~init:(empty_choice_set, s1) expr sigma d - r1 ~f:(fun (acc_r, acc_s) x1' l1 sigma1 -> - if Stdlib.(x1 = x1') && l_myfun = l1 then ( - debug (fun m -> - m - "[Var Non-Local] Relabel %s with label \ - %d and evaluate" - x l1); - let r0', s0' = - analyze_aux_step ~should_cache d - (Var (Ident x, l1)) - sigma1 pi s1 new_v new_v' - in - ( List.fold r0' ~init:acc_r ~f:Set.add, - Set.union acc_s s0' )) - else (acc_r, acc_s)) - in - info (fun m -> - m - "[Level %d] *********** Var Non-Local (%s, %d) \ - ************" - d x l); - info (fun m -> - m "[Level %d] *********** Var (%s, %d) ************" - d x l); - let r2 = Set.elements r2 in - debug (fun m -> m "r2: %a" pp_res r2); - let r2 = elim_stub r2 (St.Estate cycle_label) in - (r2, s2) - | _ -> raise Unreachable [@coverage off]) - | _ -> raise Unreachable [@coverage off]) - | If (e, e_true, e_false, l) -> ( - debug (fun m -> m "[Level %d] =========== If ===========" d); - let d = d + 1 in - let r_cond, s_cond = - analyze_aux_step ~should_cache d e sigma None s v v' - in - (* TODO: why do I need the following line? *) - (* let r_cond = simplify r_cond in *) - (* Format.printf "r_cond: %a\n" pp_res r_cond; *) - match r_cond with - (* TODO *) - | [ BoolAtom b ] -> - if b then - let r_true, s_true = - analyze_aux_step ~should_cache d e_true sigma None s v v' - in - (r_true, Set.union s_cond s_true) - else - let r_false, s_false = - analyze_aux_step ~should_cache d e_false sigma None s v v' - in - (r_false, Set.union s_cond s_false) - (* | [ InspectionAtom _ ] -> - Hashtbl.iteri cycles ~f:(fun ~key ~data -> - Format.printf "%a -> %a\n" St.pp key pp_res data); - failwith "what" *) - | _ -> - (* Format.printf "r_cond: %a\n" pp_res r_cond; *) - let r_true, s_true = - analyze_aux_step ~should_cache d e_true sigma None s v v' - in - info (fun m -> - m "Evaluating: %a" Interpreter.Pp.pp_expr e_false); - let r_false, s_false = - analyze_aux_step ~should_cache d e_false sigma None s v v' - in - (r_true @ r_false, Set.union s (Set.union s_true s_false))) - | Plus (e1, e2) - | Minus (e1, e2) - | Mult (e1, e2) - | Equal (e1, e2) - | And (e1, e2) - | Or (e1, e2) - | Ge (e1, e2) - | Gt (e1, e2) - | Le (e1, e2) - | Lt (e1, e2) -> - let d = d + 1 in - info (fun m -> - m "[Level %d] =========== Binop (%a) ============" d - Interpreter.Pp.pp_expr expr); - (* Format.printf "e1: %a | e2: %a\n" pp_expr e1 pp_expr e2; *) - let r1, s1 = analyze_aux_step ~should_cache d e1 sigma pi s v v' in - let r2, s2 = analyze_aux_step ~should_cache d e2 sigma pi s1 v v' in - debug (fun m -> - m "[Level %d] Evaluated binop to (%a %a)" d Utils.pp_res r1 - Utils.pp_res r2); - debug (fun m -> - m "[Level %d] Evaluated binop to (%a %a)" d Grammar.pp_res - r1 Grammar.pp_res r2); - info (fun m -> - m "[Level %d] *********** Binop (%a) ************" d - Interpreter.Pp.pp_expr expr); - ( (match expr with - | Plus _ -> ( - match (r1, r2) with - | [ IntAtom i1 ], [ IntAtom i2 ] -> [ IntAtom (i1 + i2) ] - | _ -> - (* Format.printf "Plus: r1: %a | r2: %a\n" pp_res r1 pp_res - r2; *) - [ IntAllAtom ]) - | Minus _ -> [ IntAllAtom ] - | Mult _ -> ( - match (r1, r2) with - | [ IntAtom i1 ], [ IntAtom i2 ] -> [ IntAtom (i1 * i2) ] - | r1', r2' -> [ IntAllAtom ]) - | And _ -> ( - match (r1, r2) with - | [ BoolAtom b1 ], [ BoolAtom b2 ] -> [ BoolAtom (b1 && b2) ] - | [ BoolAtom b11; BoolAtom b12 ], [ BoolAtom b2 ] -> - let b1 = b11 && b2 in - let b2 = b12 && b2 in - [ BoolAtom (b1 || b2) ] - | [ BoolAtom b1 ], [ BoolAtom b21; BoolAtom b22 ] -> - let b1 = b1 && b21 in - let b2 = b1 && b22 in - [ BoolAtom (b1 || b2) ] - | ( [ BoolAtom b11; BoolAtom b12 ], - [ BoolAtom b21; BoolAtom b22 ] ) -> - let b1 = (b11 && b21) || (b11 && b22) in - let b2 = (b12 && b21) || (b12 && b22) in - [ BoolAtom (b1 || b2) ] - | _ -> - (* Format.printf "r1: %a | r2: %a\n" pp_res r1 pp_res r2; *) - [ BoolAtom true; BoolAtom false ]) - | Or _ -> ( - match (r1, r2) with - | [ BoolAtom b1 ], [ BoolAtom b2 ] -> [ BoolAtom (b1 || b2) ] - | [ BoolAtom b11; BoolAtom b12 ], [ BoolAtom b2 ] -> - let b1 = b11 || b2 in - let b2 = b12 || b2 in - [ BoolAtom (b1 || b2) ] - | [ BoolAtom b1 ], [ BoolAtom b21; BoolAtom b22 ] -> - let b1 = b1 || b21 in - let b2 = b1 || b22 in - [ BoolAtom (b1 || b2) ] - | ( [ BoolAtom b11; BoolAtom b12 ], - [ BoolAtom b21; BoolAtom b22 ] ) -> - let b1 = (b11 || b21) || b11 || b22 in - let b2 = (b12 || b21) || b12 || b22 in - [ BoolAtom (b1 || b2) ] - | _ -> - (* Format.printf "r1: %a | r2: %a\n" pp_res r1 pp_res r2; *) - [ BoolAtom true; BoolAtom false ]) - | Equal _ | Ge _ | Gt _ | Le _ | Lt _ -> - [ BoolAtom true; BoolAtom false ] - | _ -> - Format.printf "%a\n" pp_expr expr; - raise Unreachable [@coverage off]), - Set.union s (Set.union s1 s2) ) - | Not e -> ( - let d = d + 1 in - let r, s = analyze_aux_step ~should_cache d e sigma pi s v v' in - match r with - | [ BoolAtom b ] -> - (* Format.printf "%a\n" pp_res r; *) - ([ BoolAtom (not b) ], s) - | [] -> ([], s) - | _ -> ([ BoolAtom false; BoolAtom true ], s)) - | Record entries -> - let d = d + 1 in - ( [ - RecordAtom - (entries - |> List.map ~f:(fun (x, ei) -> - ( x, - let r, _ = - analyze_aux_step ~should_cache d ei sigma pi s v v' - in - r ))); - ], - s ) - | Projection (e, Ident key) -> - debug (fun m -> m "[Level %d] =========== Projection ===========" d); - let d = d + 1 in - let r0, s0 = analyze_aux_step ~should_cache d e sigma pi s v v' in - ([ ProjectionAtom (r0, Ident key) ], s0) - | Inspection (Ident key, e) -> - let d = d + 1 in - let r0, s0 = analyze_aux_step ~should_cache d e sigma pi s v v' in - ([ InspectionAtom (Ident key, r0) ], s0) - | LetAssert (id, e1, e2) -> - let d = d + 1 in - let r1, s1 = analyze_aux_step ~should_cache d e1 sigma pi s v v' in - let r2 = eval_assert e2 id in - ([ AssertAtom (id, r1, r2) ], s1) - | Let _ -> raise Unreachable [@coverage off] - in - Hashtbl.remove cache cache_key; - Hashtbl.add_exn cache ~key:cache_key ~data:r; - debug (fun m -> - m "Insert into cache: (%a, %s) -> %a" Interpreter.Pp.pp_expr expr - (show_sigma sigma) pp_res r); - (simplify r, s') -(* (r, s') *) -(* TODO: run with poor man's cache first then use S to rerun *) - -and analyze_aux ?(should_cache = true) n e_glob d expr sigma pi s v v' = - debug (fun m -> m "[Level %d] [n = %d] Entered analyze_aux" d n); - let r, s' = analyze_aux_step ~should_cache d expr sigma pi s v v' in - debug (fun m -> m "[Level %d] After analyze_aux_step" d); - if Set.compare_direct s s' = 0 then ( - debug_plain "S didn't change, finishing..."; - (r, s')) - else ( - debug (fun m -> m "r: %a" pp_res r); - debug (fun m -> m "[Level %d] [n = %d] Restarting afresh" d n); - (* debug (fun m -> - m "[Level %d] S before evaluating e_glob:\n%s" d (show_set s')); *) - (* Hashtbl.clear cache; *) - let r, s' = - analyze_aux (n + 1) e_glob 0 e_glob [] None s' - (Set.empty (module NewSt)) - (Set.empty (module St)) - in - (* debug (fun m -> - m "[Level %d] S after evaluating e_glob:\n%s" d (show_set s')); *) - (* (simplify r, s') *) - (r, s')) - -let analyze ?(debug_mode = false) ?(verify = true) ?(test_num = 0) - ?(should_cache = true) e = - is_debug_mode := debug_mode; - - let e = transform_let e in - build_myfun e None; - debug (fun m -> m "%a" Interpreter.Pp.pp_expr e); - debug (fun m -> m "%a" pp_expr e); - - (* Format.printf "%a\n" pp_expr e; *) - (* let r, s = - analyze_aux 0 e 0 e [] None - (Set.empty (module SKey)) - (Set.empty (module NewSt)) - (Set.empty (module St)) - in *) - let r, s = - analyze_aux_step 0 e [] None - (Set.empty (module SKey)) - (Set.empty (module NewSt)) - (Set.empty (module St)) - ~should_cache:false - in - (* let r = simplify r in *) - (* dot_of_result test_num r; *) - debug (fun m -> m "Result: %a" Utils.pp_res r); - debug (fun m -> m "Result: %a" Grammar.pp_res r); - (if !is_debug_mode then ( - Format.printf "\n%s\n\n" @@ show_expr e; - Format.printf "****** Label Table ******\n"; - Interpreter.Interp.print_myexpr myexpr; - Format.printf "****** Label Table ******\n\n")) - [@coverage off]; - - clean_up (); - - (* if verify then verify_result r; *) - r - -(* DDE kinda similar to mCFA *) -(* performance bottleneck with checking if two sets are same if we were to cache with S set. Zach's library to give unique id for a set *) -(* fancy caching scheme to tell how to catch up (timestamped cache entries) *) - -(* make rules more clear *) -(* what's the relationship between judgements holding: e and e1, x twice deep in e1 in Var Non-Local *) diff --git a/program_analysis/reworked/simplifier.ml b/program_analysis/reworked/simplifier.ml deleted file mode 100644 index de9a523..0000000 --- a/program_analysis/reworked/simplifier.ml +++ /dev/null @@ -1,40 +0,0 @@ -open Core -open Grammar -open Interpreter.Ast - -exception Unreachable -exception Runtime_error - -let rec simplify r = - let r' = - List.concat_map r ~f:(fun a -> - match a with - | IntAtom _ | BoolAtom _ | LabelStubAtom _ | ExprStubAtom _ | FunAtom _ - | IntAllAtom -> - [ a ] - | AssertAtom (id, r, rv) -> [ AssertAtom (id, simplify r, rv) ] - | RecordAtom entries -> - [ - RecordAtom (List.map entries ~f:(fun (id, r) -> (id, simplify r))); - ] - | ProjectionAtom (r, (Ident key as x)) -> - List.concat_map r ~f:(function - | RecordAtom es -> ( - match - List.find es ~f:(fun (Ident key', _) -> String.(key = key')) - with - | Some (_, r) -> r - | None -> - [] - (* Format.printf "%a\n" pp_atom a; - raise Runtime_error *)) - | a -> [ ProjectionAtom (simplify [ a ], x) ]) - | InspectionAtom ((Ident key as x), r) -> - List.map r ~f:(function - | RecordAtom es -> - BoolAtom - (List.exists es ~f:(fun (Ident key', _) -> - String.(key = key'))) - | a -> InspectionAtom (x, simplify [ a ]))) - in - if compare_res r r' = 0 then r' else simplify r' diff --git a/program_analysis/reworked/utils.ml b/program_analysis/reworked/utils.ml deleted file mode 100644 index 50fa1cd..0000000 --- a/program_analysis/reworked/utils.ml +++ /dev/null @@ -1,531 +0,0 @@ -open Core -open Interpreter.Ast -open Grammar - -let pf = Format.printf -let pfl = pf "%s\n" -let prune_sigma ?(k = 2) s = List.filteri s ~f:(fun i _ -> i < k) -let take_sigma ?(k = 2) = Fn.flip List.take (k - 1) - -let rec starts_with sigma_parent sigma_child = - match (sigma_parent, sigma_child) with - | _, [] -> true - | [], _ -> false - | l_parent :: ls_parent, l_child :: ls_child -> - l_parent = l_child && starts_with ls_parent ls_child - -let show_set = Set.fold ~init:"" ~f:(fun acc s -> show_sigma s ^ "\n" ^ acc) -let pp_pair fmt (l, s) = Format.fprintf fmt "(%d, %s)" l @@ show_sigma s -let pp_pair_list fmt ls = Format.pp_print_list pp_pair fmt ls -let is_debug_mode = ref false - -let all_combs l1 l2 = - Set.fold l1 ~init:[] ~f:(fun acc x -> - Set.fold l2 ~init:[] ~f:(fun acc y -> (x, y) :: acc)) - -let ff = Format.fprintf - -let rec pp_atom fmt = function - | IntAllAtom -> ff fmt "Int" - | IntAtom i -> ff fmt "%d" i - | BoolAtom b -> ff fmt "%b" b - | FunAtom (f, _, _) -> Interpreter.Pp.pp_expr fmt f - (* | LabelResAtom (choices, _) -> ff fmt "%a" pp_res choices - | ExprResAtom (choices, _) -> ff fmt "%a" pp_res choices - | LabelStubAtom _ -> ff fmt "stub" - | ExprStubAtom _ -> ff fmt "stub" *) - (* | LabelResAtom (choices, (l, _)) -> ff fmt "(%a)^%d" pp_res choices l - | ExprResAtom (choices, (e, _)) -> - ff fmt "(%a)^%a" pp_res choices Interpreter.Pp.pp_expr e - | LabelStubAtom (l, _) -> ff fmt "stub@%d" l - | ExprStubAtom (e, _) -> ff fmt "(stub@%a)" Interpreter.Pp.pp_expr e *) - (* | OpAtom op -> ( - match op with - | PlusOp (r1, r2) -> ff fmt "(%a + %a)" pp_res r1 pp_res r2 - | MinusOp (r1, r2) -> ff fmt "(%a - %a)" pp_res r1 pp_res r2 - | MultOp (r1, r2) -> ff fmt "(%a * %a)" pp_res r1 pp_res r2 - | EqualOp (r1, r2) -> ff fmt "(%a = %a)" pp_res r1 pp_res r2 - | AndOp (r1, r2) -> ff fmt "(%a and %a)" pp_res r1 pp_res r2 - | OrOp (r1, r2) -> ff fmt "(%a or %a)" pp_res r1 pp_res r2 - | GeOp (r1, r2) -> ff fmt "(%a >= %a)" pp_res r1 pp_res r2 - | GtOp (r1, r2) -> ff fmt "(%a > %a)" pp_res r1 pp_res r2 - | LeOp (r1, r2) -> ff fmt "(%a <= %a)" pp_res r1 pp_res r2 - | LtOp (r1, r2) -> ff fmt "(%a < %a)" pp_res r1 pp_res r2 - | NotOp r1 -> ff fmt "(not %a)" pp_res r1) *) - (* | EquivStubAtom (s, l) -> - ff fmt "{%s}[%d]" - (s |> Set.to_list - |> List.map ~f:(fun st -> Format.sprintf "%s" (St.show st)) - |> String.concat ~sep:", ") - l *) - (* | PathCondAtom (_, r) -> ff fmt "%a" pp_res r *) - (* | PathCondAtom ((r, b), r') -> ff fmt "(%a = %b ⊩ %a)" pp_res r b pp_res r' *) - | LabelStubAtom _ -> ff fmt "stub" - | ExprStubAtom _ -> ff fmt "stub" - | RecordAtom entries -> - ff fmt - (if List.length entries = 0 then "{%a}" else "{ %a }") - pp_record_atom entries - | ProjectionAtom (r, Ident s) -> ff fmt "(%a.%s)" pp_res r s - | InspectionAtom (Ident s, r) -> ff fmt "(%s in %a)" s pp_res r - | AssertAtom (_, r, _) -> ff fmt "%a" pp_res r - -and pp_record_atom fmt = function - | [] -> () - | [ (Ident x, v) ] -> Format.fprintf fmt "%s = %a" x pp_res v - | (Ident x, v) :: rest -> - Format.fprintf fmt "%s = %a; %a" x pp_res v pp_record_atom rest - -and pp_res fmt = function - | [] -> () - | [ a ] -> ff fmt "%a" pp_atom a - | a :: _as -> ff fmt "(%a | %a)" pp_atom a pp_res _as - -type lop = - | LPlusOp of lres * lres - | LMinusOp of lres * lres - | LMultOp of lres * lres - | LEqualOp of lres * lres - | LAndOp of lres * lres - | LOrOp of lres * lres - | LGeOp of lres * lres - | LGtOp of lres * lres - | LLeOp of lres * lres - | LLtOp of lres * lres - | LNotOp of lres - -and latom = - | LIntAtom of int * int - | LBoolAtom of bool * int - | LFunAtom of expr * int * sigma - | LOpAtom of lop * int - | LLabelResAtom of lres * St.lstate * int - | LExprResAtom of lres * St.estate * int - | LLabelStubAtom of St.lstate * int - | LExprStubAtom of St.estate * int - | LPathCondAtom of lpath_cond * lres - | LRecordAtom of (ident * lres) list - | LProjectionAtom of lres * ident - | LInspectionAtom of ident * lres - | LAssertAtom of ident * lres * Interpreter.Ast.res_val_fv - -and lres = latom list - -and lpath_cond = lres * bool -[@@deriving hash, sexp, compare, show { with_path = false }] - -module LAtomKey = struct - module T = struct - type t = latom [@@deriving hash, sexp, compare] - end - - include T - include Comparable.Make (T) -end - -module LResKey = struct - module T = struct - type t = lres [@@deriving hash, sexp, compare] - end - - include T - include Comparable.Make (T) -end - -let rec ppp_latom fmt = function - | LIntAtom (x, _) -> ff fmt "%d" x - | LBoolAtom (b, _) -> ff fmt "%b" b - | LFunAtom (f, _, _) -> Interpreter.Pp.pp_expr fmt f - | LLabelResAtom (choices, _, _) | LExprResAtom (choices, _, _) -> - ff fmt "%a" ppp_lres choices - (* ff fmt "(%a, %a, %a)" pp_res choices Interpreter.Pp.pp_expr e pp_sigma s *) - | LOpAtom (op, _) -> ( - match op with - | LPlusOp (r1, r2) -> ff fmt "(%a + %a)" ppp_lres r1 ppp_lres r2 - | LMinusOp (r1, r2) -> ff fmt "(%a - %a)" ppp_lres r1 ppp_lres r2 - | LMultOp (r1, r2) -> ff fmt "(%a * %a)" ppp_lres r1 ppp_lres r2 - | LEqualOp (r1, r2) -> ff fmt "(%a = %a)" ppp_lres r1 ppp_lres r2 - | LAndOp (r1, r2) -> ff fmt "(%a and %a)" ppp_lres r1 ppp_lres r2 - | LOrOp (r1, r2) -> ff fmt "(%a or %a)" ppp_lres r1 ppp_lres r2 - | LGeOp (r1, r2) -> ff fmt "(%a >= %a)" ppp_lres r1 ppp_lres r2 - | LGtOp (r1, r2) -> ff fmt "(%a > %a)" ppp_lres r1 ppp_lres r2 - | LLeOp (r1, r2) -> ff fmt "(%a <= %a)" ppp_lres r1 ppp_lres r2 - | LLtOp (r1, r2) -> ff fmt "(%a < %a)" ppp_lres r1 ppp_lres r2 - | LNotOp r -> ( - match r with - | [ LOpAtom (lop, l) ] -> ( - match lop with - | LEqualOp (r1, r2) -> ff fmt "%a <> %a" ppp_lres r1 ppp_lres r2 - | LGeOp (r1, r2) -> - ff fmt "%a" ppp_latom (LOpAtom (LLtOp (r1, r2), l)) - | LGtOp (r1, r2) -> - ff fmt "%a" ppp_latom (LOpAtom (LLeOp (r1, r2), l)) - | LLeOp (r1, r2) -> - ff fmt "%a" ppp_latom (LOpAtom (LGtOp (r1, r2), l)) - | LLtOp (r1, r2) -> - ff fmt "%a" ppp_latom (LOpAtom (LGeOp (r1, r2), l)) - | _ -> failwith "unimplemented:160") - | _ -> failwith "unimplemented:161")) - | LLabelStubAtom _ | LExprStubAtom _ -> ff fmt "stub" - (* | PathCondAtom ((r, b), r') -> ff fmt "(%a = %b ⊩ %a)" pp_res r b pp_res r' *) - | LPathCondAtom (_, r) -> ff fmt "%a" ppp_lres r - | LRecordAtom entries -> - ff fmt - (if List.length entries = 0 then "{%a}" else "{ %a }") - pp_lrecord_atom entries - | LProjectionAtom (r, Ident s) -> ff fmt "%a.%s" ppp_lres r s - | LInspectionAtom (Ident s, r) -> ff fmt "%s in %a" s ppp_lres r - | LAssertAtom (_, r, _) -> ff fmt "%a" ppp_lres r - -and pp_lrecord_atom fmt = function - | [] -> () - | [ (Ident x, v) ] -> Format.fprintf fmt "%s = %a" x ppp_lres v - | (Ident x, v) :: rest -> - Format.fprintf fmt "%s = %a; %a" x ppp_lres v pp_lrecord_atom rest - -and ppp_lres fmt = function - | [] -> () - | [ a ] -> ff fmt "%a" ppp_latom a - | a :: _as -> ff fmt "(%a | %a)" ppp_latom a ppp_lres _as - -let res_to_id = Hashtbl.create (module LResKey) -let atom_to_id = Hashtbl.create (module LAtomKey) -let nodes = Hashset.create 100 -let edges = Hashtbl.create (module String) -let edge_props = Hashtbl.create (module String) -let siblings = Hashtbl.create (module String) -let fresh_id = ref (-1) - -let get_next_id () = - incr fresh_id; - !fresh_id - -let idr r = - Format.sprintf "P%d" (Hashtbl.find_or_add res_to_id r ~default:get_next_id) - -let ida a = - Format.sprintf "P%d" (Hashtbl.find_or_add atom_to_id a ~default:get_next_id) - -let add_node = Hashset.add nodes -let remove_node = Hashset.remove nodes - -let add_edge hd tl = - match Hashtbl.find edges hd with - | None -> Hashtbl.add_exn edges ~key:hd ~data:(String.Set.singleton tl) - | Some tls -> - Hashtbl.remove edges hd; - Hashtbl.add_exn edges ~key:hd ~data:(Set.add tls tl) - -let remove_edge hd tl = - match Hashtbl.find edges hd with - | None -> () - | Some tls -> - Hashtbl.remove edges hd; - Hashtbl.add_exn edges ~key:hd ~data:(Set.remove tls tl) - -let add_sibling p n = - match Hashtbl.find siblings p with - | None -> Hashtbl.add_exn siblings ~key:p ~data:(String.Set.singleton n) - | Some ns -> - Hashtbl.remove siblings p; - Hashtbl.add_exn siblings ~key:p ~data:(Set.add ns n) - -let remove_sibling p n = - match Hashtbl.find siblings p with - | None -> () - | Some ns -> - Hashtbl.remove siblings p; - Hashtbl.add_exn siblings ~key:p ~data:(Set.remove ns n) - -let add_edge_prop e (k, v) = - let p = Format.sprintf "%s=%s" k v in - match Hashtbl.find edge_props e with - | None -> Hashtbl.add_exn edge_props ~key:e ~data:(String.Set.singleton p) - | Some ps -> - Hashtbl.remove edge_props e; - Hashtbl.add_exn edge_props ~key:e ~data:(Set.add ps p) - -let op_symbol = function - | LPlusOp _ -> "+" - | LMinusOp _ -> "-" - | LMultOp _ -> "*" - | LEqualOp _ -> "=" - | LAndOp _ -> "&&" - | LOrOp _ -> "||" - | LNotOp _ -> "!" - | LGeOp _ -> ">=" - | LGtOp _ -> ">" - | LLeOp _ -> "<=" - | LLtOp _ -> "<" - -let next_label = ref 100000 - -let get_next_label () = - incr next_label; - !next_label - -let rec label_prim = - List.map ~f:(function - | IntAllAtom -> LIntAtom (-1, get_next_label ()) - | IntAtom i -> LIntAtom (i, get_next_label ()) - | BoolAtom b -> LBoolAtom (b, get_next_label ()) - | FunAtom (e, l, s) -> LFunAtom (e, l, s) - (* | OpAtom op -> - LOpAtom - ( (match op with - | PlusOp (r1, r2) -> LPlusOp (label_prim r1, label_prim r2) - | MinusOp (r1, r2) -> LMinusOp (label_prim r1, label_prim r2) - | MultOp (r1, r2) -> LMultOp (label_prim r1, label_prim r2) - | EqualOp (r1, r2) -> LEqualOp (label_prim r1, label_prim r2) - | GeOp (r1, r2) -> LGeOp (label_prim r1, label_prim r2) - | GtOp (r1, r2) -> LGtOp (label_prim r1, label_prim r2) - | LeOp (r1, r2) -> LLeOp (label_prim r1, label_prim r2) - | LtOp (r1, r2) -> LLtOp (label_prim r1, label_prim r2) - | AndOp (r1, r2) -> LAndOp (label_prim r1, label_prim r2) - | OrOp (r1, r2) -> LOrOp (label_prim r1, label_prim r2) - | NotOp r -> LNotOp (label_prim r)), - get_next_label () ) *) - | AssertAtom (id, r, assn) -> LAssertAtom (id, label_prim r, assn) - (* | LabelResAtom (r, st) -> LLabelResAtom (label_prim r, st, get_next_label ()) - | ExprResAtom (r, st) -> LExprResAtom (label_prim r, st, get_next_label ()) - | PathCondAtom ((r_cond, b), r) -> - LPathCondAtom ((label_prim r_cond, b), label_prim r) - | LabelStubAtom st -> LLabelStubAtom (st, get_next_label ()) - | ExprStubAtom st -> LExprStubAtom (st, get_next_label ()) *) - | RecordAtom entries -> - LRecordAtom (List.map entries ~f:(fun (id, r) -> (id, label_prim r))) - | ProjectionAtom (r, id) -> LProjectionAtom (label_prim r, id) - | _ as a -> - Format.printf "%a" Grammar.pp_atom a; - failwith "unimplemented:290") - -let dot_of_result ?(display_path_cond = true) test_num r = - let r = label_prim r in - (* Logs.info (fun m -> m "AST: %a" pp_lres r); *) - (* p is the parent *atom* of a *) - (* l is the label of the enclosing labeled result, if any *) - (* any cycle (particularly its start) should be unique in - each path condition subtree *) - let rec dot_of_atom a p cycles = - let aid = ida a in - match a with - | LIntAtom (i, l) -> add_node (Format.sprintf "%s [label=\"%i\"];" aid i) - | LBoolAtom (b, l) -> add_node (Format.sprintf "%s [label=\"%b\"];" aid b) - | LOpAtom (op, _) -> ( - match op with - | LPlusOp (r1, r2) - | LMinusOp (r1, r2) - | LEqualOp (r1, r2) - | LMultOp (r1, r2) - | LGeOp (r1, r2) - | LGtOp (r1, r2) - | LLeOp (r1, r2) - | LLtOp (r1, r2) - | LAndOp (r1, r2) - | LOrOp (r1, r2) -> - add_node (Format.sprintf "%s [label=\"%s\"];" aid (op_symbol op)); - add_edge aid (idr r1); - add_edge aid (idr r2); - dot_of_res r1 (Some a) cycles; - dot_of_res r2 (Some a) cycles - | LNotOp r -> - add_node (Format.sprintf "%s [label=\"%s\"];" aid (op_symbol op)); - add_edge aid (idr r); - dot_of_res r (Some a) cycles) - | LLabelResAtom (r, st, l) -> - (* always point to the lowest instance of such a disjunction *) - add_node (Format.sprintf "%s [label=\"|\", shape=\"diamond\"];" aid); - add_edge aid (idr r); - let lst = St.Lstate st in - dot_of_res r (Some a) - (Map.add_exn (Map.remove cycles lst) ~key:lst ~data:aid) - | LExprResAtom (r, st, l) -> - add_node (Format.sprintf "%s [label=\"|\", shape=\"diamond\"];" aid); - add_edge aid (idr r); - let est = St.Estate st in - dot_of_res r (Some a) - (Map.add_exn (Map.remove cycles est) ~key:est ~data:aid) - | LLabelStubAtom (st, _) -> ( - add_node (Format.sprintf "%s [label=\"stub\", shape=\"box\"];" aid); - match Map.find cycles (St.Lstate st) with - | Some dom_node -> - let aid = Format.sprintf "%s:n" aid in - let edge_id = Format.sprintf "%s_%s" dom_node aid in - add_edge dom_node aid; - add_edge_prop edge_id ("dir", "back") - | None -> Logs.debug (fun m -> m "Lone stub: %s" (St.show_lstate st)) - (* Format.printf "Lone stub: %s\n" (St.show_lstate st) *) - (* failwith "Lone stub!" *)) - | LExprStubAtom (st, l) -> ( - add_node (Format.sprintf "%s [label=\"stub\", shape=\"box\"];" aid); - match Map.find cycles (St.Estate st) with - | Some dom_node -> - let aid = Format.sprintf "%s:sw" aid in - let edge_id = Format.sprintf "%s_%s" dom_node aid in - add_edge dom_node aid; - add_edge_prop edge_id ("dir", "back") - | None -> Logs.debug (fun m -> m "Lone stub: %s" (St.show_estate st)) - (* Format.printf "Lone stub: %s\n" (St.show_estate st) *) - (* failwith "Lone stub!" *)) - | LAssertAtom (_, r, _) -> - add_node (Format.sprintf "%s [label=\"Assert\"];" aid); - let rid = idr r in - add_edge aid rid; - dot_of_res r (Some a) cycles - | LPathCondAtom ((r, b), r0) -> - add_node (Format.sprintf "%s [label=\"⊩\"];" aid); - (if b then ( - add_edge aid (idr r); - dot_of_res r (Some a) cycles) - else - match r with - | [ LOpAtom (lop, _) ] -> ( - match lop with - | LEqualOp (r1, r2) -> - let a' = LOpAtom (LNotOp r, get_next_label ()) in - add_edge aid (ida a'); - dot_of_atom a' (Some a) cycles - | LGeOp (r1, r2) -> - let a' = LOpAtom (LLtOp (r1, r2), get_next_label ()) in - add_edge aid (ida a'); - dot_of_atom a' (Some a) cycles - | LGtOp (r1, r2) -> - let a' = LOpAtom (LLeOp (r1, r2), get_next_label ()) in - add_edge aid (ida a'); - dot_of_atom a' (Some a) cycles - | LLeOp (r1, r2) -> - let a' = LOpAtom (LGtOp (r1, r2), get_next_label ()) in - add_edge aid (ida a'); - dot_of_atom a' (Some a) cycles - | LLtOp (r1, r2) -> - let a' = LOpAtom (LGeOp (r1, r2), get_next_label ()) in - add_edge aid (ida a'); - dot_of_atom a' (Some a) cycles - | _ -> failwith "unimplemented:395") - | [ LBoolAtom (b, _) ] -> - let a' = LBoolAtom (not b, get_next_label ()) in - add_edge aid (ida a'); - dot_of_atom a' (Some a) cycles - | _ -> - Format.printf "%a\n" pp_lres r; - raise Unreachable); - add_edge aid (idr r0); - dot_of_res r0 (Some a) cycles; - ( (* match p with - | None -> - (* incr fresh_id; - let parent_aid = Format.sprintf "P%d" !fresh_id in *) - failwith "TODO" - | Some parent_a -> - let parent_aid = ida parent_a in - remove_edge parent_aid aid; - remove_sibling parent_aid aid; - let r0id = idr r0 in - add_edge parent_aid r0id; - ignore - (Hashtbl.add edge_labels - ~key:(Format.sprintf "%s_%s" parent_aid r0id) - ~data: - (match r with - | [ LOpAtom (op, _) ] -> - if b then Format.asprintf "%a" pp_lres r - else - Format.asprintf "%a" ppp_latom - (LOpAtom (LNotOp r, get_next_label ())) - | _ -> raise Unreachable)); - dot_of_res r0 (Some parent_a) *) ) - | LRecordAtom entries -> - add_node - (Format.sprintf "%s [shape=record, label=\"%s\"]" aid - (String.concat ~sep:"|" - (List.map entries ~f:(fun (Ident id, r) -> - let entry_id = Format.sprintf "%s_%s" aid id in - add_edge (Format.sprintf "%s:%s" aid entry_id) (idr r); - dot_of_res r (Some a) cycles; - Format.sprintf "<%s> %s" entry_id id)))) - | _ -> - Format.printf "%a\n" ppp_latom a; - raise Unreachable - and dot_of_res r p pl = - let rid = idr r in - match p with - | None -> - if List.length r = 1 then dot_of_atom (List.hd_exn r) None pl - else - List.iter r ~f:(fun a -> - dot_of_atom a None pl; - add_node (Format.sprintf "%s [label=\"|\"];" rid); - add_edge rid (ida a)) - | Some p -> ( - let pid = ida p in - add_sibling pid rid; - match p with - | LLabelResAtom _ | LExprResAtom _ -> - remove_edge pid rid; - remove_sibling pid rid; - List.iter r ~f:(fun a -> - let aid = ida a in - add_edge pid aid; - add_sibling pid aid; - dot_of_atom a (Some p) pl) - | _ -> - if List.length r = 1 then ( - let a = List.hd_exn r in - let aid = ida a in - remove_edge pid rid; - remove_sibling pid rid; - add_edge pid aid; - add_sibling pid aid; - (* needs to be called last to remove edges to PathCondAtoms *) - dot_of_atom a (Some p) pl) - else - List.iter r ~f:(fun a -> - dot_of_atom a (Some p) pl; - add_node (Format.sprintf "%s [label=\"|\"];" rid); - add_edge rid (ida a))) - in - dot_of_res r None (Map.empty (module St)); - let nodes_str = Hashset.fold (Format.sprintf "%s\n%s") nodes "" in - let ranks_str = - Hashtbl.fold siblings ~init:"" ~f:(fun ~key ~data acc -> - (* https://stackoverflow.com/questions/44274518/how-can-i-control-within-level-node-order-in-graphvizs-dot/44274606#44274606 *) - let rank2 = Format.sprintf "%s_rank2" key in - if Set.length data = 1 then acc - else - Format.sprintf - "%s\n\ - %s [style=invis];\n\ - {rank=same; rankdir=LR; %s -> %s [style=invis];}" acc rank2 rank2 - (String.concat ~sep:" -> " (Set.to_list data))) - in - let edges_str = - Hashtbl.fold edges ~init:"" ~f:(fun ~key ~data acc -> - Set.fold data ~init:acc ~f:(fun acc n -> - let id = Format.sprintf "%s_%s" key n in - let props = - match Hashtbl.find edge_props id with - | None -> "" - | Some ps -> - Format.sprintf "[%s]" - (String.concat ~sep:"," (Set.to_list ps)) - in - Format.sprintf "%s\n%s -> %s %s" acc key n props)) - in - let dot_file = Format.sprintf "graph%d.dot" test_num in - Out_channel.write_all dot_file - ~data: - (Format.sprintf - "digraph G {\n\ - node [fontname=\"Monospace\"]\n\ - edge [fontname=\"Monospace\"]\n\ - %s%s\n\ - %s\n\ - }" - nodes_str ranks_str edges_str); - Hashtbl.clear res_to_id; - Hashtbl.clear atom_to_id; - Hashset.clear nodes; - Hashtbl.clear edges; - Hashtbl.clear edge_props; - Hashtbl.clear siblings; - fresh_id := -1 diff --git a/program_analysis/reworked/debugutils.ml b/program_analysis/simple/debugutils.ml similarity index 78% rename from program_analysis/reworked/debugutils.ml rename to program_analysis/simple/debugutils.ml index 793b5d7..0c57011 100644 --- a/program_analysis/reworked/debugutils.ml +++ b/program_analysis/simple/debugutils.ml @@ -4,12 +4,11 @@ open Utils let is_debug_mode = ref false let parse s = - s ^ ";;" |> Lexing.from_string - |> Interpreter.Parser.main Interpreter.Lexer.token + s ^ ";;" |> Lexing.from_string |> Interp.Parser.main Interp.Lexer.token |> fun e -> (* keep labeling consistent across multiple calls to `analyze` *) - Interpreter.Ast.reset_label (); + Interp.Ast.reset_label (); e let unparse = Format.asprintf "%a" pp_res diff --git a/program_analysis/reworked/dune b/program_analysis/simple/dune similarity index 63% rename from program_analysis/reworked/dune rename to program_analysis/simple/dune index 5d5861a..7a7fcf9 100644 --- a/program_analysis/reworked/dune +++ b/program_analysis/simple/dune @@ -1,9 +1,9 @@ (library - (name pa_reworked) - (public_name dde.pa_reworked) + (name simple_pa) + (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 dde.interpreter hashset core z3 logs logs.fmt) + (libraries hashset core z3 logs logs.fmt dde.interp dde.pa) (instrumentation (backend landmarks --auto))) diff --git a/program_analysis/reworked/grammar.ml b/program_analysis/simple/grammar.ml similarity index 86% rename from program_analysis/reworked/grammar.ml rename to program_analysis/simple/grammar.ml index aa6d81a..ad41c60 100644 --- a/program_analysis/reworked/grammar.ml +++ b/program_analysis/simple/grammar.ml @@ -1,5 +1,5 @@ open Core -open Interpreter.Ast +open Interp.Ast module SKey = struct module T = struct @@ -51,8 +51,8 @@ module NewSt = struct [@@deriving compare, sexp, hash] let show_estate (e, sigma, s) = - Format.asprintf "(%a, %s, {%s})" Interpreter.Ast.pp_expr e - (show_sigma sigma) (show_set s) + Format.asprintf "(%a, %s, {%s})" Interp.Ast.pp_expr e (show_sigma sigma) + (show_set s) let pp_estate fmt est = Format.fprintf fmt "%s" (show_estate est) @@ -82,18 +82,18 @@ module Cache_key = struct end open Core -open Interpreter.Ast +open Interp.Ast type atom = - | IntAllAtom + | IntAnyAtom | IntAtom of int | BoolAtom of bool | FunAtom of expr * int * sigma - | LabelStubAtom of (int * sigma) - | ExprStubAtom of (expr * sigma) - | RecordAtom of (ident * res) list - | ProjectionAtom of res * ident - | InspectionAtom of ident * res + | LStubAtom of (int * sigma) + | EStubAtom of (expr * sigma) + | RecAtom of (ident * res) list + | ProjAtom of res * ident + | InspAtom of ident * res | AssertAtom of ident * res * res_val_fv and res = atom list [@@deriving hash, sexp, compare, show { with_path = false }] @@ -123,15 +123,6 @@ module Choice = struct include Comparable.Make (T) end -(* module PathChoice = struct - module T = struct - type t = path_cond * atom [@@deriving compare, sexp] - end - - include T - include Comparable.Make (T) - end *) - module AtomKey = struct module T = struct type t = atom [@@deriving hash, sexp, compare] @@ -165,3 +156,5 @@ module Z3ExprKey = struct include T include Comparable.Make (T) end + +let choice_empty = Set.empty (module Choice) diff --git a/program_analysis/simple/lib.ml b/program_analysis/simple/lib.ml new file mode 100644 index 0000000..c83de17 --- /dev/null +++ b/program_analysis/simple/lib.ml @@ -0,0 +1,566 @@ +open Core +open Logs +open Option.Let_syntax +open Interp.Ast +open Pa.Exns +open Pa.Logging +open Grammar +open Utils +open Solver +open Simplifier + +(* max recursion depth ever reached by execution *) +let max_d = ref 0 + +let rec eval_assert_aux e = + match e with + | Int i -> IntResFv i + | Bool b -> BoolResFv b + | Plus (e1, e2) + | Minus (e1, e2) + | Equal (e1, e2) + | Ge (e1, e2) + | Gt (e1, e2) + | Le (e1, e2) + | Lt (e1, e2) -> ( + match (eval_assert_aux e1, eval_assert_aux e2) with + | IntResFv i1, IntResFv i2 -> ( + match e with + | Plus _ -> IntResFv (i1 + i2) + | Minus _ -> IntResFv (i1 - i2) + | Equal _ -> BoolResFv (i1 = i2) + | Ge _ -> BoolResFv (i1 >= i2) + | Gt _ -> BoolResFv (i1 > i2) + | Le _ -> BoolResFv (i1 <= i2) + | Lt _ -> BoolResFv (i1 < i2) + | _ -> raise Unreachable) + | _ -> raise Unreachable) + | And (e1, e2) | Or (e1, e2) -> ( + match (eval_assert_aux e1, eval_assert_aux e2) with + | BoolResFv b1, BoolResFv b2 -> ( + match e with + | And _ -> BoolResFv (b1 && b2) + | Or _ -> BoolResFv (b1 || b2) + | _ -> raise Unreachable) + | _ -> raise Unreachable) + | Not e -> ( + match eval_assert_aux e with + | BoolResFv b -> BoolResFv (not b) + | _ -> raise Unreachable) + | _ -> + Format.printf "%a" Interp.Pp.pp_expr e; + raise BadAssert + +(** only allows the following forms: + - arbitrary variable-free arithmetic + - + - not + - *) +let eval_assert e id = + match e with + | Bool b -> BoolResFv b + | Var (id', _) when Stdlib.(id = id') -> VarResFv id' + | Equal (e1, e2) | Ge (e1, e2) | Gt (e1, e2) | Le (e1, e2) | Lt (e1, e2) -> ( + match e1 with + | Var (id', _) when Stdlib.(id = id') -> ( + let v1 = VarResFv id' in + let v2 = eval_assert_aux e2 in + match e with + | Equal _ -> EqResFv (v1, v2) + | Ge _ -> GeResFv (v1, v2) + | Gt _ -> GtResFv (v1, v2) + | Le _ -> LeResFv (v1, v2) + | Lt _ -> LtResFv (v1, v2) + | _ -> raise Unreachable) + | Projection (e1, x) -> failwith "Not supported" + | _ -> ( + let v1, v2 = (eval_assert_aux e1, eval_assert_aux e2) in + match (v1, v2) with + | IntResFv i1, IntResFv i2 -> ( + match e with + | Equal _ -> BoolResFv (i1 = i2) + | Ge _ -> BoolResFv (i1 >= i2) + | Gt _ -> BoolResFv (i1 > i2) + | Le _ -> BoolResFv (i1 <= i2) + | Lt _ -> BoolResFv (i1 < i2) + | _ -> raise Unreachable) + | _ -> raise BadAssert)) + (* TODO: support And/Or (low priority) *) + | Not e' -> ( + match e' with + | Var (id', _) when Stdlib.(id = id') -> NotResFv (VarResFv id') + | _ -> eval_assert_aux e') + | _ -> raise BadAssert + +let log_v_set = Set.iter ~f:(fun st -> debug (fun m -> m "%s" (NewSt.show st))) + +let fold_res_app ~init ~f l sigma d = + List.fold ~init ~f:(fun ((acc_r, acc_s) as acc) a -> + debug (fun m -> + m "[Level %d] [Appl] Evaluating 1 possible function being applied:" d); + debug (fun m -> m "%a" pp_atom a); + match a with + | FunAtom (Function (_, e1, _), _, _) -> f acc e1 + | _ -> (acc_r, acc_s)) + +let fold_res_var ~init ~f expr sigma d r = + List.fold r ~init ~f:(fun ((acc_r, acc_s) as acc) a -> + debug (fun m -> m "r1 length: %d" (List.length r)); + debug (fun m -> m "[Level %d] Visiting 1 possible function for e1:" d); + debug (fun m -> m "%a" pp_atom a); + match a with + | FunAtom (Function (Ident x1, _, l1), _, sigma1) -> f acc x1 l1 sigma1 + | _ -> (acc_r, acc_s)) + +let elim_stub r label = + if exists_stub r label then + (* Format.printf "elim_stub: %a\n" pp_res r; *) + (* Format.printf "label: %a\n" St.pp label; *) + let bases = + List.filter_map r ~f:(fun a -> + match a with + | RecAtom _ when not (exists_stub [ a ] label) -> Some a + | ProjAtom (([ RecAtom es ] as r), Ident key) + when not (exists_stub r label) -> ( + match + List.find es ~f:(fun (Ident key', _) -> String.(key = key')) + with + | Some (_, [ a ]) -> Some a + | _ -> raise Runtime_error) + | FunAtom _ -> Some a + | _ -> None) + in + let r' = + List.concat_map r ~f:(function + | ProjAtom ([ EStubAtom st ], Ident key) when St.(label = Estate st) -> + List.concat_map bases ~f:(fun base -> + match base with + | RecAtom es -> ( + match + List.find es ~f:(fun (Ident key', _) -> + String.(key = key')) + with + | Some (_, r) -> r + | None -> + [] + (* Format.printf "base: %a\n" pp_atom base; + raise Runtime_error *)) + | _ -> raise Runtime_error) + (* fun x -> x | stub *) + | EStubAtom st when St.(label = Estate st) -> [] + | a -> + (* Format.printf "%a\n" pp_atom a; *) + [ a ]) + in + (* Format.printf "result: %a\n" pp_res r'; *) + r' + else r + +let rec analyze_aux_step d expr sigma pi s v v' = + if d > !max_d then max_d := d; + debug_plain "Began recursive call to execution"; + debug (fun m -> m "Max depth so far is: %d" !max_d); + debug (fun m -> m "expr: %a" Interp.Pp.pp_expr expr); + debug (fun m -> m "sigma: %s" (show_sigma sigma)); + let r, s' = + match expr with + | Int i -> ([ IntAnyAtom ], s) + | Bool b -> ([ BoolAtom b ], s) + | Function (_, _, l) -> ([ FunAtom (expr, l, sigma) ], s) + | Appl (e, _, l) -> + let d = d + 1 in + info (fun m -> + m "[Level %d] === Appl (%a) ====" d Interp.Pp.pp_expr expr); + (* debug (fun m -> m "%a" Interp.Ast.pp_expr expr); *) + debug (fun m -> m "sigma: %s" (show_sigma sigma)); + let cycle_label = (l, sigma) in + let sigma' = l :: sigma in + let pruned_sigma' = prune_sigma sigma' in + debug (fun m -> m "sigma_pruned': %s" (show_sigma pruned_sigma')); + let st = (l, sigma, s) in + let st' = (l, sigma) in + (* let st = (l, pruned_sigma', s) in *) + let lst = NewSt.Lstate st in + let lst' = St.Lstate st' in + (* debug (fun m -> m "State: %s" (NewSt.show lst)); *) + (* debug_plain "v_set:"; + log_v_set v; *) + (* TODO: try two-pass mechanism again *) + if Set.mem v lst then ( + debug_plain "Stubbed"; + (* Format.printf "Stubbed\n"; *) + (* debug (fun m -> + m "sigma: %s | take: %s" (show_sigma sigma) + (show_sigma (sigma))); *) + info (fun m -> + m "[Level %d] *** Appl (%a) ****" d Interp.Pp.pp_expr expr); + ([ LStubAtom cycle_label ], s)) + else ( + (* Application *) + debug_plain "Didn't stub"; + debug (fun m -> + m "Evaluating function being applied: %a" Interp.Pp.pp_expr e); + debug (fun m -> + m "Evaluating function being applied: %a" Interp.Ast.pp_expr e); + let new_v = Set.add v lst in + let new_v' = Set.add v' lst' in + (* we don't remember whatever this subtree visited *) + let r1, s1 = analyze_aux_step d e sigma pi s new_v new_v' in + (* let r1 = simplify r1 in *) + debug (fun m -> m "r1 length: %d" (List.length r1)); + let new_s = Set.add s1 pruned_sigma' in + let r2, s2 = + fold_res_app ~init:(choice_empty, new_s) l sigma d r1 + ~f:(fun (acc_r, acc_s) e1 -> + debug (fun m -> + m "[Appl] Evaluating body of function being applied: %a" + Interp.Pp.pp_expr e1); + let ri, si = + analyze_aux_step d e1 pruned_sigma' pi new_s new_v new_v' + in + (List.fold ri ~init:acc_r ~f:Set.add, Set.union acc_s si)) + in + let r2 = Set.elements r2 in + debug (fun m -> m "r2: %a" pp_res r2); + let r2 = elim_stub r2 (St.Lstate cycle_label) in + info (fun m -> + m "[Level %d] *** Appl (%a) ****" d Interp.Pp.pp_expr expr); + (r2, s2)) + | Var (Ident x, l) -> + let d = d + 1 in + info (fun m -> m "[Level %d] === Var (%s, %d) ====" d x l); + let cycle_label = (expr, sigma) in + let st = (expr, sigma, s) in + let st' = (expr, sigma) in + let est = NewSt.Estate st in + let est' = St.Estate st' in + let new_v = Set.add v est in + let new_v' = Set.add v' est' in + (* debug (fun m -> m "State: %s" (Grammar.NewSt.show est)); *) + (* debug_plain "v_set:"; + log_v_set v; *) + if Set.mem v est then ( + (* Var Stub *) + debug (fun m -> m "Stubbed: %s" x); + (* Format.printf "Stubbed: %s\n" x; *) + info (fun m -> m "[Level %d] *** Var (%s, %d) ****" d x l); + ([ EStubAtom cycle_label ], s)) + else ( + debug_plain "Didn't stub"; + match get_myfun l with + | Some (Function (Ident x1, _, l_myfun)) -> + if String.(x = x1) then ( + (* Var Local *) + info (fun m -> m "[Level %d] === Var Local (%s, %d) ====" d x l); + debug (fun m -> m "sigma: %s" (show_sigma sigma)); + let s_hd, s_tl = (List.hd_exn sigma, List.tl_exn sigma) in + match get_myexpr s_hd with + | Appl (_, e2, l') -> + let r1, s1 = + debug_plain "Begin stitching stacks"; + (* debug_plain "S set:"; + debug (fun m -> m "%s" (show_set s)); + debug (fun m -> + m "Head of candidate fragments must be: %d" l'); + debug (fun m -> + m + "Tail of candidate fragments must start with: \ + %s" + (show_sigma s_tl)); *) + (* enumerate all matching stacks in the set *) + Set.fold s ~init:(choice_empty, s) + ~f:(fun (acc_r, acc_s) sigma_i -> + let sigma_i_hd, sigma_i_tl = + (List.hd_exn sigma_i, List.tl_exn sigma_i) + in + (* the fact that we can prune away "bad" stacks like this + makes DDE for program analysis superior *) + if sigma_i_hd = l' && starts_with sigma_i_tl s_tl then ( + debug (fun m -> + m + "[Level %d] Stitched! Evaluating Appl \ + argument, using stitched stack %s:" + d (show_sigma sigma_i_tl)); + debug (fun m -> m "%a" Interp.Pp.pp_expr e2); + (* debug (fun m -> + m "%a" Interp.Ast.pp_expr e2); *) + (* stitch the stack to gain more precision *) + let ri, si = + analyze_aux_step d e2 sigma_i_tl pi s new_v new_v' + in + ( List.fold ri ~init:acc_r ~f:Set.add, + Set.union acc_s si )) + else (acc_r, acc_s)) + in + info (fun m -> + m "[Level %d] *** Var Local (%s, %d) ****" d x l); + info (fun m -> m "[Level %d] *** Var (%s, %d) ****" d x l); + let r1 = Set.elements r1 in + debug (fun m -> m "r1: %a" pp_res r1); + let r1 = elim_stub r1 (St.Estate cycle_label) in + (r1, s1) + | _ -> raise Unreachable [@coverage off]) + else ( + (* Var Non-Local *) + info (fun m -> + m "[Level %d] === Var Non-Local (%s, %d) ====" d x l); + debug (fun m -> m "sigma: %s" (show_sigma sigma)); + debug_plain "Reading Appl at front of sigma"; + match get_myexpr (List.hd_exn sigma) with + | Appl (e1, _, l2) -> + debug_plain "[Var Non-Local] Didn't stub e1"; + debug_plain "Function being applied at front of sigma:"; + debug (fun m -> m "%a" Interp.Pp.pp_expr e1); + debug (fun m -> m "%a" Interp.Ast.pp_expr e1); + let s_tl = List.tl_exn sigma in + debug_plain "Begin stitching stacks"; + (* debug_plain "S set:"; + debug (fun m -> m "%s" (show_set s)); + debug (fun m -> + m "Head of candidate fragments must be: %d" l2); + debug (fun m -> + m "Tail of candidate fragments must start with: %s" + (show_sigma s_tl)); *) + (* enumerate all matching stacks in the set *) + let r1, s1 = + Set.fold s ~init:(choice_empty, s) + ~f:(fun (acc_r, acc_s) si -> + let si_hd, si_tl = (List.hd_exn si, List.tl_exn si) in + if Stdlib.(si_hd = l2) && starts_with si_tl s_tl then ( + debug (fun m -> + m + "[Level %d] Stitched! Evaluating function \ + being applied at front of sigma, using \ + stitched stack %s" + d (show_sigma si_tl)); + (* stitch the stack to gain more precision *) + (* let new_v = + Set.add v (NewSt.Estate (e1, si_tl, s)) + in *) + let r0, s0 = + analyze_aux_step d e1 si_tl pi s v v' + in + ( List.fold r0 ~init:acc_r ~f:Set.add, + Set.union acc_s s0 )) + else (acc_r, acc_s)) + in + let r1 = Set.elements r1 in + (* let r1 = simplify r1 in *) + (* let new_st = (expr, sigma, s1) in + let new_v = Set.add v (NewSt.Estate new_st) in *) + debug_plain + "Found all stitched stacks and evaluated e1, begin \ + relabeling variables"; + let r2, s2 = + fold_res_var ~init:(choice_empty, s1) expr sigma d r1 + ~f:(fun (acc_r, acc_s) x1' l1 sigma1 -> + if Stdlib.(x1 = x1') && l_myfun = l1 then ( + debug (fun m -> + m + "[Var Non-Local] Relabel %s with label %d \ + and evaluate" + x l1); + let r0', s0' = + analyze_aux_step d + (Var (Ident x, l1)) + sigma1 pi s1 new_v new_v' + in + ( List.fold r0' ~init:acc_r ~f:Set.add, + Set.union acc_s s0' )) + else (acc_r, acc_s)) + in + info (fun m -> + m "[Level %d] *** Var Non-Local (%s, %d) ****" d x l); + info (fun m -> m "[Level %d] *** Var (%s, %d) ****" d x l); + let r2 = Set.elements r2 in + debug (fun m -> m "r2: %a" pp_res r2); + let r2 = elim_stub r2 (St.Estate cycle_label) in + (r2, s2) + | _ -> raise Unreachable [@coverage off]) + | _ -> raise Unreachable [@coverage off]) + | If (e, e_true, e_false, l) -> ( + debug (fun m -> m "[Level %d] === If ===" d); + let d = d + 1 in + let r_cond, s_cond = analyze_aux_step d e sigma None s v v' in + (* TODO: why do I need the following line? *) + (* let r_cond = simplify r_cond in *) + (* Format.printf "r_cond: %a\n" pp_res r_cond; *) + match r_cond with + (* TODO *) + | [ BoolAtom b ] -> + debug (fun m -> m "[Level %d] === If %b ===" d b); + if b then ( + let r_true, s_true = + analyze_aux_step d e_true sigma None s v v' + in + debug (fun m -> m "[Level %d] *** If %b ***" d b); + (r_true, Set.union s_cond s_true)) + else + let r_false, s_false = + analyze_aux_step d e_false sigma None s v v' + in + debug (fun m -> m "[Level %d] *** If %b ***" d b); + (r_false, Set.union s_cond s_false) + | _ -> + debug (fun m -> m "[Level %d] === If Both ===" d); + (* Format.printf "r_cond: %a\n" pp_res r_cond; *) + let r_true, s_true = analyze_aux_step d e_true sigma None s v v' in + info (fun m -> m "Evaluating: %a" Interp.Pp.pp_expr e_false); + let r_false, s_false = + analyze_aux_step d e_false sigma None s v v' + in + debug (fun m -> m "[Level %d] *** If Both ***" d); + (r_true @ r_false, Set.union s (Set.union s_true s_false))) + | Plus (e1, e2) + | Minus (e1, e2) + | Mult (e1, e2) + | Equal (e1, e2) + | And (e1, e2) + | Or (e1, e2) + | Ge (e1, e2) + | Gt (e1, e2) + | Le (e1, e2) + | Lt (e1, e2) -> + let d = d + 1 in + info (fun m -> + m "[Level %d] === Binop (%a) ====" d Interp.Pp.pp_expr expr); + (* Format.printf "e1: %a | e2: %a\n" pp_expr e1 pp_expr e2; *) + let r1, s1 = analyze_aux_step d e1 sigma pi s v v' in + let r2, s2 = analyze_aux_step d e2 sigma pi s1 v v' in + debug (fun m -> + m "[Level %d] Evaluated binop to (%a %a)" d Utils.pp_res r1 + Utils.pp_res r2); + debug (fun m -> + m "[Level %d] Evaluated binop to (%a %a)" d Grammar.pp_res r1 + Grammar.pp_res r2); + info (fun m -> + m "[Level %d] *** Binop (%a) ****" d Interp.Pp.pp_expr expr); + ( (match expr with + | Plus _ -> ( + match (r1, r2) with + | [ IntAtom i1 ], [ IntAtom i2 ] -> [ IntAtom (i1 + i2) ] + | _ -> + (* Format.printf "Plus: r1: %a | r2: %a\n" pp_res r1 pp_res + r2; *) + [ IntAnyAtom ]) + | Minus _ -> [ IntAnyAtom ] + | Mult _ -> ( + match (r1, r2) with + | [ IntAtom i1 ], [ IntAtom i2 ] -> [ IntAtom (i1 * i2) ] + | r1', r2' -> [ IntAnyAtom ]) + | And _ -> ( + match (r1, r2) with + | [ BoolAtom b1 ], [ BoolAtom b2 ] -> [ BoolAtom (b1 && b2) ] + | [ BoolAtom b11; BoolAtom b12 ], [ BoolAtom b2 ] -> + let b1 = b11 && b2 in + let b2 = b12 && b2 in + [ BoolAtom (b1 || b2) ] + | [ BoolAtom b1 ], [ BoolAtom b21; BoolAtom b22 ] -> + let b1 = b1 && b21 in + let b2 = b1 && b22 in + [ BoolAtom (b1 || b2) ] + | [ BoolAtom b11; BoolAtom b12 ], [ BoolAtom b21; BoolAtom b22 ] + -> + let b1 = (b11 && b21) || (b11 && b22) in + let b2 = (b12 && b21) || (b12 && b22) in + [ BoolAtom (b1 || b2) ] + | _ -> + (* Format.printf "r1: %a | r2: %a\n" pp_res r1 pp_res r2; *) + [ BoolAtom true; BoolAtom false ]) + | Or _ -> ( + match (r1, r2) with + | [ BoolAtom b1 ], [ BoolAtom b2 ] -> [ BoolAtom (b1 || b2) ] + | [ BoolAtom b11; BoolAtom b12 ], [ BoolAtom b2 ] -> + let b1 = b11 || b2 in + let b2 = b12 || b2 in + [ BoolAtom (b1 || b2) ] + | [ BoolAtom b1 ], [ BoolAtom b21; BoolAtom b22 ] -> + let b1 = b1 || b21 in + let b2 = b1 || b22 in + [ BoolAtom (b1 || b2) ] + | [ BoolAtom b11; BoolAtom b12 ], [ BoolAtom b21; BoolAtom b22 ] + -> + let b1 = (b11 || b21) || b11 || b22 in + let b2 = (b12 || b21) || b12 || b22 in + [ BoolAtom (b1 || b2) ] + | _ -> + (* Format.printf "r1: %a | r2: %a\n" pp_res r1 pp_res r2; *) + [ BoolAtom true; BoolAtom false ]) + | Equal _ | Ge _ | Gt _ | Le _ | Lt _ -> + [ BoolAtom true; BoolAtom false ] + | _ -> + Format.printf "%a\n" pp_expr expr; + raise Unreachable [@coverage off]), + Set.union s (Set.union s1 s2) ) + | Not e -> ( + let d = d + 1 in + let r, s = analyze_aux_step d e sigma pi s v v' in + match r with + | [ BoolAtom b ] -> + (* Format.printf "%a\n" pp_res r; *) + ([ BoolAtom (not b) ], s) + | [] -> ([], s) + | _ -> ([ BoolAtom false; BoolAtom true ], s)) + | Record entries -> + let d = d + 1 in + ( [ + RecAtom + (entries + |> List.map ~f:(fun (x, ei) -> + ( x, + let r, _ = analyze_aux_step d ei sigma pi s v v' in + r ))); + ], + s ) + | Projection (e, Ident key) -> + debug (fun m -> m "[Level %d] === Projection ===" d); + let d = d + 1 in + let r0, s0 = analyze_aux_step d e sigma pi s v v' in + ([ ProjAtom (r0, Ident key) ], s0) + | Inspection (Ident key, e) -> + let d = d + 1 in + let r0, s0 = analyze_aux_step d e sigma pi s v v' in + ([ InspAtom (Ident key, r0) ], s0) + | LetAssert (id, e1, e2) -> + let d = d + 1 in + let r1, s1 = analyze_aux_step d e1 sigma pi s v v' in + let r2 = eval_assert e2 id in + ([ AssertAtom (id, r1, r2) ], s1) + | Let _ -> raise Unreachable [@coverage off] + in + (simplify r, s') +(* (r, s') *) +(* TODO: run with poor man's cache first then use S to rerun *) + +let analyze ?(debug_mode = false) ?(verify = true) ?(test_num = 0) + ?(should_cache = true) e = + is_debug_mode := debug_mode; + + let e = transform_let e in + build_myfun e None; + debug (fun m -> m "%a" Interp.Pp.pp_expr e); + debug (fun m -> m "%a" pp_expr e); + + (* Format.printf "%a\n" pp_expr e; *) + let r, s = + analyze_aux_step 0 e [] None + (Set.empty (module SKey)) + (Set.empty (module NewSt)) + (Set.empty (module St)) + in + + (* let r = simplify r in *) + (* dot_of_result test_num r; *) + debug (fun m -> m "Result: %a" Utils.pp_res r); + debug (fun m -> m "Result: %a" Grammar.pp_res r); + (if !is_debug_mode then ( + Format.printf "\n%s\n\n" @@ show_expr e; + Format.printf "****** Label Table ******\n"; + Interp.Lib.print_myexpr myexpr; + Format.printf "****** Label Table ******\n\n")) + [@coverage off]; + + clean_up (); + + (* if verify then verify_result r; *) + r diff --git a/program_analysis/simple/simplifier.ml b/program_analysis/simple/simplifier.ml new file mode 100644 index 0000000..87154ad --- /dev/null +++ b/program_analysis/simple/simplifier.ml @@ -0,0 +1,59 @@ +open Core +open Interp.Ast +open Pa.Exns +open Grammar + +let rec exists_stub r label = + List.exists r ~f:(function + | FunAtom _ | IntAtom _ | IntAnyAtom | BoolAtom _ -> false + | LStubAtom st -> St.(label = St.Lstate st) + | EStubAtom st -> St.(label = St.Estate st) + | RecAtom entries -> + List.exists entries ~f:(fun (_, r) -> exists_stub r label) + | ProjAtom (r, _) | InspAtom (_, r) | AssertAtom (_, r, _) -> + exists_stub r label) + +let rec simplify ?(pa = None) r = + let r' = + List.filter_map r ~f:(fun a -> + match a with + | IntAtom _ | IntAnyAtom | BoolAtom _ | LStubAtom _ | EStubAtom _ + | FunAtom _ -> + Some [ a ] + | AssertAtom (id, r, rv) -> + Some [ AssertAtom (id, simplify r ~pa:(Some a), rv) ] + | RecAtom rs -> + Some + [ + RecAtom + (List.map rs ~f:(fun (id, r) -> (id, simplify r ~pa:(Some a)))); + ] + | ProjAtom (r, id) -> + Some + (List.concat_map r ~f:(fun a -> + match a with + | RecAtom rs -> ( + match + List.find rs ~f:(fun (id', _) -> + compare_ident id id' = 0) + with + | Some (_, r) -> r + | None -> + (* [ ProjAtom ([ a ], id) ] *) + []) + | a -> + (* Format.printf "%a\n" pp_atom a; *) + [ ProjAtom ([ a ], id) ])) + | InspAtom (id, r) -> + Some + (List.concat_map r ~f:(function + | RecAtom rs -> + [ + BoolAtom + (List.exists rs ~f:(fun (id', _) -> + compare_ident id id' = 0)); + ] + | a -> [ InspAtom (id, [ a ]) ]))) + in + let r' = List.concat r' in + if compare_res r r' = 0 then r' else simplify r' ~pa diff --git a/program_analysis/reworked/solver.ml b/program_analysis/simple/solver.ml similarity index 100% rename from program_analysis/reworked/solver.ml rename to program_analysis/simple/solver.ml diff --git a/program_analysis/simple/utils.ml b/program_analysis/simple/utils.ml new file mode 100644 index 0000000..cd4f1ed --- /dev/null +++ b/program_analysis/simple/utils.ml @@ -0,0 +1,82 @@ +open Core +open Interp.Ast +open Grammar + +let pf = Format.printf +let pfl = pf "%s\n" +let prune_sigma ?(k = 2) s = List.filteri s ~f:(fun i _ -> i < k) +let take_sigma ?(k = 2) = Fn.flip List.take (k - 1) + +let rec starts_with sigma_parent sigma_child = + match (sigma_parent, sigma_child) with + | _, [] -> true + | [], _ -> false + | l_parent :: ls_parent, l_child :: ls_child -> + l_parent = l_child && starts_with ls_parent ls_child + +let show_set = Set.fold ~init:"" ~f:(fun acc s -> show_sigma s ^ "\n" ^ acc) +let pp_pair fmt (l, s) = Format.fprintf fmt "(%d, %s)" l @@ show_sigma s +let pp_pair_list fmt ls = Format.pp_print_list pp_pair fmt ls +let is_debug_mode = ref false + +let all_combs l1 l2 = + Set.fold l1 ~init:[] ~f:(fun acc x -> + Set.fold l2 ~init:[] ~f:(fun acc y -> (x, y) :: acc)) + +let ff = Format.fprintf + +let rec pp_atom fmt = function + | IntAnyAtom -> ff fmt "Int" + | IntAtom i -> ff fmt "%d" i + | BoolAtom b -> ff fmt "%b" b + | FunAtom (f, _, _) -> Interp.Pp.pp_expr fmt f + (* | LabelResAtom (choices, _) -> ff fmt "%a" pp_res choices + | ExprResAtom (choices, _) -> ff fmt "%a" pp_res choices + | LabelStubAtom _ -> ff fmt "stub" + | ExprStubAtom _ -> ff fmt "stub" *) + (* | LabelResAtom (choices, (l, _)) -> ff fmt "(%a)^%d" pp_res choices l + | ExprResAtom (choices, (e, _)) -> + ff fmt "(%a)^%a" pp_res choices Interpreter.Pp.pp_expr e + | LabelStubAtom (l, _) -> ff fmt "stub@%d" l + | ExprStubAtom (e, _) -> ff fmt "(stub@%a)" Interpreter.Pp.pp_expr e *) + (* | OpAtom op -> ( + match op with + | PlusOp (r1, r2) -> ff fmt "(%a + %a)" pp_res r1 pp_res r2 + | MinusOp (r1, r2) -> ff fmt "(%a - %a)" pp_res r1 pp_res r2 + | MultOp (r1, r2) -> ff fmt "(%a * %a)" pp_res r1 pp_res r2 + | EqualOp (r1, r2) -> ff fmt "(%a = %a)" pp_res r1 pp_res r2 + | AndOp (r1, r2) -> ff fmt "(%a and %a)" pp_res r1 pp_res r2 + | OrOp (r1, r2) -> ff fmt "(%a or %a)" pp_res r1 pp_res r2 + | GeOp (r1, r2) -> ff fmt "(%a >= %a)" pp_res r1 pp_res r2 + | GtOp (r1, r2) -> ff fmt "(%a > %a)" pp_res r1 pp_res r2 + | LeOp (r1, r2) -> ff fmt "(%a <= %a)" pp_res r1 pp_res r2 + | LtOp (r1, r2) -> ff fmt "(%a < %a)" pp_res r1 pp_res r2 + | NotOp r1 -> ff fmt "(not %a)" pp_res r1) *) + (* | EquivStubAtom (s, l) -> + ff fmt "{%s}[%d]" + (s |> Set.to_list + |> List.map ~f:(fun st -> Format.sprintf "%s" (St.show st)) + |> String.concat ~sep:", ") + l *) + (* | PathCondAtom (_, r) -> ff fmt "%a" pp_res r *) + (* | PathCondAtom ((r, b), r') -> ff fmt "(%a = %b ⊩ %a)" pp_res r b pp_res r' *) + | LStubAtom _ -> ff fmt "stub" + | EStubAtom _ -> ff fmt "stub" + | RecAtom entries -> + ff fmt + (if List.length entries = 0 then "{%a}" else "{ %a }") + pp_record_atom entries + | ProjAtom (r, Ident s) -> ff fmt "(%a.%s)" pp_res r s + | InspAtom (Ident s, r) -> ff fmt "(%s in %a)" s pp_res r + | AssertAtom (_, r, _) -> ff fmt "%a" pp_res r + +and pp_record_atom fmt = function + | [] -> () + | [ (Ident x, v) ] -> Format.fprintf fmt "%s = %a" x pp_res v + | (Ident x, v) :: rest -> + Format.fprintf fmt "%s = %a; %a" x pp_res v pp_record_atom rest + +and pp_res fmt = function + | [] -> () + | [ a ] -> ff fmt "%a" pp_atom a + | a :: _as -> ff fmt "(%a | %a)" pp_atom a pp_res _as diff --git a/program_analysis/src/debugutils.ml b/program_analysis/src/debugutils.ml index fc9972f..e485ba9 100644 --- a/program_analysis/src/debugutils.ml +++ b/program_analysis/src/debugutils.ml @@ -6,12 +6,11 @@ open Utils let is_debug_mode = ref false let parse s = - s ^ ";;" |> Lexing.from_string - |> Interpreter.Parser.main Interpreter.Lexer.token + s ^ ";;" |> Lexing.from_string |> Interp.Parser.main Interp.Lexer.token |> fun e -> (* keep labeling consistent across multiple calls to `analyze` *) - Interpreter.Ast.reset_label (); + Interp.Ast.reset_label (); e let unparse = Format.asprintf "%a" pp_res diff --git a/program_analysis/src/dune b/program_analysis/src/dune index 4886a1e..6f06a2c 100644 --- a/program_analysis/src/dune +++ b/program_analysis/src/dune @@ -1,17 +1,17 @@ (library - (name program_analysis) - (public_name dde.program_analysis) + (name pa) + (public_name dde.pa) (preprocess (pps bisect_ppx ppx_deriving.show ppx_let ppx_jane landmarks-ppx --auto)) (instrumentation (backend bisect_ppx --bisect-file _build/bisect)) (instrumentation (backend landmarks --auto)) - (modules lib grammar solver simplifier utils debugutils) - (libraries dde.interpreter hashset core z3 logs logs.fmt)) + (modules lib grammar solver simplifier utils debugutils exns logging) + (libraries dde.interp hashset core z3 logs logs.fmt)) (executable (name main) (modes byte) (modules main) - (libraries program_analysis)) + (libraries pa)) diff --git a/program_analysis/src/exns.ml b/program_analysis/src/exns.ml new file mode 100644 index 0000000..4064812 --- /dev/null +++ b/program_analysis/src/exns.ml @@ -0,0 +1,3 @@ +exception Unreachable +exception BadAssert +exception Runtime_error diff --git a/program_analysis/src/grammar.ml b/program_analysis/src/grammar.ml index 40944a5..37041c2 100644 --- a/program_analysis/src/grammar.ml +++ b/program_analysis/src/grammar.ml @@ -1,5 +1,5 @@ open Core -open Interpreter.Ast +open Interp.Ast module S_key = struct module T = struct @@ -52,8 +52,8 @@ module NewSt = struct [@@deriving compare, sexp, hash] let show_estate (e, sigma, s) = - Format.asprintf "(%a, %s, {%s})" Interpreter.Ast.pp_expr e - (show_sigma sigma) (show_set s) + Format.asprintf "(%a, %s, {%s})" Interp.Ast.pp_expr e (show_sigma sigma) + (show_set s) let pp_estate fmt est = Format.fprintf fmt "%s" (show_estate est) diff --git a/program_analysis/src/lib.ml b/program_analysis/src/lib.ml index b240576..3a4387a 100644 --- a/program_analysis/src/lib.ml +++ b/program_analysis/src/lib.ml @@ -1,42 +1,29 @@ open Core open Logs -open Interpreter.Ast +open Interp.Ast open Grammar open Grammar.Let_syntax open Utils open Solver open Simplifier +open Exns +open Logging -exception Unreachable -exception BadAssert -exception Runtime_error - -(* controls whether to generate logs: - "logs" in _build/default/program_analysis/tests *) -let gen_logs = ref false -let debug_plain msg = if !gen_logs then debug (fun m -> m msg) -let debug msg = if !gen_logs then debug msg -let info_plain msg = if !gen_logs then info msg -let info msg = if !gen_logs then info msg - -(* maximum recursion depth ever reached by execution so far *) +(* max recursion depth ever reached by execution *) let max_d = ref 0 let solve_cond r b = - (* let solver = Z3.Solver.mk_solver_s ctx "HORN" in *) Solver.chcs_of_res r; let p = Option.value_exn !Solver.entry_decl in let chcs = Hash_set.to_list Solver.chcs in let rb = zconst "r" bsort in let manual = [ rb ] |. (p <-- [ rb ]) --> (rb === zbool b) in - let chcs = manual :: chcs in - Z3.Solver.add solver chcs; + Z3.Solver.add solver (manual :: chcs); - (* let start = Stdlib.Sys.time () in *) - let status = Z3.Solver.check solver [] in - (* Format.printf "cond execution time: %f\n" (Stdlib.Sys.time () -. start); *) let sat = - match status with SATISFIABLE -> true | UNSATISFIABLE | UNKNOWN -> false + match Z3.Solver.check solver [] with + | SATISFIABLE -> true + | UNSATISFIABLE | UNKNOWN -> false in Solver.reset (); sat @@ -77,7 +64,7 @@ let rec eval_assert_aux e = | BoolResFv b -> BoolResFv (not b) | _ -> raise Unreachable) | _ -> - Format.printf "%a" Interpreter.Pp.pp_expr e; + Format.printf "%a" Interp.Pp.pp_expr e; raise BadAssert (** only allows the following forms: @@ -238,7 +225,7 @@ let rec analyze_aux_step d expr sigma pi s v = if d > !max_d then max_d := d; debug_plain "Began recursive call to execution"; debug (fun m -> m "Max depth so far is: %d" !max_d); - debug (fun m -> m "expr: %a" Interpreter.Pp.pp_expr expr); + debug (fun m -> m "expr: %a" Interp.Pp.pp_expr expr); debug (fun m -> m "sigma: %s" (show_sigma sigma)); let r, s' = let d = d + 1 in @@ -248,8 +235,8 @@ let rec analyze_aux_step d expr sigma pi s v = | Function (_, _, l) -> ([ FunAtom (expr, l, sigma) ], s) | Appl (e, _, l) -> info (fun m -> - m "[Level %d] ====== Appl (%a) ======" d Interpreter.Pp.pp_expr expr); - debug (fun m -> m "%a" Interpreter.Ast.pp_expr expr); + m "[Level %d] ====== Appl (%a) ======" d Interp.Pp.pp_expr expr); + debug (fun m -> m "%a" Interp.Ast.pp_expr expr); debug (fun m -> m "sigma: %s" (show_sigma sigma)); let sigma' = l :: sigma in let pruned_sigma' = prune_sigma sigma' in @@ -265,17 +252,15 @@ let rec analyze_aux_step d expr sigma pi s v = if Set.mem v lst then ( debug_plain "Stubbed"; info (fun m -> - m "[Level %d] ****** Appl (%a) *******" d Interpreter.Pp.pp_expr - expr); + m "[Level %d] ****** Appl (%a) *******" d Interp.Pp.pp_expr expr); ([ LStubAtom stub_key ], s)) else ( (* Application *) debug_plain "Didn't stub"; debug (fun m -> - m "Evaluating function being applied: %a" Interpreter.Pp.pp_expr e); + m "Evaluating function being applied: %a" Interp.Pp.pp_expr e); debug (fun m -> - m "Evaluating function being applied: %a" Interpreter.Ast.pp_expr - e); + m "Evaluating function being applied: %a" Interp.Ast.pp_expr e); let new_v = Set.add v lst in (* we don't remember whatever this subtree visited *) let r1, s1 = analyze_aux_step d e sigma pi s new_v in @@ -288,7 +273,7 @@ let rec analyze_aux_step d expr sigma pi s v = ~f:(fun (acc_r, acc_s) e1 -> debug (fun m -> m "[Appl] Evaluating body of function being applied: %a" - Interpreter.Pp.pp_expr e1); + Interp.Pp.pp_expr e1); let ri, si = analyze_aux_step d e1 pruned_sigma' pi new_s new_v in @@ -298,8 +283,7 @@ let rec analyze_aux_step d expr sigma pi s v = let r2 = elim_stub r2 (St.Lstate stub_key) in let r2 = [ LResAtom (r2, stub_key) ] in info (fun m -> - m "[Level %d] ****** Appl (%a) *******" d Interpreter.Pp.pp_expr - expr); + m "[Level %d] ****** Appl (%a) *******" d Interp.Pp.pp_expr expr); (r2, s2)) | Var (Ident x, l) -> info (fun m -> m "[Level %d] ====== Var (%s, %d) ======" d x l); @@ -350,8 +334,8 @@ let rec analyze_aux_step d expr sigma pi s v = "[Level %d] Stitched! Evaluating Appl \ argument, using stitched stack %s:" d (show_sigma sigma_i_tl)); - debug (fun m -> m "%a" Interpreter.Pp.pp_expr e2); - debug (fun m -> m "%a" Interpreter.Ast.pp_expr e2); + debug (fun m -> m "%a" Interp.Pp.pp_expr e2); + debug (fun m -> m "%a" Interp.Ast.pp_expr e2); (* stitch the stack to gain more precision *) let ri, si = analyze_aux_step d e2 sigma_i_tl pi s new_v @@ -379,8 +363,8 @@ let rec analyze_aux_step d expr sigma pi s v = | Appl (e1, _, l2) -> debug_plain "[Var Non-Local] Didn't stub e1"; debug_plain "Function being applied at front of sigma:"; - debug (fun m -> m "%a" Interpreter.Pp.pp_expr e1); - debug (fun m -> m "%a" Interpreter.Ast.pp_expr e1); + debug (fun m -> m "%a" Interp.Pp.pp_expr e1); + debug (fun m -> m "%a" Interp.Ast.pp_expr e1); let s_tl = List.tl_exn sigma in debug_plain "Begin stitching stacks"; debug_plain "S set:"; @@ -459,7 +443,7 @@ let rec analyze_aux_step d expr sigma pi s v = match (true_sat, false_sat) with | true, false -> info (fun m -> m "[Level %d] ====== If True only ======" d); - debug (fun m -> m "Evaluating: %a" Interpreter.Pp.pp_expr e_true); + debug (fun m -> m "Evaluating: %a" Interp.Pp.pp_expr e_true); let r_true, s_true = analyze_aux_step d e_true sigma (Some pc_true) s0 v in @@ -468,7 +452,7 @@ let rec analyze_aux_step d expr sigma pi s v = ([ PathCondAtom (pc_true, r_true) ], Set.union s0 s_true) | false, true -> info (fun m -> m "[Level %d] ====== If False only ======" d); - debug (fun m -> m "Evaluating: %a" Interpreter.Pp.pp_expr e_false); + debug (fun m -> m "Evaluating: %a" Interp.Pp.pp_expr e_false); let r_false, s_false = analyze_aux_step d e_false sigma (Some pc_false) s0 v in @@ -478,13 +462,13 @@ let rec analyze_aux_step d expr sigma pi s v = | _ -> info (fun m -> m "[Level %d] ====== If both ======" d); info (fun m -> m "[Level %d] ====== If True ======" d); - debug (fun m -> m "Evaluating: %a" Interpreter.Pp.pp_expr e_true); + debug (fun m -> m "Evaluating: %a" Interp.Pp.pp_expr e_true); let r_true, s_true = analyze_aux_step d e_true sigma (Some pc_true) s0 v in info (fun m -> m "[Level %d] ****** If True ******" d); info (fun m -> m "[Level %d] ====== If False ======" d); - debug (fun m -> m "Evaluating: %a" Interpreter.Pp.pp_expr e_false); + debug (fun m -> m "Evaluating: %a" Interp.Pp.pp_expr e_false); let r_false, s_false = analyze_aux_step d e_false sigma (Some pc_false) s0 v in @@ -505,8 +489,7 @@ let rec analyze_aux_step d expr sigma pi s v = | Le (e1, e2) | Lt (e1, e2) -> info (fun m -> - m "[Level %d] ====== Binop (%a) ======" d Interpreter.Pp.pp_expr - expr); + m "[Level %d] ====== Binop (%a) ======" d Interp.Pp.pp_expr expr); let r1, s1 = analyze_aux_step d e1 sigma pi s v in let r2, s2 = analyze_aux_step d e2 sigma pi s1 v in debug (fun m -> @@ -516,8 +499,7 @@ let rec analyze_aux_step d expr sigma pi s v = m "[Level %d] Evaluated binop to (%a %a)" d Grammar.pp_res r1 Grammar.pp_res r2); info (fun m -> - m "[Level %d] ****** Binop (%a) *******" d Interpreter.Pp.pp_expr - expr); + m "[Level %d] ****** Binop (%a) *******" d Interp.Pp.pp_expr expr); ( [ (match expr with | Plus _ -> PlusAtom (r1, r2) @@ -600,13 +582,13 @@ let analyze ?(debug_mode = false) ?(verify = true) ?(test_num = 0) e = (Set.empty (module NewSt)) in (* let r = simplify r in *) - dot_of_result test_num r; + (* dot_of_result test_num r; *) debug (fun m -> m "Result: %a" Utils.pp_res r); debug (fun m -> m "Result: %a" Grammar.pp_res r); (if !is_debug_mode then ( Format.printf "\n%s\n\n" @@ show_expr e; Format.printf "****** Label Table ******\n"; - Interpreter.Interp.print_myexpr myexpr; + Interp.Lib.print_myexpr myexpr; Format.printf "****** Label Table ******\n\n")) [@coverage off]; diff --git a/program_analysis/src/logging.ml b/program_analysis/src/logging.ml new file mode 100644 index 0000000..a6c127b --- /dev/null +++ b/program_analysis/src/logging.ml @@ -0,0 +1,9 @@ +open Logs + +(* controls whether to generate logs: + "logs" in _build/default/program_analysis/tests *) +let gen_logs = ref false +let debug_plain msg = if !gen_logs then debug (fun m -> m msg) +let debug msg = if !gen_logs then debug msg +let info_plain msg = if !gen_logs then info msg +let info msg = if !gen_logs then info msg diff --git a/program_analysis/src/main.ml b/program_analysis/src/main.ml index d700226..da9258a 100644 --- a/program_analysis/src/main.ml +++ b/program_analysis/src/main.ml @@ -1,4 +1,4 @@ -open Program_analysis +open Pa let toplevel_loop = let print_exception ex = @@ -10,7 +10,7 @@ let toplevel_loop = let safe_parse () = try let lexbuf = Lexing.from_channel stdin in - Some (Interpreter.Parser.main Interpreter.Lexer.token lexbuf) + Some (Interp.Parser.main Interp.Lexer.token lexbuf) with | Exit -> exit 0 | ex -> diff --git a/program_analysis/src/simplifier.ml b/program_analysis/src/simplifier.ml index d116da1..372e3a9 100644 --- a/program_analysis/src/simplifier.ml +++ b/program_analysis/src/simplifier.ml @@ -1,9 +1,7 @@ open Core +open Interp.Ast open Grammar -open Interpreter.Ast - -exception Unreachable -exception Runtime_error +open Exns let rec exists_stub r label = List.exists r ~f:(function @@ -32,6 +30,19 @@ let rec exists_stub r label = | OrAtom (r1, r2) -> exists_stub r1 label || exists_stub r2 label) +let int_op = function + | EqAtom _ -> ( = ) + | GeAtom _ -> ( >= ) + | GtAtom _ -> ( > ) + | LeAtom _ -> ( <= ) + | LtAtom _ -> ( < ) + | _ -> raise Unreachable + +let bool_op = function + | AndAtom _ -> ( && ) + | OrAtom _ -> ( || ) + | _ -> raise Unreachable + let rec simplify ?(pa = None) r = let r' = List.filter_map r ~f:(fun a -> @@ -212,17 +223,9 @@ let rec simplify ?(pa = None) r = | GtAtom (r1, r2) | LeAtom (r1, r2) | LtAtom (r1, r2) -> ( - let int_op = - match a with - | EqAtom _ -> ( = ) - | GeAtom _ -> ( >= ) - | GtAtom _ -> ( > ) - | LeAtom _ -> ( <= ) - | LtAtom _ -> ( < ) - | _ -> raise Unreachable - in match (r1, r2) with - | [ IntAtom i1 ], [ IntAtom i2 ] -> Some [ BoolAtom (int_op i1 i2) ] + | [ IntAtom i1 ], [ IntAtom i2 ] -> + Some [ BoolAtom (int_op a i1 i2) ] | _ -> let r1', r2' = (simplify r1 ~pa:(Some a), simplify r2 ~pa:(Some a)) @@ -237,27 +240,19 @@ let rec simplify ?(pa = None) r = | LtAtom _ -> LtAtom (r1', r2') | _ -> raise Unreachable); ]) - | AndAtom (r1, r2) | OrAtom (r1, r2) -> ( - let bool_op = - match a with - | AndAtom _ -> ( && ) - | OrAtom _ -> ( || ) - | _ -> raise Unreachable - in - match (r1, r2) with - | [ BoolAtom b1 ], [ BoolAtom b2 ] -> - Some [ BoolAtom (bool_op b1 b2) ] - | _ -> - let r1', r2' = - (simplify r1 ~pa:(Some a), simplify r2 ~pa:(Some a)) - in - Some - [ - (match a with - | AndAtom _ -> AndAtom (r1', r2') - | OrAtom _ -> OrAtom (r1', r2') - | _ -> raise Unreachable); - ]) + | AndAtom (r1, r2) | OrAtom (r1, r2) -> + Some + (List.concat_map r1 ~f:(fun a1 -> + List.map r2 ~f:(fun a2 -> + match (a1, a2) with + | BoolAtom b1, BoolAtom b2 -> BoolAtom (bool_op a b1 b2) + | _ -> ( + let r1' = simplify r1 ~pa:(Some a) in + let r2' = simplify r2 ~pa:(Some a) in + match a with + | AndAtom _ -> AndAtom (r1', r2') + | OrAtom _ -> OrAtom (r1', r2') + | _ -> raise Unreachable)))) | NotAtom r -> ( match r with | [ BoolAtom b ] -> Some [ BoolAtom (not b) ] diff --git a/program_analysis/src/solver.ml b/program_analysis/src/solver.ml index f0e6831..795eb77 100644 --- a/program_analysis/src/solver.ml +++ b/program_analysis/src/solver.ml @@ -100,7 +100,7 @@ let reset () = fresh_id := -1 (** can assume good form due to call to `eval_assert` *) -let chcs_of_assert r1 (r2 : Interpreter.Ast.res_val_fv) = +let chcs_of_assert r1 (r2 : Interp.Ast.res_val_fv) = let p = Hashtbl.find_exn id_to_decl (idr r1) in let ri = zconst "r" isort in let rb = zconst "r" bsort in diff --git a/program_analysis/src/utils.ml b/program_analysis/src/utils.ml index 90396ca..0f799fa 100644 --- a/program_analysis/src/utils.ml +++ b/program_analysis/src/utils.ml @@ -1,5 +1,5 @@ open Core -open Interpreter.Ast +open Interp.Ast open Grammar exception Unreachable @@ -30,7 +30,7 @@ let ff = Format.fprintf let rec pp_atom fmt = function | IntAtom x -> ff fmt "%d" x | BoolAtom b -> ff fmt "%b" b - | FunAtom (f, _, _) -> Interpreter.Pp.pp_expr fmt f + | FunAtom (f, _, _) -> Interp.Pp.pp_expr fmt f | LResAtom (choices, _) -> ff fmt "%a" pp_res choices | EResAtom (choices, _) -> ff fmt "%a" pp_res choices | LStubAtom _ -> ff fmt "stub" @@ -101,7 +101,7 @@ type latom = | LRecAtom of (ident * lres) list * int | LProjAtom of lres * ident | LInspAtom of ident * lres - | LAssertAtom of ident * lres * Interpreter.Ast.res_val_fv + | LAssertAtom of ident * lres * Interp.Ast.res_val_fv and lres = latom list @@ -129,7 +129,7 @@ end let rec ppp_latom fmt = function | LIntAtom (x, _) -> ff fmt "%d" x | LBoolAtom (b, _) -> ff fmt "%b" b - | LFunAtom (f, _, _) -> Interpreter.Pp.pp_expr fmt f + | LFunAtom (f, _, _) -> Interp.Pp.pp_expr fmt f | LLResAtom (choices, _, _) | LEResAtom (choices, _, _) -> ff fmt "%a" ppp_lres choices (* ff fmt "(%a, %a, %a)" pp_res choices Interpreter.Pp.pp_expr e pp_sigma s *) @@ -373,8 +373,7 @@ let dot_of_result ?(display_path_cond = true) test_num r = add_edge xid rid; let rvid = Format.sprintf "%s_assn" aid in add_node - (Format.asprintf "%s [label=\"%a\"];" rvid - Interpreter.Pp.pp_res_val_fv rv); + (Format.asprintf "%s [label=\"%a\"];" rvid Interp.Pp.pp_res_val_fv rv); add_edge aid rvid; (* add_sibling aid xid; add_sibling aid rvid; *) diff --git a/program_analysis/tests/dune b/program_analysis/tests/dune index 98a0f59..ef939aa 100644 --- a/program_analysis/tests/dune +++ b/program_analysis/tests/dune @@ -5,10 +5,10 @@ core core_bench core_unix.command_unix - dde.interpreter + dde.interp dde.dinterp - dde.program_analysis - dde.pa_reworked + dde.pa + dde.simple_pa dde.display_pa fbdk.fb ounit2 diff --git a/program_analysis/tests/test_cases.ml b/program_analysis/tests/test_cases.ml index d5ec707..861a236 100644 --- a/program_analysis/tests/test_cases.ml +++ b/program_analysis/tests/test_cases.ml @@ -1,5 +1,5 @@ open Core -open Program_analysis.Solver +open Pa.Solver let ri = zconst "r" isort let rb = zconst "r" bsort diff --git a/program_analysis/tests/tests.ml b/program_analysis/tests/tests.ml index 66f3261..b2b8afb 100644 --- a/program_analysis/tests/tests.ml +++ b/program_analysis/tests/tests.ml @@ -104,36 +104,6 @@ let recursion_thunked = let test_recursion _ = gen_test recursion_thunked -let lossy_core_thunked = - [ - (* (fun _ -> ("Int", pau'' ~verify:false (read_input "ack.ml"))); *) - (* (fun _ -> ("false", pau' ~verify:false (read_input "blur.ml"))); *) - (* (fun _ -> ("Int", pau' ~verify:false (read_input "cpstak.ml"))); *) - (fun _ -> ("false", pau' ~verify:false (read_input "eta.ml"))); - (* (fun _ -> ("Int", pau' ~verify:false (read_input "facehugger.ml"))); *) - (fun _ -> ("Int", pau' ~verify:false (read_input "fact.ml"))); - (fun _ -> ("false", pau' ~verify:false (read_input "kcfa2.ml"))); - (fun _ -> ("false", pau' ~verify:false (read_input "kcfa3.ml"))); - (* (fun _ -> ("Int", pau' ~verify:false (read_input "loop2.ml"))); *) - (* (fun _ -> - ( "(Int | (stub | (stub | (stub | (stub | stub)))))", - pau' ~verify:false (read_input "loop2'.ml") )); *) - (fun _ -> ("Int", pau' ~verify:false (read_input "mj09.ml"))); - (* (fun _ -> ("true", pau' ~verify:false (read_input "sat-3.ml"))); *) - (* (fun _ -> ("true", pau' ~verify:false (read_input "sat.ml"))); *) - (* (fun _ -> ("Int", pau' ~verify:false (read_input "tak.ml"))); *) - (* TODO: still have to keep mapping? *) - (* (fun _ -> - ( "{ hd = Int; tl = { hd = Int; tl = ({} | { hd = Int; tl = ({} | { hd = \ - Int; tl = stub }) }) } }", - pau' ~verify:false (read_input "map.ml") )); - (fun _ -> ("stub", pau' ~verify:false (read_input "primtest.ml"))); - (fun _ -> ("(false | true)", pau' ~verify:false (read_input "rsa.ml"))); *) - (* (fun _ -> ("", pau' ~verify:false (read_input "church.ml"))); *) - ] - -let test_lossy_core _ = gen_test lossy_core_thunked - let church_basic_thunked = [ (fun _ -> ("(0 + 1)", pau ~test_num:41 church_basic.(0))); @@ -171,6 +141,31 @@ let tests_thunked = @ conditional_thunked @ currying_thunked @ recursion_thunked @ church_basic_thunked @ church_binop_thunked @ lists_thunked +let test_prune_d _ = + let open Dinterp.Ast in + let open Dinterp.Interp in + let open Display_pa.Lib in + (* assert_equal ((0, DNil) => DNil) (prune_d ((0, DNil) => DNil)); + assert_equal + ((0, (1, DNil) => DNil) => DNil) + (prune_d ((0, (1, DNil) => DNil) => DNil)); + assert_equal + ((0, (1, DNil) => DNil) => DNil) + (prune_d ((0, (1, (2, DNil) => DNil) => DNil) => DNil)); + (* [ 0^[ 1^[ 2 ], 3^[ 3 ] ] ] -> [ 0^[ 1, 3^[ 3 ] ] ] *) + assert_equal + ((0, (1, DNil) => ((3, DNil) => DNil)) => DNil) + (prune_d ((0, (1, (2, DNil) => DNil) => ((3, DNil) => DNil)) => DNil)); + assert_equal true (matches_d ((0, DNil) => DNil) ((1, DNil) => DNil)); + assert_equal true + (matches_d ((0, DNil) => DNil) ((1, (2, DNil) => DNil) => DNil)); + assert_equal false + (matches_d ((1, (2, DNil) => DNil) => DNil) ((0, DNil) => DNil)); *) + assert_equal + ~printer:(Format.asprintf "%a" Dinterp.Pp.pp_d) + ((0, (1, DNil) => ((3, DNil) => DNil)) => DNil) + (prune_d ((0, DNil) => ((1, DNil) => ((2, DNil) => ((3, DNil) => DNil))))) + let ddpa_display_thunked = [ (* (fun _ -> ("true", pau'' (read_input "blur.ml"))); *) @@ -200,72 +195,102 @@ let test_ddpa_display _ = gen_test ddpa_display_thunked let ddpa_thunked = [ - (* (fun _ -> ("true", pau ~verify:false ~test_num:1 (read_input "blur.ml"))); *) - (* (fun _ -> ("false", pau ~verify:false ~test_num:1 (read_input "eta.ml"))); *) + (fun _ -> + ("true", pau ~verify:false ~test_name:"blur" (read_input "blur.ml"))); + (fun _ -> + ("false", pau ~verify:false ~test_name:"eta" (read_input "eta.ml"))); + (fun _ -> + ( "((6 * 1) + (12 * ((((3 | (stub - 1)) - 1) * ((((3 | (stub - 1)) - 1) \ + * stub) | 1)) | 1)))", + pau ~verify:false ~test_name:"facehugger" (read_input "facehugger.ml") + )); + (fun _ -> + ( "(90 * ((((9 | (stub - 1)) - 1) * ((((9 | (stub - 1)) - 1) * stub) | \ + 1)) | 1))", + pau ~verify:false ~test_name:"fact" (read_input "fact.ml") )); + (fun _ -> + ("false", pau ~verify:false ~test_name:"kcfa2" (read_input "kcfa2.ml"))); + (fun _ -> + ("false", pau ~verify:false ~test_name:"kcfa3" (read_input "kcfa3.ml"))); + (fun _ -> + ( read_output "loop2-1.txt", + pau ~verify:false ~test_name:"loop2-1" (read_input "loop2-1.ml") )); (* (fun _ -> - ( "((6 * 1) + (12 * ((((3 | (stub - 1)) - 1) * ((((3 | (stub - 1)) - 1) \ - * stub) | 1)) | 1)))", - pau ~verify:false ~test_num:1 (read_input "facehugger.ml") )); *) + ( "((stub | ((stub | stub) | stub)) | ((stub | stub) | stub))", + pau ~verify:false ~test_name:"loop2'" (read_input "loop2'.ml") )); *) + (fun _ -> ("2", pau ~verify:false ~test_name:"mj09" (read_input "mj09.ml"))); + (fun _ -> + ( "{ hd = 8; tl = { hd = 9; tl = ({} | { hd = (9 | 10); tl = ({} | { hd \ + = (9 | 10); tl = stub }) }) } }", + pau ~verify:false ~test_name:"map" (read_input "map.ml") )); + (fun _ -> + ("15", pau ~verify:false ~test_name:"primtest" (read_input "primtest.ml"))); + (fun _ -> + ( "(false | true)", + pau ~verify:false ~test_name:"sat-1" (read_input "sat-1.ml") )); + (fun _ -> + ( "(false | true)", + pau ~verify:false ~test_name:"sat-2" (read_input "sat-2.ml") )); + (fun _ -> + ( "(false | true)", + pau ~verify:false ~test_name:"sat-3" (read_input "sat-3.ml") )); + (fun _ -> + ("false", pau ~verify:false ~test_name:"rsa" (read_input "rsa.ml"))); + (* (fun _ -> ("Int", pau ~verify:false ~test_name:"ack" (read_input "ack.ml"))); + (fun _ -> ("Int", pau ~verify:false ~test_name:"tak" (read_input "tak.ml"))); + (fun _ -> + ("", pau ~verify:false ~test_name:"church" (read_input "church.ml"))); + (fun _ -> + ("", pau ~verify:false ~test_name:"cpstak" (read_input "cpstak.ml"))); *) + ] + +let test_ddpa _ = gen_test ddpa_thunked + +let ddpa_simple_thunked = + [ (* (fun _ -> - ( "(90 * ((((9 | (stub - 1)) - 1) * ((((9 | (stub - 1)) - 1) * stub) | \ - 1)) | 1))", - pau ~verify:false ~test_num:1 (read_input "fact.ml") )); *) - (* (fun _ -> ("false", pau ~verify:false ~test_num:1 (read_input "kcfa2.ml"))); *) - (* (fun _ -> ("false", pau ~verify:false ~test_num:1 (read_input "kcfa3.ml"))); *) + ( "(false | true)", + pau' ~verify:false ~test_name:"blur" (read_input "blur.ml") )); *) (* (fun _ -> - ( read_output "loop2-1.txt", - pau ~verify:false ~test_num:1 (read_input "loop2-1.ml") )); *) + ("false", pau' ~verify:false ~test_name:"eta" (read_input "eta.ml"))); *) (* (fun _ -> - ( "((stub | ((stub | stub) | stub)) | ((stub | stub) | stub))", - pau ~verify:false ~test_num:1 (read_input "loop2'.ml") )); *) - (* (fun _ -> ("2", pau ~verify:false ~test_num:1 (read_input "mj09.ml"))); *) + ( "Int", + pau' ~verify:false ~test_name:"facehugger" (read_input "facehugger.ml") + )); *) (* (fun _ -> - ( "{ hd = 8; tl = { hd = 9; tl = ({} | { hd = (9 | 10); tl = ({} | { hd \ - = (9 | 10); tl = stub }) }) } }", - pau ~verify:false ~test_num:1 (read_input "map.ml") )); *) - (* (fun _ -> ("15", pau ~verify:false ~test_num:1 (read_input "primtest.ml"))); *) + ("false", pau' ~verify:false ~test_name:"kcfa2" (read_input "kcfa2.ml"))); *) (* (fun _ -> - ( read_output "sat-1.txt", - pau ~verify:false ~test_num:1 (read_input "sat-1.ml") )); *) + ("false", pau' ~verify:false ~test_name:"kcfa3" (read_input "kcfa3.ml"))); *) (fun _ -> - ( read_output "sat-2.txt", - pau ~verify:false ~test_num:1 (read_input "sat-2.ml") )); + ( "(Int | (stub | (stub | (stub | (stub | stub)))))", + pau' ~verify:false ~test_name:"loop2-1" (read_input "loop2-1.ml") )); + (* (fun _ -> + ("Int", pau' ~verify:false ~test_name:"mj09" (read_input "mj09.ml"))); *) + (* (fun _ -> + ( "{ hd = Int; tl = { hd = Int; tl = ({} | { hd = Int; tl = ({} | { hd = \ + Int; tl = stub }) }) } }", + pau' ~verify:false ~test_name:"map" (read_input "map.ml") )); *) (* (fun _ -> - ( read_output "sat-3.txt", - pau ~verify:false ~test_num:1 (read_input "sat-3.ml") )); *) - (* (fun _ -> ("false", pau ~verify:false ~test_num:1 (read_input "rsa.ml"))); *) - (* (fun _ -> ("Int", pau ~verify:false ~test_num:1 (read_input "ack.ml"))); *) - (* (fun _ -> ("Int", pau ~verify:false ~test_num:1 (read_input "tak.ml"))); *) - (* (fun _ -> ("", pau ~verify:false ~test_num:1 (read_input "church.ml"))); *) - (* (fun _ -> ("", pau ~verify:false ~test_num:1 (read_input "cpstak.ml"))); *) + ( "stub", + pau' ~verify:false ~test_name:"primtest" (read_input "primtest.ml") )); *) + (* (fun _ -> + ("true", pau' ~verify:false ~test_name:"sat-1" (read_input "sat-1.ml"))); *) + (* (fun _ -> + ("true", pau' ~verify:false ~test_name:"sat-2" (read_input "sat-2.ml"))); *) + (* (fun _ -> + ("true", pau' ~verify:false ~test_name:"sat-3" (read_input "sat-3.ml"))); *) + (* (fun _ -> + ( "(false | true)", + pau' ~verify:false ~test_name:"rsa" (read_input "rsa.ml") )); *) + (* (fun _ -> + ("Int", pau' ~verify:false ~test_name:"ack" (read_input "ack.ml"))); *) + (* (fun _ -> + ("Int", pau' ~verify:false ~test_name:"tak" (read_input "tak.ml"))); *) + (* (fun _ -> + ("", pau' ~verify:false ~test_name:"cpstak" (read_input "cpstak.ml"))); *) ] -let test_ddpa _ = gen_test ddpa_thunked - -let test_prune_d _ = - let open Dinterp.Ast in - let open Dinterp.Interp in - let open Display_pa.Lib in - (* assert_equal ((0, DNil) => DNil) (prune_d ((0, DNil) => DNil)); - assert_equal - ((0, (1, DNil) => DNil) => DNil) - (prune_d ((0, (1, DNil) => DNil) => DNil)); - assert_equal - ((0, (1, DNil) => DNil) => DNil) - (prune_d ((0, (1, (2, DNil) => DNil) => DNil) => DNil)); - (* [ 0^[ 1^[ 2 ], 3^[ 3 ] ] ] -> [ 0^[ 1, 3^[ 3 ] ] ] *) - assert_equal - ((0, (1, DNil) => ((3, DNil) => DNil)) => DNil) - (prune_d ((0, (1, (2, DNil) => DNil) => ((3, DNil) => DNil)) => DNil)); - assert_equal true (matches_d ((0, DNil) => DNil) ((1, DNil) => DNil)); - assert_equal true - (matches_d ((0, DNil) => DNil) ((1, (2, DNil) => DNil) => DNil)); - assert_equal false - (matches_d ((1, (2, DNil) => DNil) => DNil) ((0, DNil) => DNil)); *) - assert_equal - ~printer:(Format.asprintf "%a" Dinterp.Pp.pp_d) - ((0, (1, DNil) => ((3, DNil) => DNil)) => DNil) - (prune_d ((0, DNil) => ((1, DNil) => ((2, DNil) => ((3, DNil) => DNil))))) +let test_ddpa_simple _ = gen_test ddpa_simple_thunked let test_pa = [ @@ -279,12 +304,12 @@ let test_pa = (* "Church numerals binary operations" >:: test_church_binop; *) (* "Adapted" >:: test_adapted; *) (* "Lists" >:: test_lists; *) - (* "Core (simple)" >:: test_lossy_core; *) - (* "Core (display)" >:: test_lossy_core'; *) (* "pruned_d" >:: test_prune_d; *) - "DDPA (display)" - >: test_case test_ddpa_display ~length:(OUnitTest.Custom_length 100000.); + "DDPA (simple)" + >: test_case test_ddpa_simple ~length:(OUnitTest.Custom_length 100000.); (* "DDPA" >: test_case test_ddpa ~length:(OUnitTest.Custom_length 100000.); *) + (* "DDPA (display)" + >: test_case test_ddpa_display ~length:(OUnitTest.Custom_length 100000.); *) ] let tests = "Program analysis tests" >::: test_pa diff --git a/program_analysis/tests/utils.ml b/program_analysis/tests/utils.ml index de1d971..e770969 100644 --- a/program_analysis/tests/utils.ml +++ b/program_analysis/tests/utils.ml @@ -1,12 +1,10 @@ -open Interpreter -open Program_analysis +open Interp +open Pa open Solver open Test_cases exception Unreachable -let pf = Format.printf - (** PBT *) module IdentSet = Set.Make (struct @@ -29,15 +27,28 @@ let ( |>-> ) v f = Option.bind v f (** General *) -(*? can't use Debugutils.parse_analyze *) -let pau ?(verify = true) ?(test_num = 0) s = +let pau ?(verify = true) ?(test_num = 0) + ?(test_name = Format.sprintf "Test %d" test_num) ?(time = true) s = s |> Core.Fn.flip ( ^ ) ";;" |> Lexing.from_string |> Parser.main Lexer.token - |> Lib.analyze ~verify ~test_num - |> Format.asprintf "%a" Utils.pp_res - -let pau' ?(verify = true) ?(test_num = 0) s = + |> fun e -> + let before = Sys.time () in + let r = Lib.analyze e ~verify ~test_num in + let after = Sys.time () in + if time then ( + Format.printf "%s: %f\n" test_name (after -. before); + flush_all ()); + r |> Format.asprintf "%a" Utils.pp_res + +let pau' ?(verify = true) ?(test_num = 0) + ?(test_name = Format.sprintf "Test %d" test_num) ?(time = true) s = s |> Core.Fn.flip ( ^ ) ";;" |> Lexing.from_string |> Parser.main Lexer.token - |> Pa_reworked.Lib.analyze ~verify ~test_num - |> Format.asprintf "%a" Pa_reworked.Utils.pp_res + |> fun e -> + let before = Sys.time () in + let r = Simple_pa.Lib.analyze e ~verify ~test_num in + let after = Sys.time () in + if time then ( + Format.printf "%s: %f\n" test_name (after -. before); + flush_all ()); + r |> Format.asprintf "%a" Simple_pa.Utils.pp_res let pau'' = Display_pa.Debugutils.pau