From 8effc338b4c65f4cc745b499245ad02be4554098 Mon Sep 17 00:00:00 2001 From: Robert Zhang Date: Fri, 1 Dec 2023 11:46:59 -0500 Subject: [PATCH] [PA] Monadic rewrite of simplified program analysis --- program_analysis/simple/debugutils.ml | 4 +- program_analysis/simple/grammar.ml | 151 ++-- program_analysis/simple/lib.ml | 929 ++++++++++++---------- program_analysis/simple/simplifier.ml | 63 +- program_analysis/simple/utils.ml | 14 +- program_analysis/src/grammar.ml | 37 +- program_analysis/src/lib.ml | 678 ++++++++-------- program_analysis/src/logging.ml | 2 +- program_analysis/src/utils.ml | 4 +- program_analysis/tests/inputs/blur.ml | 3 +- program_analysis/tests/inputs/kcfa2.ml | 4 +- program_analysis/tests/inputs/mack.ml | 5 + program_analysis/tests/inputs/map.ml | 3 +- program_analysis/tests/inputs/not.ml | 0 program_analysis/tests/inputs/primtest.ml | 3 +- program_analysis/tests/inputs/sat-2.ml | 6 +- program_analysis/tests/inputs/sat-3.ml | 8 +- program_analysis/tests/tests.ml | 160 ++-- program_analysis/tests/utils.ml | 2 +- 19 files changed, 1127 insertions(+), 949 deletions(-) create mode 100644 program_analysis/tests/inputs/mack.ml create mode 100644 program_analysis/tests/inputs/not.ml diff --git a/program_analysis/simple/debugutils.ml b/program_analysis/simple/debugutils.ml index 0c57011..bd20f21 100644 --- a/program_analysis/simple/debugutils.ml +++ b/program_analysis/simple/debugutils.ml @@ -11,10 +11,10 @@ let parse s = Interp.Ast.reset_label (); e -let unparse = Format.asprintf "%a" pp_res +let unparse r = Format.asprintf "%a" pp_res (Core.Set.elements r) let parse_analyze s = s |> parse |> analyze ~debug_mode:!is_debug_mode let parse_analyze_unparse s = s |> parse_analyze |> unparse let pau = parse_analyze_unparse let parse_analyze_print s = - s |> parse_analyze |> Format.printf "==> %a\n" pp_res + s |> parse_analyze |> Core.Set.elements |> Format.printf "==> %a\n" pp_res diff --git a/program_analysis/simple/grammar.ml b/program_analysis/simple/grammar.ml index ad41c60..201e19e 100644 --- a/program_analysis/simple/grammar.ml +++ b/program_analysis/simple/grammar.ml @@ -1,7 +1,7 @@ open Core open Interp.Ast -module SKey = struct +module S_key = struct module T = struct type t = sigma [@@deriving compare, sexp, show { with_path = false }, hash] end @@ -26,38 +26,29 @@ module St = struct include Comparable.Make (T) end -module NewSt = struct +module V_key = struct module T = struct - type lstate = - int - * sigma - * ((SKey.t, (SKey.comparator_witness[@compare.ignore])) Set.t - [@sexp.opaque] [@show.opaque] [@hash.ignore]) - [@@deriving compare, sexp, hash] - - let show_set s = - s |> Set.to_list |> List.map ~f:show_sigma |> String.concat ~sep:", " + type lstate = int * sigma * int [@@deriving compare, sexp, hash] let show_lstate (l, sigma, s) = - Format.sprintf "(%d, %s, {%s})" l (show_sigma sigma) (show_set s) + Format.sprintf "(%d, %s, %d)" l (S_key.show sigma) s let pp_lstate fmt lst = Format.fprintf fmt "%s" (show_lstate lst) - type estate = - expr - * sigma - * ((SKey.t, (SKey.comparator_witness[@compare.ignore])) Set.t - [@sexp.opaque] [@show.opaque] [@hash.ignore]) - [@@deriving compare, sexp, hash] + type estate = expr * sigma * int [@@deriving compare, sexp, hash] let show_estate (e, sigma, s) = - Format.asprintf "(%a, %s, {%s})" Interp.Ast.pp_expr e (show_sigma sigma) - (show_set s) + Format.asprintf "(%a, %s, %d)" Interp.Ast.pp_expr e (S_key.show sigma) s let pp_estate fmt est = Format.fprintf fmt "%s" (show_estate est) type t = Lstate of lstate | Estate of estate - [@@deriving compare, sexp, show { with_path = false }, hash] + [@@deriving compare, sexp, hash] + + let show (k : t) = + match k with + | Lstate st -> Format.asprintf "%a" pp_lstate st + | Estate st -> Format.asprintf "%a" pp_estate st end include T @@ -67,80 +58,106 @@ end module Cache_key = struct module T = struct (* type t = expr * sigma [@@deriving hash, sexp, compare] *) - type t = - expr - * sigma - * ((NewSt.t, (NewSt.comparator_witness[@compare.ignore])) Set.t - [@sexp.opaque]) - [@@deriving compare, sexp] - - let hash = Hashtbl.hash + type t = expr * sigma * int * int [@@deriving compare, sexp, hash] + (* [@@deriving_inline hash] *) + + (* [@@@end] *) + + (* let hash = Hashtbl.hash *) end include T include Comparable.Make (T) end -open Core -open Interp.Ast +module V = struct + module T = struct + type t = Set.M(V_key).t [@@deriving compare, sexp] + + let show (v : t) = + v |> Set.to_list |> List.map ~f:V_key.show |> String.concat ~sep:", " + |> Format.sprintf "{%s}" + end -type atom = - | IntAnyAtom - | IntAtom of int - | BoolAtom of bool - | FunAtom of expr * int * sigma - | 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 }] - -type pi = (atom list * bool) option -[@@deriving hash, sexp, compare, show { with_path = false }] - -module Let_syntax = struct - let return r = (r, Set.empty (module SKey)) - - let bind (r, s) ~f = - let r', s' = f (r, s) in - (r', Set.union s s') - - let map (r, s) ~f = return (f (r, s)) - let ( >>= ) t f = bind t ~f - let ( >>| ) t f = map t ~f + include T + include Comparable.Make (T) end -(* used to accumulate disjuncts when stitching stacks *) -module Choice = struct +module S = struct module T = struct - type t = atom [@@deriving compare, sexp] + type t = Set.M(S_key).t [@@deriving compare, sexp] + + let show (s : t) = + s |> Set.to_list |> List.map ~f:S_key.show |> String.concat ~sep:", " + |> Format.sprintf "{%s}" end include T include Comparable.Make (T) end -module AtomKey = struct +module Freq_key = struct module T = struct - type t = atom [@@deriving hash, sexp, compare] + type t = expr * sigma * int * int [@@deriving compare, sexp] end include T include Comparable.Make (T) end -module ResKey = struct +open Core +open Interp.Ast + +module rec Atom : sig + type t = + | IntAnyAtom + | IntAtom of int + | BoolAtom of bool + | FunAtom of expr * int * sigma + | LStubAtom of (int * sigma) + | EStubAtom of (expr * sigma) + | RecAtom of (ident * Res.t) list + | ProjAtom of Res.t * ident + | InspAtom of ident * Res.t + | AssertAtom of ident * Res.t * res_val_fv + [@@deriving compare, sexp] +end = struct + type t = + | IntAnyAtom + | IntAtom of int + | BoolAtom of bool + | FunAtom of expr * int * sigma + | LStubAtom of (int * sigma) + | EStubAtom of (expr * sigma) + | RecAtom of (ident * Res.t) list + | ProjAtom of Res.t * ident + | InspAtom of ident * Res.t + | AssertAtom of ident * Res.t * res_val_fv + [@@deriving compare, sexp] +end + +and Res_key : sig + type t = Atom.t [@@deriving compare, sexp] + type comparator_witness + + val comparator : (t, comparator_witness) Comparator.t +end = struct module T = struct - type t = res [@@deriving hash, sexp, compare] + type t = Atom.t [@@deriving compare, sexp] end include T include Comparable.Make (T) end +and Res : sig + type t = Set.M(Res_key).t [@@deriving compare, sexp] +end = struct + type t = Set.M(Res_key).t [@@deriving compare, sexp] +end + +type pi = (Res.t * bool) option [@@deriving compare] + module Z3ExprKey = struct module T = struct open Z3 @@ -157,4 +174,6 @@ module Z3ExprKey = struct include Comparable.Make (T) end -let choice_empty = Set.empty (module Choice) +let empty_res = Set.empty (module Res_key) +let single_res = Set.singleton (module Res_key) +let unwrap_res = Set.elements diff --git a/program_analysis/simple/lib.ml b/program_analysis/simple/lib.ml index c83de17..e0b3a4e 100644 --- a/program_analysis/simple/lib.ml +++ b/program_analysis/simple/lib.ml @@ -1,6 +1,5 @@ open Core open Logs -open Option.Let_syntax open Interp.Ast open Pa.Exns open Pa.Logging @@ -92,445 +91,530 @@ let eval_assert e 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 log_v_set = Set.iter ~f:(fun st -> debug (fun m -> m "%s" (V_key.show st))) let fold_res_app ~init ~f l sigma d = - List.fold ~init ~f:(fun ((acc_r, acc_s) as acc) a -> + Set.fold ~init ~f:(fun 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)) + match a with FunAtom (Function (_, e1, _), _, _) -> f acc e1 | _ -> acc) 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)); + Set.fold r ~init ~f:(fun acc a -> + debug (fun m -> m "r1 length: %d" (Set.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)) + | _ -> acc) 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 -> + Set.fold r ~init:empty_res ~f:(fun acc 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) + | RecAtom _ when not (exists_stub (single_res a) label) -> + Set.add acc a + | ProjAtom (r, Ident key) when not (exists_stub r label) -> ( + match unwrap_res r with + | [ RecAtom rs ] -> ( + match + List.find rs ~f:(fun (Ident key', _) -> String.(key = key')) + with + | Some (_, r') when Set.length r' = 1 -> + Set.add acc (r' |> unwrap_res |> List.hd_exn) + | _ -> raise Runtime_error) + | _ -> acc) + | FunAtom _ -> Set.add acc a + | _ -> acc) 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 ]) + Set.fold r ~init:empty_res ~f:(fun acc a -> + match a with + | ProjAtom (r, Ident key) -> ( + match unwrap_res r with + | [ EStubAtom st ] when St.(label = Estate st) -> + Set.fold bases ~init:empty_res ~f:(fun acc -> function + | RecAtom es -> ( + match + List.find es ~f:(fun (Ident key', _) -> + String.(key = key')) + with + | Some (_, r) -> Set.union acc r + | None -> + acc + (* Format.printf "base: %a\n" pp_atom base; + raise Runtime_error *)) + | _ -> raise Runtime_error) + | _ -> Set.add acc a) + (* (fun x -> x) | stub *) + | EStubAtom st when St.(label = Estate st) -> acc + | _ -> Set.add acc 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' = +module With_state = struct + module T = struct + type cache = Res.t Map.M(Cache_key).t + type vids = int Map.M(V).t + type sids = int Map.M(S).t + type freqs = int64 Map.M(Freq_key).t + + type state = { + s : S.t; + v : V.t; + c : cache; + freqs : freqs; + sids : sids; + vids : vids; + cnt : int; + } + + type 'a t = state -> 'a * state + + let return (a : 'a) : 'a t = fun st -> (a, st) + + let bind (m : 'a t) ~(f : 'a -> 'b t) : 'b t = + fun st -> + let a, ({ s; v; sids; vids; cnt; _ } as st') = m st in + let sids', cnt' = + if Map.mem sids s then (sids, cnt) + else (Map.add_exn sids ~key:s ~data:cnt, cnt + 1) + in + let vids', cnt' = + if Map.mem vids v then (vids, cnt') + else (Map.add_exn vids ~key:v ~data:cnt', cnt' + 1) + in + f a { st' with sids = sids'; vids = vids'; cnt = cnt' } + + let map = `Define_using_bind + let get () : state t = fun st -> (st, st) + + let get_cnt () : int t = + fun ({ cnt; _ } as st) -> (cnt, { st with cnt = cnt + 1 }) + + let get_vid v : int t = fun ({ vids; _ } as st) -> (Map.find_exn vids v, st) + let get_sid s : int t = fun ({ sids; _ } as st) -> (Map.find_exn sids s, st) + let set_s s : unit t = fun st -> ((), { st with s }) + let set_v v : unit t = fun st -> ((), { st with v }) + let set_cache c : unit t = fun st -> ((), { st with c }) + let set_vids vids : unit t = fun st -> ((), { st with vids }) + let set_sids sids : unit t = fun st -> ((), { st with sids }) + let set_freqs freqs : unit t = fun st -> ((), { st with freqs }) + + let inc_freq freq_key : unit t = + fun ({ freqs; _ } as st) -> + let freqs' = + match Map.find freqs freq_key with + | None -> Map.add_exn freqs ~key:freq_key ~data:1L + | Some freq -> + Map.add_exn + (Map.remove freqs freq_key) + ~key:freq_key + ~data:Int64.(freq + 1L) + in + ((), { st with freqs = freqs' }) + end + + include T + include Monad.Make (T) +end + +open With_state +open With_state.Let_syntax + +let cache key data = + let%bind { c; _ } = get () in + let%bind () = set_cache (Map.add_exn (Map.remove c key) ~key ~data) in + return data + +let print_freqs ?(sort = true) freqs = + freqs |> Map.to_alist |> fun freqs -> + (if not sort then freqs + else + List.sort freqs ~compare:(fun (_, freq1) (_, freq2) -> + Int64.descending freq1 freq2)) + |> List.iter ~f:(fun ((e, sigma, vid, sid), freq) -> + Format.printf "(%a, %a, %d, %d) -> %Ld\n" Interp.Pp.pp_expr e pp_sigma + sigma vid sid freq) + +let print_vids ?(size = false) ?(sort = false) vids = + vids |> Map.to_alist |> fun vids -> + (if not sort then vids + else + List.sort vids ~compare:(fun (_, id1) (_, id2) -> Int.descending id1 id2)) + |> List.iter ~f:(fun (key, data) -> + if size then Format.printf "%d -> %d\n" (Set.length key) data + else Format.printf "%s -> %d\n" (V.show key) data) + +let print_sids ?(size = false) = + Map.iteri ~f:(fun ~key ~data -> + if size then Format.printf "%d -> %d\n" (Set.length key) data + else Format.printf "%s -> %d\n" (S.show key) data) + +let start_time = ref (Stdlib.Sys.time ()) + +let rec analyze_aux ?(tmp = false) d expr sigma pi : Res.t T.t = + let%bind { c; s; v; sids; vids; freqs; _ } = get () in + (* if Float.(Stdlib.Sys.time () - !start_time > 120.) then ( + print_freqs freqs ~sort:true; + Format.printf "vids:\n"; + print_vids vids ~size:true ~sort:true; + Format.printf "sids:\n"; + print_sids sids; + failwith "timed out"); *) + (* Logs.debug (fun m -> m "Level %d" d); *) + (* Logs.debug (fun m -> m "S length: %d" (Set.length s)); *) + (* if d >= 100 then gen_logs := true; *) + (* if Set.length s >= 23 then gen_logs := true; *) 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 + (* Logs.debug (fun m -> m "max d: %d" !max_d); *) + let%bind vid = get_vid v in + let%bind sid = get_sid s in + let%bind () = inc_freq (expr, sigma, vid, sid) in + (* let%bind freqs = get_freqs () in + let%bind () = set_freqs (Map.add_exn ()) *) + let cache_key = (expr, sigma, vid, sid) in + match Map.find c cache_key with + | Some r -> + debug (fun m -> m "Cache hit"); + return r + | None -> + (* debug (fun m -> m "S size: %d" (Set.length s)); *) + let d = d + 1 in + let%bind r = + match expr with + | Int i -> return (single_res IntAnyAtom) + | Bool b -> return (single_res (BoolAtom b)) + | Function (_, _, l) -> return (single_res (FunAtom (expr, l, sigma))) + | Appl (e, _, l) -> + info (fun m -> + m "[Level %d] === Appl (%a) ====" d Interp.Pp.pp_expr expr); + (* debug (fun m -> m "%a" Interp.Ast.pp_expr expr); *) + let cycle_label = (l, sigma) in + (* let st = (l, pruned_sigma', s) in *) + let lst = V_key.Lstate (l, sigma, sid) 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"; + info (fun m -> + m "[Level %d] *** Appl (%a) ****" d Interp.Pp.pp_expr expr); + return (single_res (LStubAtom cycle_label))) + else ( + (* Application *) + debug_plain "Didn't stub"; + debug (fun m -> m "sigma: %s" (show_sigma sigma)); + let sigma' = l :: sigma in + let pruned_sigma' = prune_sigma sigma' in + debug (fun m -> m "sigma_pruned': %s" (show_sigma pruned_sigma')); + 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%bind () = set_v (Set.add v lst) in + let%bind r1 = analyze_aux d e sigma pi in + debug (fun m -> m "r1 length: %d" (Set.length r1)); + let%bind { s = s1; _ } = get () in + let%bind () = set_s (Set.add s1 pruned_sigma') in + let%bind r2 = + fold_res_app ~init:(return empty_res) l sigma d r1 + ~f:(fun acc e1 -> + let%bind acc = acc in + debug (fun m -> + m "[Appl] Evaluating body of function being applied: %a" + Interp.Pp.pp_expr e1); + analyze_aux d e1 pruned_sigma' pi) + in + let r2 = elim_stub r2 (St.Lstate cycle_label) in + debug (fun m -> m "r2: %a" pp_res (unwrap_res r2)); + info (fun m -> + m "[Level %d] *** Appl (%a) ****" d Interp.Pp.pp_expr expr); + return r2) + | Var (Ident x, l) -> + info (fun m -> m "[Level %d] === Var (%s, %d) ====" d x l); + let cycle_label = (expr, sigma) in + let est = V_key.Estate (expr, sigma, sid) in + let%bind () = set_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); + return (single_res (EStubAtom cycle_label))) + 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); - 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 + 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%bind r1 = + debug_plain "Begin stitching stacks"; + debug_plain "S set:"; + debug (fun m -> m "%s" (S.show 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:(return empty_res) + ~f:(fun acc sigma_i -> + let%bind acc' = acc in + 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 *) + analyze_aux d e2 sigma_i_tl pi) + else acc) + 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 = elim_stub r1 (St.Estate cycle_label) in + debug (fun m -> m "r1: %a" pp_res (unwrap_res r1)); + return r1 + | _ -> raise Unreachable [@coverage off]) + else ( + (* Var Non-Local *) 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' + 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 "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 est = V_key.Estate (e1, sigma, sid) in + if Set.mem v est && not tmp then ( + debug_plain "Stubbed e1"; + return (single_res @@ EStubAtom (e1, sigma))) + else + let sigma_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)); *) + (* let new_v = Set.add new_v est in *) + (* enumerate all matching stacks in the set *) + debug (fun m -> m "S size: %d" (Set.length s)); + let%bind r1 = + Set.fold s ~init:(return empty_res) + ~f:(fun acc sigma_i -> + let%bind acc' = acc in + let sigma_i_hd, sigma_i_tl = + (List.hd_exn sigma_i, List.tl_exn sigma_i) + in + (* stitch the stack to gain more precision *) + if + sigma_i_hd = l2 + && starts_with sigma_i_tl sigma_tl + then ( + debug (fun m -> + m + "[Level %d] Stitched! Evaluating \ + function being applied at front of \ + sigma, using stitched stack %s" + d (show_sigma sigma_i_tl)); + analyze_aux ~tmp:true d e1 sigma_i_tl pi) + else acc) + in + debug_plain + "Found all stitched stacks and evaluated e1, begin \ + relabeling variables"; + let%bind r2 = + fold_res_var ~init:(return empty_res) expr sigma d + r1 ~f:(fun acc x1' l1 sigma1 -> + let%bind acc' = acc in + if Stdlib.(x1 = x1') && l_myfun = l1 then ( + debug (fun m -> + m + "[Var Non-Local] Relabel %s with label \ + %d and evaluate" + x l1); + analyze_aux d (Var (Ident x, l1)) sigma1 pi) + else acc) + 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 = elim_stub r2 (St.Estate cycle_label) in + debug (fun m -> m "r2: %a" pp_res (unwrap_res r2)); + return r2 + | _ -> raise Unreachable [@coverage off]) + | _ -> raise Unreachable [@coverage off]) + | If (e, e_true, e_false, l) -> ( + debug (fun m -> m "[Level %d] === If ===" d); + let%bind r_cond = analyze_aux d e sigma None in + match unwrap_res r_cond with + | [ BoolAtom b ] -> + debug (fun m -> m "[Level %d] === If %b ===" d b); + if b then ( + let%bind r_true = analyze_aux d e_true sigma None in + debug (fun m -> m "[Level %d] *** If %b ***" d b); + return r_true) + else + let%bind r_false = analyze_aux d e_false sigma None in + debug (fun m -> m "[Level %d] *** If %b ***" d b); + return r_false + | _ -> + debug (fun m -> m "[Level %d] === If Both ===" d); + (* Format.printf "r_cond: %a\n" pp_res r_cond; *) + let%bind r_true = analyze_aux d e_true sigma None in + info (fun m -> m "Evaluating: %a" Interp.Pp.pp_expr e_false); + let%bind r_false = analyze_aux d e_false sigma None in + debug (fun m -> m "[Level %d] *** If Both ***" d); + return (Set.union r_true r_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) -> + 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%bind r1 = analyze_aux d e1 sigma pi in + let%bind r2 = analyze_aux d e2 sigma pi in + debug (fun m -> + m "[Level %d] Evaluated binop to (%a %a)" d Utils.pp_res + (unwrap_res r1) Utils.pp_res (unwrap_res r2)); + (* debug (fun m -> + m "[Level %d] Evaluated binop to (%a %a)" d Grammar.pp_res + (unwrap_res r1) Grammar.pp_res (unwrap_res r2)); *) + info (fun m -> + m "[Level %d] *** Binop (%a) ****" d Interp.Pp.pp_expr expr); + let bool_tf_res = + Set.of_list (module Res_key) [ BoolAtom true; BoolAtom false ] 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) ] + return + (match expr with + | Plus _ -> ( + match (unwrap_res r1, unwrap_res r2) with + | [ IntAtom i1 ], [ IntAtom i2 ] -> + single_res (IntAtom (i1 + i2)) + | _ -> single_res IntAnyAtom) + | Minus _ -> single_res IntAnyAtom + | Mult _ -> ( + match (unwrap_res r1, unwrap_res r2) with + | [ IntAtom i1 ], [ IntAtom i2 ] -> + single_res (IntAtom (i1 * i2)) + | r1', r2' -> single_res IntAnyAtom) + | And _ -> ( + match (unwrap_res r1, unwrap_res r2) with + | [ BoolAtom b1 ], [ BoolAtom b2 ] -> + single_res (BoolAtom (b1 && b2)) + | [ BoolAtom b11; BoolAtom b12 ], [ BoolAtom b2 ] -> + let b1 = b11 && b2 in + let b2 = b12 && b2 in + single_res (BoolAtom (b1 || b2)) + | [ BoolAtom b1 ], [ BoolAtom b21; BoolAtom b22 ] -> + let b1 = b1 && b21 in + let b2 = b1 && b22 in + single_res (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 + single_res (BoolAtom (b1 || b2)) + | _ -> bool_tf_res) + | Or _ -> ( + match (unwrap_res r1, unwrap_res r2) with + | [ BoolAtom b1 ], [ BoolAtom b2 ] -> + single_res (BoolAtom (b1 || b2)) + | [ BoolAtom b11; BoolAtom b12 ], [ BoolAtom b2 ] -> + let b1 = b11 || b2 in + let b2 = b12 || b2 in + single_res (BoolAtom (b1 || b2)) + | [ BoolAtom b1 ], [ BoolAtom b21; BoolAtom b22 ] -> + let b1 = b1 || b21 in + let b2 = b1 || b22 in + single_res (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 + single_res (BoolAtom (b1 || b2)) + | _ -> bool_tf_res) + | Equal _ | Ge _ | Gt _ | Le _ | Lt _ -> bool_tf_res | _ -> - (* 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 "%a\n" pp_expr expr; + raise Unreachable [@coverage off]) + | Not e -> + let%bind r = analyze_aux d e sigma pi in + return + (match unwrap_res r with + | [] -> empty_res + | [ BoolAtom b ] -> single_res (BoolAtom (not b)) | _ -> - (* 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 *) + Set.of_list (module Res_key) [ BoolAtom true; BoolAtom false ]) + | Record es -> + if List.is_empty es then return (single_res (RecAtom [])) + else + es + |> List.fold ~init:(return []) ~f:(fun acc (id, ei) -> + let%bind acc = acc in + let%bind p = analyze_aux d ei sigma pi in + return ((id, p) :: acc)) + |> fun rs -> + let%bind rs = rs in + return (single_res (RecAtom rs)) + | Projection (e, Ident key) -> + debug (fun m -> m "[Level %d] === Projection ===" d); + let%bind r0 = analyze_aux d e sigma pi in + return (single_res (ProjAtom (r0, Ident key))) + | Inspection (Ident key, e) -> + let%bind r0 = analyze_aux d e sigma pi in + return (single_res (InspAtom (Ident key, r0))) + | LetAssert (id, e1, e2) -> + let%bind r1 = analyze_aux d e1 sigma pi in + let r2 = eval_assert e2 id in + return (single_res (AssertAtom (id, r1, r2))) + | Let _ -> raise Unreachable [@coverage off] + in + cache cache_key (simplify r) let analyze ?(debug_mode = false) ?(verify = true) ?(test_num = 0) ?(should_cache = true) e = @@ -542,17 +626,30 @@ let analyze ?(debug_mode = false) ?(verify = true) ?(test_num = 0) 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)) + start_time := Stdlib.Sys.time (); + let r, { vids; sids; freqs; _ } = + analyze_aux 0 e [] None + { + s = Set.empty (module S_key); + v = Set.empty (module V_key); + c = Map.empty (module Cache_key); + vids = Map.empty (module V); + sids = Map.empty (module S); + cnt = 0; + freqs = Map.empty (module Freq_key); + } in + (* print_freqs freqs; + Format.printf "vids:\n"; + print_vids vids ~size:false; + Format.printf "sids:\n"; + print_sids sids ~size:false; *) + (* 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); + debug (fun m -> m "Result: %a" Utils.pp_res (unwrap_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"; diff --git a/program_analysis/simple/simplifier.ml b/program_analysis/simple/simplifier.ml index 87154ad..03621be 100644 --- a/program_analysis/simple/simplifier.ml +++ b/program_analysis/simple/simplifier.ml @@ -2,9 +2,10 @@ open Core open Interp.Ast open Pa.Exns open Grammar +open Grammar.Atom let rec exists_stub r label = - List.exists r ~f:(function + Set.exists r ~f:(function | FunAtom _ | IntAtom _ | IntAnyAtom | BoolAtom _ -> false | LStubAtom st -> St.(label = St.Lstate st) | EStubAtom st -> St.(label = St.Estate st) @@ -15,45 +16,37 @@ let rec exists_stub r label = let rec simplify ?(pa = None) r = let r' = - List.filter_map r ~f:(fun a -> + Set.fold r ~init:empty_res ~f:(fun acc a -> match a with | IntAtom _ | IntAnyAtom | BoolAtom _ | LStubAtom _ | EStubAtom _ | FunAtom _ -> - Some [ a ] + Set.add acc a | AssertAtom (id, r, rv) -> - Some [ AssertAtom (id, simplify r ~pa:(Some a), rv) ] + Set.add acc (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)))); - ] + Set.add acc + (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) ])) + Set.fold r ~init:acc ~f:(fun acc a -> + match a with + | RecAtom rs -> ( + match + List.find rs ~f:(fun (id', _) -> compare_ident id id' = 0) + with + | Some (_, r) -> Set.union acc r + | None -> acc) + | a -> + Set.add acc + (ProjAtom (Set.singleton (module Res_key) 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 ]) ]))) + Set.fold r ~init:acc ~f:(fun acc -> function + | RecAtom rs -> + Set.add acc + (BoolAtom + (List.exists rs ~f:(fun (id', _) -> + compare_ident id id' = 0))) + | a -> + Set.add acc (InspAtom (id, Set.singleton (module Res_key) a)))) in - let r' = List.concat r' in - if compare_res r r' = 0 then r' else simplify r' ~pa + if Res.compare r r' = 0 then r' else simplify r' ~pa diff --git a/program_analysis/simple/utils.ml b/program_analysis/simple/utils.ml index cd4f1ed..cbc89c7 100644 --- a/program_analysis/simple/utils.ml +++ b/program_analysis/simple/utils.ml @@ -1,6 +1,7 @@ open Core open Interp.Ast open Grammar +open Grammar.Atom let pf = Format.printf let pfl = pf "%s\n" @@ -66,15 +67,16 @@ let rec pp_atom fmt = function 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 + | ProjAtom (r, Ident s) -> ff fmt "(%a.%s)" pp_res (Set.elements r) s + | InspAtom (Ident s, r) -> ff fmt "(%s in %a)" s pp_res (Set.elements r) + | AssertAtom (_, r, _) -> ff fmt "%a" pp_res (Set.elements 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 + | [ (Ident x, v) ] -> Format.fprintf fmt "%s = %a" x pp_res (Set.elements v) + | (Ident x, r) :: rest -> + Format.fprintf fmt "%s = %a; %a" x pp_res (Set.elements r) pp_record_atom + rest and pp_res fmt = function | [] -> () diff --git a/program_analysis/src/grammar.ml b/program_analysis/src/grammar.ml index 37041c2..3d08f0a 100644 --- a/program_analysis/src/grammar.ml +++ b/program_analysis/src/grammar.ml @@ -65,23 +65,6 @@ module NewSt = struct include Comparable.Make (T) end -module Cache_key = struct - module T = struct - (* type t = expr * sigma [@@deriving hash, sexp, compare] *) - type t = - expr - * sigma - * ((NewSt.t, (NewSt.comparator_witness[@compare.ignore])) Set.t - [@sexp.opaque]) - [@@deriving compare, sexp] - - let hash = Hashtbl.hash - end - - include T - include Comparable.Make (T) -end - type atom = | IntAtom of int | BoolAtom of bool @@ -115,6 +98,26 @@ and path_cond = res * bool type pi = (atom list * bool) option [@@deriving hash, sexp, compare, show { with_path = false }] +module Cache_key = struct + module T = struct + (* type t = expr * sigma [@@deriving hash, sexp, compare] *) + type t = + expr + * sigma + * ((NewSt.t, (NewSt.comparator_witness[@compare.ignore])) Set.t + [@sexp.opaque]) + * ((S_key.t, (S_key.comparator_witness[@compare.ignore])) Set.t + [@sexp.opaque]) + * pi + [@@deriving compare, sexp] + + let hash = Hashtbl.hash + end + + include T + include Comparable.Make (T) +end + module Let_syntax = struct let return r = (r, Set.empty (module S_key)) diff --git a/program_analysis/src/lib.ml b/program_analysis/src/lib.ml index 3a4387a..f573357 100644 --- a/program_analysis/src/lib.ml +++ b/program_analysis/src/lib.ml @@ -208,340 +208,359 @@ let elim_stub r label = r' else r -(* let cache = Hashtbl.create (module Cache_key) *) +let cache = Hashtbl.create (module Cache_key) let rec analyze_aux_step d expr sigma pi s v = + (* Logs.debug (fun m -> m "S size: %d" (Set.length s)); *) (* TODO: prepass to do record simplifications *) - (* let cache_key = (expr, sigma, v) in - let found = Hashtbl.find cache cache_key in - match found with - | Some r when not (exists_lone_stub v (Set.empty (module St)) r) -> - debug (fun m -> m "cache hit: %a" pp_res r); - (* debug (fun m -> m "cache hit: %a" Grammar.pp_res r); *) - (r, s) - | _ -> - if Option.is_some found then - debug (fun m -> m "[Level %d] Cache hit but lone stub" d); *) - 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' = - let d = d + 1 in - match expr with - | Int i -> ([ IntAtom i ], s) - | Bool b -> ([ BoolAtom b ], s) - | Function (_, _, l) -> ([ FunAtom (expr, l, sigma) ], s) - | Appl (e, _, l) -> - 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 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, pruned_sigma', s) in *) - let lst = NewSt.Lstate st in - debug (fun m -> m "State: %s" (NewSt.show lst)); - debug_plain "v_set:"; - log_v_set v; - let stub_key = (l, sigma) in - (* TODO: try two-pass mechanism again *) - if Set.mem v lst then ( - debug_plain "Stubbed"; - info (fun m -> - 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" 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 - (* we don't remember whatever this subtree visited *) - let r1, s1 = analyze_aux_step d e sigma pi s 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 new_s = Set.add s1 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 - in - (List.fold ri ~init:acc_r ~f:Set.add, Set.union acc_s si)) - in - let r2 = Set.elements r2 in - 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 Interp.Pp.pp_expr expr); - (r2, s2)) - | Var (Ident x, l) -> - info (fun m -> m "[Level %d] ====== Var (%s, %d) ======" d x l); - let st = (expr, sigma, s) in - let est = NewSt.Estate st in - debug (fun m -> m "State: %s" (Grammar.NewSt.show est)); - debug_plain "v_set:"; - log_v_set v; - let stub_key = (expr, sigma) in - if Set.mem v est then ( - (* Var Stub *) - debug (fun m -> m "Stubbed: %s" x); - info (fun m -> m "[Level %d] ****** Var (%s, %d) *******" d x l); - ([ EStubAtom stub_key ], 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)); - let new_v = Set.add v est in - (* 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 - 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 - let r1 = elim_stub r1 (St.Estate (expr, sigma)) in - let r1 = [ EResAtom (r1, stub_key) ] 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); + let cache_key = (expr, sigma, v, s, pi) in + let found = Hashtbl.find cache cache_key in + match found with + | Some r when not (exists_lone_stub v (Set.empty (module St)) r) -> + (* Format.printf "cache hit\n"; *) + debug (fun m -> m "cache hit: %a" pp_res r); + (* debug (fun m -> m "cache hit: %a" Grammar.pp_res r); *) + (r, s) + | _ -> + if Option.is_some found then + debug (fun m -> m "[Level %d] Cache hit but lone stub" d); + 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' = + let d = d + 1 in + match expr with + | Int i -> ([ IntAtom i ], s) + | Bool b -> ([ BoolAtom b ], s) + | Function (_, _, l) -> ([ FunAtom (expr, l, sigma) ], s) + | Appl (e, _, l) -> + 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 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, pruned_sigma', s) in *) + let lst = NewSt.Lstate st in + debug (fun m -> m "State: %s" (NewSt.show lst)); + debug_plain "v_set:"; + log_v_set v; + let stub_key = (l, sigma) in + (* TODO: try two-pass mechanism again *) + if Set.mem v lst then ( + debug_plain "Stubbed"; + info (fun m -> + 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" 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 + (* we don't remember whatever this subtree visited *) + let r1, s1 = analyze_aux_step d e sigma pi s 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 new_s = Set.add s1 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 "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)); - let r0, s0 = analyze_aux_step d e1 si_tl pi s 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 new_v = Set.add v (NewSt.Estate (expr, sigma, s1)) 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 - in - ( List.fold r0' ~init:acc_r ~f:Set.add, - Set.union acc_s s0' )) - else (acc_r, acc_s)) + 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 in + (List.fold ri ~init:acc_r ~f:Set.add, Set.union acc_s si)) + in + let r2 = Set.elements r2 in + 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 Interp.Pp.pp_expr + expr); + (r2, s2)) + | Var (Ident x, l) -> + info (fun m -> m "[Level %d] ====== Var (%s, %d) ======" d x l); + let st = (expr, sigma, s) in + let est = NewSt.Estate st in + debug (fun m -> m "State: %s" (Grammar.NewSt.show est)); + debug_plain "v_set:"; + log_v_set v; + let stub_key = (expr, sigma) in + if Set.mem v est then ( + (* Var Stub *) + debug (fun m -> m "Stubbed: %s" x); + info (fun m -> m "[Level %d] ****** Var (%s, %d) *******" d x l); + ([ EStubAtom stub_key ], 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 Non-Local (%s, %d) *******" d x - l); + 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)); + let new_v = Set.add v est in + (* 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 + 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 + let r1 = elim_stub r1 (St.Estate (expr, sigma)) in + let r1 = [ EResAtom (r1, stub_key) ] in + (r1, s1) + | _ -> raise Unreachable [@coverage off]) + else ( + (* Var Non-Local *) info (fun m -> - m "[Level %d] ****** Var (%s, %d) *******" d x l); - let r2 = Set.elements r2 in - let r2 = elim_stub r2 (St.Estate stub_key) in - (* let r2 = [ EResAtom (r2, stub_key) ] in *) - (r2, s2) - | _ -> raise Unreachable [@coverage off]) - | _ -> raise Unreachable [@coverage off]) - | If (e, e_true, e_false, l) -> ( - (* let r_true, s_true = analyze_aux_step d e_true sigma None s v in - info (fun m -> m "Evaluating: %a" Interpreter.Pp.pp_expr e_false); - let r_false, s_false = analyze_aux_step d e_false sigma None s v in - (r_true @ r_false, Set.union s (Set.union s_true s_false)) *) - info (fun m -> m "[Level %d] ====== If (%d) ======" d l); - let r_cond, s0 = analyze_aux_step d e sigma pi s v in - debug (fun m -> m "r_cond: %a" Utils.pp_res r_cond); - debug (fun m -> m "r_cond: %a" Grammar.pp_res r_cond); - debug_plain "v_set:"; - log_v_set v; - let true_sat = solve_cond r_cond true in - let pc_true = (r_cond, true) in - let false_sat = solve_cond r_cond false in - let pc_false = (r_cond, false) in - match (true_sat, false_sat) with - | true, false -> - info (fun m -> m "[Level %d] ====== If True only ======" d); - 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 only ******" d); - debug (fun m -> m "[Level %d] ****** If (%d) *******" d l); - ([ 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" Interp.Pp.pp_expr e_false); - let r_false, s_false = - analyze_aux_step d e_false sigma (Some pc_false) s0 v - in - info (fun m -> m "[Level %d] ****** If False only ******" d); - info (fun m -> m "[Level %d] ****** If (%d) *******" d l); - ([ PathCondAtom (pc_false, r_false) ], Set.union s0 s_false) - | _ -> - info (fun m -> m "[Level %d] ====== If both ======" d); - info (fun m -> m "[Level %d] ====== If True ======" d); - 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" Interp.Pp.pp_expr e_false); - let r_false, s_false = - analyze_aux_step d e_false sigma (Some pc_false) s0 v - in - info (fun m -> m "[Level %d] ****** If False ******" d); - info (fun m -> m "[Level %d] ****** If both ******" d); - info (fun m -> m "[Level %d] ****** If (%d) *******" d l); - let pc_false = PathCondAtom (pc_false, r_false) in - let pc_true = PathCondAtom (pc_true, r_true) in - ([ pc_true; pc_false ], Set.union s0 (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) -> - info (fun m -> - 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 -> - 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 _ -> PlusAtom (r1, r2) - | Minus _ -> MinusAtom (r1, r2) - | Mult _ -> MultAtom (r1, r2) - | Equal _ -> EqAtom (r1, r2) - | And _ -> AndAtom (r1, r2) - | Or _ -> OrAtom (r1, r2) - | Ge _ -> GeAtom (r1, r2) - | Gt _ -> GtAtom (r1, r2) - | Le _ -> LeAtom (r1, r2) - | Lt _ -> LtAtom (r1, r2) - | _ -> raise Unreachable [@coverage off]); - ], - Set.union s (Set.union s1 s2) ) - | Not e -> - let r, s = analyze_aux_step d e sigma pi s v in - ([ NotAtom r ], s) - | Record es -> - if List.is_empty es then ([ RecAtom [] ], s) - else - es - |> List.map ~f:(fun (id, ei) -> - (id, analyze_aux_step d ei sigma pi s v)) - |> List.map ~f:(fun (id, (r, s)) -> ((id, r), s)) - |> List.unzip - |> fun (rs, ss) -> ([ RecAtom rs ], Set.union_list (module S_key) ss) - | Projection (e, x) -> - let r0, s0 = analyze_aux_step d e sigma pi s v in - ([ ProjAtom (r0, x) ], s0) - | Inspection (x, e) -> - let r0, s0 = analyze_aux_step d e sigma pi s v in - ([ InspAtom (x, r0) ], s0) - | LetAssert (id, e1, e2) -> - let r1, s1 = analyze_aux_step d e1 sigma pi s 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; *) - (simplify r, s') + 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)); + let r0, s0 = + analyze_aux_step d e1 si_tl pi s 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 new_v = + Set.add v (NewSt.Estate (expr, sigma, s1)) + 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 + 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 + let r2 = elim_stub r2 (St.Estate stub_key) in + (* let r2 = [ EResAtom (r2, stub_key) ] in *) + (r2, s2) + | _ -> raise Unreachable [@coverage off]) + | _ -> raise Unreachable [@coverage off]) + | If (e, e_true, e_false, l) -> ( + (* let r_true, s_true = analyze_aux_step d e_true sigma None s v in + info (fun m -> m "Evaluating: %a" Interpreter.Pp.pp_expr e_false); + let r_false, s_false = analyze_aux_step d e_false sigma None s v in + (r_true @ r_false, Set.union s (Set.union s_true s_false)) *) + info (fun m -> m "[Level %d] ====== If (%d) ======" d l); + let r_cond, s0 = analyze_aux_step d e sigma pi s v in + debug (fun m -> m "r_cond: %a" Utils.pp_res r_cond); + debug (fun m -> m "r_cond: %a" Grammar.pp_res r_cond); + debug_plain "v_set:"; + log_v_set v; + let true_sat = solve_cond r_cond true in + let pc_true = (r_cond, true) in + let false_sat = solve_cond r_cond false in + let pc_false = (r_cond, false) in + match (true_sat, false_sat) with + | true, false -> + info (fun m -> m "[Level %d] ====== If True only ======" d); + 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 only ******" d); + debug (fun m -> m "[Level %d] ****** If (%d) *******" d l); + ([ 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" Interp.Pp.pp_expr e_false); + let r_false, s_false = + analyze_aux_step d e_false sigma (Some pc_false) s0 v + in + info (fun m -> m "[Level %d] ****** If False only ******" d); + info (fun m -> m "[Level %d] ****** If (%d) *******" d l); + ([ PathCondAtom (pc_false, r_false) ], Set.union s0 s_false) + | _ -> + info (fun m -> m "[Level %d] ====== If both ======" d); + info (fun m -> m "[Level %d] ====== If True ======" d); + 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" Interp.Pp.pp_expr e_false); + let r_false, s_false = + analyze_aux_step d e_false sigma (Some pc_false) s0 v + in + info (fun m -> m "[Level %d] ****** If False ******" d); + info (fun m -> m "[Level %d] ****** If both ******" d); + info (fun m -> m "[Level %d] ****** If (%d) *******" d l); + let pc_false = PathCondAtom (pc_false, r_false) in + let pc_true = PathCondAtom (pc_true, r_true) in + ([ pc_true; pc_false ], Set.union s0 (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) -> + info (fun m -> + 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 -> + 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 _ -> PlusAtom (r1, r2) + | Minus _ -> MinusAtom (r1, r2) + | Mult _ -> MultAtom (r1, r2) + | Equal _ -> EqAtom (r1, r2) + | And _ -> AndAtom (r1, r2) + | Or _ -> OrAtom (r1, r2) + | Ge _ -> GeAtom (r1, r2) + | Gt _ -> GtAtom (r1, r2) + | Le _ -> LeAtom (r1, r2) + | Lt _ -> LtAtom (r1, r2) + | _ -> raise Unreachable [@coverage off]); + ], + Set.union s (Set.union s1 s2) ) + | Not e -> + let r, s = analyze_aux_step d e sigma pi s v in + ([ NotAtom r ], s) + | Record es -> + if List.is_empty es then ([ RecAtom [] ], s) + else + es + |> List.map ~f:(fun (id, ei) -> + (id, analyze_aux_step d ei sigma pi s v)) + |> List.map ~f:(fun (id, (r, s)) -> ((id, r), s)) + |> List.unzip + |> fun (rs, ss) -> + ([ RecAtom rs ], Set.union_list (module S_key) ss) + | Projection (e, x) -> + let r0, s0 = analyze_aux_step d e sigma pi s v in + ([ ProjAtom (r0, x) ], s0) + | Inspection (x, e) -> + let r0, s0 = analyze_aux_step d e sigma pi s v in + ([ InspAtom (x, r0) ], s0) + | LetAssert (id, e1, e2) -> + let r1, s1 = analyze_aux_step d e1 sigma pi s 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; + (simplify r, s') (* (r, s') *) and analyze_aux n e_glob d expr sigma pi s v = @@ -555,13 +574,12 @@ and analyze_aux n e_glob d expr sigma pi s v = 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; *) + Hashtbl.clear cache; let r, s' = analyze_aux (n + 1) e_glob 0 e_glob [] None s' (Set.empty (module NewSt)) 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) e = @@ -573,7 +591,7 @@ let analyze ?(debug_mode = false) ?(verify = true) ?(test_num = 0) e = (* let r, s = analyze_aux 0 e 0 e [] None - (Set.empty (module SKey)) + (Set.empty (module S_key)) (Set.empty (module NewSt)) in *) let r, s = diff --git a/program_analysis/src/logging.ml b/program_analysis/src/logging.ml index a6c127b..4635517 100644 --- a/program_analysis/src/logging.ml +++ b/program_analysis/src/logging.ml @@ -2,7 +2,7 @@ open Logs (* controls whether to generate logs: "logs" in _build/default/program_analysis/tests *) -let gen_logs = ref false +let gen_logs = ref true 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 diff --git a/program_analysis/src/utils.ml b/program_analysis/src/utils.ml index 0f799fa..1f4dd45 100644 --- a/program_analysis/src/utils.ml +++ b/program_analysis/src/utils.ml @@ -57,8 +57,8 @@ let rec pp_atom fmt = function |> 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' *) + (* | PathCondAtom (_, r) -> ff fmt "%a" pp_res r *) + | PathCondAtom ((r, b), r') -> ff fmt "(%a = %b ⊩ %a)" pp_res r b pp_res r' | RecAtom entries -> ff fmt (if List.is_empty entries then "{%a}" else "{ %a }") diff --git a/program_analysis/tests/inputs/blur.ml b/program_analysis/tests/inputs/blur.ml index a9a40a6..e59b9c3 100644 --- a/program_analysis/tests/inputs/blur.ml +++ b/program_analysis/tests/inputs/blur.ml @@ -7,7 +7,8 @@ letassert x = else let r = blur id true in let s = blur id false in - if (blur (self self) s (n - 1)) then false else true + (* if (blur (self self) s (n - 1)) then false else true *) + not (blur (self self) s (n - 1)) in lp lp false 2 in x diff --git a/program_analysis/tests/inputs/kcfa2.ml b/program_analysis/tests/inputs/kcfa2.ml index 30af0f9..a25906d 100644 --- a/program_analysis/tests/inputs/kcfa2.ml +++ b/program_analysis/tests/inputs/kcfa2.ml @@ -1,5 +1,5 @@ (* https://github.com/adamsmd/paper-push-down-for-free-prototype/blob/master/benchmarks/gcfa2/kcfa2.scm *) -letassert x = +(* letassert x = *) (fun f1 -> let a = (f1 true) in f1 false) (fun x1 -> @@ -7,4 +7,4 @@ letassert x = let b = (f2 true) in let c = (f2 false) in f2 true) (fun x2 -> (fun z -> z x1 x2) (fun y1 -> fun y2 -> y1))) -in not x +(* in not x *) diff --git a/program_analysis/tests/inputs/mack.ml b/program_analysis/tests/inputs/mack.ml new file mode 100644 index 0000000..62a9290 --- /dev/null +++ b/program_analysis/tests/inputs/mack.ml @@ -0,0 +1,5 @@ +let mack = fun self -> fun n -> + if n = 0 then self self 1 + else self self (self self (n - 1)) +in +mack mack 0 \ No newline at end of file diff --git a/program_analysis/tests/inputs/map.ml b/program_analysis/tests/inputs/map.ml index b1c9993..367374b 100644 --- a/program_analysis/tests/inputs/map.ml +++ b/program_analysis/tests/inputs/map.ml @@ -1,7 +1,8 @@ let id = (fun xx -> xx) in let my_map = (fun f -> fun l -> let lp = fun self -> fun lst -> - if (if (hd in lst) then false else true) then {} + (* if (if (hd in lst) then false else true) then {} *) + if not (hd in lst) then {} else ({ hd = id f (lst.hd); tl = self self (lst.tl) }) in lp lp l) in diff --git a/program_analysis/tests/inputs/not.ml b/program_analysis/tests/inputs/not.ml new file mode 100644 index 0000000..e69de29 diff --git a/program_analysis/tests/inputs/primtest.ml b/program_analysis/tests/inputs/primtest.ml index e7635cc..ce960bc 100644 --- a/program_analysis/tests/inputs/primtest.ml +++ b/program_analysis/tests/inputs/primtest.ml @@ -31,7 +31,8 @@ in let generate_fermat_prime = (fun self -> fun byte_size -> fun iterations -> let n = rand byte_size in - if (if (is_trivial_composite n) && (is_fermat_prime is_fermat_prime n iterations) then false else true) then + (* if (if (is_trivial_composite n) && (is_fermat_prime is_fermat_prime n iterations) then false else true) then *) + if not ((is_trivial_composite n) && (is_fermat_prime is_fermat_prime n iterations)) then n else self self byte_size iterations) diff --git a/program_analysis/tests/inputs/sat-2.ml b/program_analysis/tests/inputs/sat-2.ml index 508b6d1..4d0faf2 100644 --- a/program_analysis/tests/inputs/sat-2.ml +++ b/program_analysis/tests/inputs/sat-2.ml @@ -2,10 +2,10 @@ let phi = fun x1 -> fun x2 -> fun x3 -> fun x4 -> fun x5 -> fun x6 -> fun x7 -> (x1 || x2) && - (x1 || (if x2 then false else true) || (if x3 then false else true)) && + (x1 || (not x2) || (not x3)) && (x3 || x4) && - ((if x4 then false else true) || x1) && - ((if x2 then false else true) || (if x3 then false else true)) && + ((not x4) || x1) && + ((not x2) || (not x3)) && (x4 || x2) in let try_ = fun f -> diff --git a/program_analysis/tests/inputs/sat-3.ml b/program_analysis/tests/inputs/sat-3.ml index a120099..44dad81 100644 --- a/program_analysis/tests/inputs/sat-3.ml +++ b/program_analysis/tests/inputs/sat-3.ml @@ -1,10 +1,10 @@ -let not' = fun b -> if b then false else true in +(* let not' = fun b -> if b then false else true in *) let phi = fun ps -> ((ps.x1) || (ps.x2)) && - ((ps.x1) || (if (ps.x2) then false else true) || (if (ps.x3) then false else true)) && + ((ps.x1) || (not (ps.x2)) || (not (ps.x3))) && ((ps.x3) || (ps.x4)) && - ((if (ps.x4) then false else true) || (ps.x1)) && - ((if (ps.x2) then false else true) || (if (ps.x3) then false else true)) && + ((not (ps.x4)) || (ps.x1)) && + ((not (ps.x2)) || (not (ps.x3))) && ((ps.x4) || (ps.x2)) in let try_ = fun f -> diff --git a/program_analysis/tests/tests.ml b/program_analysis/tests/tests.ml index b2b8afb..798e02e 100644 --- a/program_analysis/tests/tests.ml +++ b/program_analysis/tests/tests.ml @@ -68,7 +68,7 @@ let recursion_thunked = [ (fun _ -> ( "(1 + (1 + ((1 + ((1 + stub) | 0)) | 0)))", - pau ~test_num:18 ~verify:true recursion.(0) )); + pau' ~test_num:18 ~verify:true recursion.(0) )); (* (fun _ -> ( "(false or (false or ((false or ((false or stub) | true)) | true)))", pau ~test_num:19 ~verify:false recursion.(1) )); *) @@ -193,49 +193,85 @@ let ddpa_display_thunked = let test_ddpa_display _ = gen_test ddpa_display_thunked -let ddpa_thunked = +let poly_thunked = [ - (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 _ -> - ( "((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") )); + ( "(90 * ((((9 | (stub - 1)) - 1) * ((((9 | (stub - 1)) - 1) * stub) | \ + 1)) | 1))", + pau ~verify:false ~test_name:"fact 10" + "let fact = fun self -> fun n -> if n = 0 then 1 else n * self self \ + (n - 1) in fact fact 10" )); *) + (* (fun _ -> + ( "(380 * ((((19 | (stub - 1)) - 1) * ((((19 | (stub - 1)) - 1) * stub) \ + | 1)) | 1))", + pau ~verify:false ~test_name:"fact 20" + "let fact = fun self -> fun n -> if n = 0 then 1 else n * self self \ + (n - 1) in fact fact 20" )); *) + (* (fun _ -> + ( "(1560 * ((((39 | (stub - 1)) - 1) * ((((39 | (stub - 1)) - 1) * stub) \ + | 1)) | 1))", + pau ~verify:false ~test_name:"fact 40" + "let fact = fun self -> fun n -> if n = 0 then 1 else n * self self \ + (n - 1) in fact fact 40" )); *) + (* (fun _ -> + ( "(3540 * ((((59 | (stub - 1)) - 1) * ((((59 | (stub - 1)) - 1) * stub) \ + | 1)) | 1))", + pau ~verify:false ~test_name:"fact 60" + "let fact = fun self -> fun n -> if n = 0 then 1 else n * self self \ + (n - 1) in fact fact 60" )); *) (fun _ -> - ( "(false | true)", - pau ~verify:false ~test_name:"sat-2" (read_input "sat-2.ml") )); + ( "(9900 * ((((99 | (stub - 1)) - 1) * ((((99 | (stub - 1)) - 1) * stub) \ + | 1)) | 1))", + pau ~verify:false ~test_name:"fact 100" + "let fact = fun self -> fun n -> if n = 0 then 1 else n * self self \ + (n - 1) in fact fact 100" )); + ] + +let test_poly _ = gen_test poly_thunked + +let ddpa_thunked = + [ + (* (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 _ -> + ( "((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 _ -> + ("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 _ -> @@ -249,34 +285,33 @@ let test_ddpa _ = gen_test ddpa_thunked let ddpa_simple_thunked = [ (* (fun _ -> - ( "(false | true)", - pau' ~verify:false ~test_name:"blur" (read_input "blur.ml") )); *) - (* (fun _ -> - ("false", pau' ~verify:false ~test_name:"eta" (read_input "eta.ml"))); *) - (* (fun _ -> - ( "Int", - pau' ~verify:false ~test_name:"facehugger" (read_input "facehugger.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"))); *) + ( "(false | true)", + pau' ~verify:false ~test_name:"blur" (read_input "blur.ml") )); *) (fun _ -> - ( "(Int | (stub | (stub | (stub | (stub | stub)))))", - pau' ~verify:false ~test_name:"loop2-1" (read_input "loop2-1.ml") )); + ("false", pau' ~verify:false ~test_name:"eta" (read_input "eta.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 _ -> - ( "stub", - pau' ~verify:false ~test_name:"primtest" (read_input "primtest.ml") )); *) + ( "Int", + pau' ~verify:false ~test_name:"facehugger" (read_input "facehugger.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 _ -> + ("Int", 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 _ -> + ( "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"))); *) + ("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 _ -> @@ -284,6 +319,8 @@ let ddpa_simple_thunked = 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:"mack" (read_input "mack.ml"))); *) (* (fun _ -> ("Int", pau' ~verify:false ~test_name:"tak" (read_input "tak.ml"))); *) (* (fun _ -> @@ -305,6 +342,7 @@ let test_pa = (* "Adapted" >:: test_adapted; *) (* "Lists" >:: test_lists; *) (* "pruned_d" >:: test_prune_d; *) + (* "Polynomial" >:: test_poly; *) "DDPA (simple)" >: test_case test_ddpa_simple ~length:(OUnitTest.Custom_length 100000.); (* "DDPA" >: test_case test_ddpa ~length:(OUnitTest.Custom_length 100000.); *) diff --git a/program_analysis/tests/utils.ml b/program_analysis/tests/utils.ml index e770969..65f7f76 100644 --- a/program_analysis/tests/utils.ml +++ b/program_analysis/tests/utils.ml @@ -49,6 +49,6 @@ let pau' ?(verify = true) ?(test_num = 0) if time then ( Format.printf "%s: %f\n" test_name (after -. before); flush_all ()); - r |> Format.asprintf "%a" Simple_pa.Utils.pp_res + r |> Core.Set.elements |> Format.asprintf "%a" Simple_pa.Utils.pp_res let pau'' = Display_pa.Debugutils.pau