[PA] More sync (more working recursive programs)

ghstack-source-id: fbab1f5058c768ef7522ccf10de5f53b9a722554
Pull Request resolved: #100

program_analysis/src/utils.ml

@@ -28,8 +28,11 @@ 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
-  | LabelResAtom (choices, _) | ExprResAtom (choices, _) ->
-      ff fmt "%a" pp_res choices
+  | LabelResAtom (choices, _) -> ff fmt "%a" pp_res choices
+  (* | LabelResAtom (choices, (l, _)) -> ff fmt "(%a)^%d" pp_res choices l *)
+  | ExprResAtom (choices, _) -> ff fmt "%a" pp_res choices
+  (* | ExprResAtom (choices, (e, _)) ->
+      ff fmt "(%a)^%a" pp_res choices Interpreter.Pp.pp_expr e *)
   (* ff fmt "(%a, %a, %a)" pp_res choices Interpreter.Pp.pp_expr e pp_sigma s *)
   | OpAtom op -> (
       match op with
@@ -44,15 +47,18 @@ let rec pp_atom fmt = function
       | 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)
-  | LabelStubAtom _ | ExprStubAtom _ -> ff fmt "stub"
-  (* | PathCondAtom ((r, b), r') -> ff fmt "(%a = %b ⊩ %a)" pp_res r b pp_res r' *)
+  | LabelStubAtom _ -> ff fmt "stub"
+  (* | LabelStubAtom (l, _) -> ff fmt "stub@%d" l *)
+  | ExprStubAtom _ -> ff fmt "stub"
+  (* | ExprStubAtom (e, _) -> ff fmt "(stub@%a)" Interpreter.Pp.pp_expr e *)
   (* | 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' *)
   | RecordAtom entries ->
       ff fmt
         (if List.length entries = 0 then "{%a}" else "{ %a }")
@@ -335,13 +341,17 @@ let dot_of_result ?(display_path_cond = true) test_num 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, _) ->
+    | LLabelStubAtom (st, _) -> (
         add_node (Format.sprintf "%s [label=\"stub\", shape=\"box\"];" aid);
-        let dom_node = Map.find_exn cycles (St.Lstate st) in
-        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")
+        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 ->
+            Format.printf "%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
@@ -350,7 +360,9 @@ let dot_of_result ?(display_path_cond = true) test_num r =
             let edge_id = Format.sprintf "%s_%s" dom_node aid in
             add_edge dom_node aid;
             add_edge_prop edge_id ("dir", "back")
-        | None -> failwith "Lone stub!")
+        | None ->
+            Format.printf "%s\n" (St.show_estate st);
+            failwith "Lone stub!")
     | LAssertAtom (_, r, _) ->
         add_node (Format.sprintf "%s [label=\"Assert\"];" aid);
         let rid = idr r in

program_analysis/tests/progs/adapted2.ml

@@ -0,0 +1,9 @@
+let lp1 = fun self1 -> fun i ->
+  if i = 0 then 5
+  else
+    let lp2 = fun self2 -> fun j ->
+      if j = 0 then self1 self1 (i - 1) else self2 self2 (j - 1)
+    in
+    lp2 lp2 10 
+in
+lp1 lp1 10

program_analysis/tests/progs/adapted3.ml

@@ -1,9 +1,9 @@
 let lp1 = fun self1 -> fun i ->
   if i = 0 then 5
   else
-    let lp2 = fun self2 ->
-     self1 self1 (i - 1)
+    let lp2 = fun self2 -> fun j ->
+      self1 self1 (i - 1)
     in
-    lp2 lp2
+    lp2 lp2 10 
 in
 lp1 lp1 10

program_analysis/tests/test_cases.ml

@@ -152,6 +152,7 @@ let adapted =
     read_file "tak.ml";
     read_file "cpstak.ml";
     read_file "adapted4.ml";
+    read_file "adapted2.ml";
   |]
 
 (** Church numerals *)

program_analysis/tests/tests.ml

@@ -112,32 +112,33 @@ let adapted_thunked =
        (fun _ -> ("", pau ~test_num:37 ~verify:false adapted.(7))); *)
     (* (fun _ -> ("", pau ~test_num:38 ~verify:false adapted.(8))); *)
     (* (fun _ -> ("", pau ~verify:false ~test_num:39 adapted.(9))); *)
+    (* (fun _ -> ("", pau ~verify:false ~test_num:40 adapted.(10))); *)
   ]
 
 let test_adapted _ = gen_test adapted_thunked
 
 let church_basic_thunked =
   [
-    (fun _ -> ("1", pau ~test_num:31 church_basic.(0)));
-    (fun _ -> ("2", pau ~test_num:32 church_basic.(1)));
-    (fun _ -> ("3", pau ~test_num:33 church_basic.(2)));
-    (fun _ -> ("4", pau ~test_num:34 church_basic.(3)));
+    (fun _ -> ("1", pau ~test_num:41 church_basic.(0)));
+    (fun _ -> ("2", pau ~test_num:42 church_basic.(1)));
+    (fun _ -> ("3", pau ~test_num:43 church_basic.(2)));
+    (fun _ -> ("4", pau ~test_num:44 church_basic.(3)));
   ]
 
 let test_church_basic _ = gen_test church_basic_thunked
 
 let church_binop_thunked =
-  [ (fun _ -> ("1", pau ~test_num:35 church_binop.(0))) ]
+  [ (fun _ -> ("1", pau ~test_num:45 church_binop.(0))) ]
 
 let test_church_binop _ = gen_test church_binop_thunked
 
 let lists_thunked =
   [
-    (* (fun _ -> ("1", pau ~test_num:36 lists.(0)));
-       (fun _ -> ("2", pau ~test_num:37 lists.(1)));
-       (fun _ -> ("2", pau ~test_num:38 lists.(2)));
-       (fun _ -> ("2", pau ~test_num:39 lists.(3))); *)
-    (fun _ -> ("", pau ~test_num:40 ~verify:false lists.(4)));
+    (* (fun _ -> ("1", pau ~test_num:46 lists.(0)));
+       (fun _ -> ("2", pau ~test_num:47 lists.(1)));
+       (fun _ -> ("2", pau ~test_num:48 lists.(2)));
+       (fun _ -> ("2", pau ~test_num:49 lists.(3))); *)
+    (fun _ -> ("", pau ~test_num:50 ~verify:false lists.(4)));
   ]
 
 let test_lists _ = gen_test lists_thunked
@@ -155,10 +156,10 @@ let test_pa =
        "Var local stack stitching" >:: test_local_stitching;
        "Conditional" >:: test_conditional;
        "Currying" >:: test_currying; *)
-    "Recursion" >:: test_recursion;
+    (* "Recursion" >:: test_recursion; *)
     (* "Church numerals basics" >:: test_church_basic;
        "Church numerals binary operations" >:: test_church_binop; *)
-    (* "Adapted" >:: test_adapted; *)
+    "Adapted" >:: test_adapted;
     (* "Lists" >:: test_lists; *)
   ]