[sledge] Improve tracing

Reviewed By: jvillard

Differential Revision: D24630523

fbshipit-source-id: 1e42bd331

sledge/src/exec.ml

@@ -636,6 +636,8 @@ let strlen_spec reg ptr =
 
 open Option.Import
 
+let pp ppf q = Sh.pp ppf (Option.value q ~default:(Sh.false_ Var.Set.empty))
+
 let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) =
   let gain_us = Var.Set.diff q1.us q0.us in
   let lose_us = Var.Set.diff q0.us q1.us in
@@ -679,7 +681,7 @@ let exec_spec_ (xs, pre) (gs, {foot; sub; ms; post}) =
     (Sh.star post (Sh.exists ms (Sh.rename sub frame))))
   |>
   [%Trace.retn fun {pf} r ->
-    pf "%a" (Option.pp "%a" Sh.pp) r ;
+    pf "%a" pp r ;
     assert (Option.for_all ~f:(check_preserve_us (Sh.exists xs pre)) r)]
 
 (* execute a command with given spec from pre *)

sledge/src/fol/context.ml

@@ -445,8 +445,8 @@ let pp_diff_cls = List.pp_diff ~cmp:Trm.compare "@ = " Trm.pp
 let ppx_classes x fs clss =
   List.pp "@ @<2>∧ "
     (fun fs (rep, cls) ->
-      Format.fprintf fs "@[%a@ = %a@]" (Trm.ppx x) rep (ppx_cls x)
-        (List.sort ~cmp:Trm.compare cls) )
+      if not (List.is_empty cls) then
+        Format.fprintf fs "@[%a@ = %a@]" (Trm.ppx x) rep (ppx_cls x) cls )
     fs
     (Iter.to_list (Trm.Map.to_iter clss))
 
@@ -455,9 +455,26 @@ let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r)
 let pp_diff_clss =
   Trm.Map.pp_diff ~eq:(List.equal Trm.equal) Trm.pp pp_cls pp_diff_cls
 
-let pp fs r = ppx_classes (fun _ -> None) fs (classes r)
+let pp fs r =
+  let clss = classes r in
+  if Trm.Map.is_empty clss then
+    Format.fprintf fs (if r.sat then "tt" else "ff")
+  else ppx_classes (fun _ -> None) fs clss
 
 let ppx var_strength fs clss noneqs =
+  let without_anon_vars =
+    List.filter ~f:(fun e ->
+        match Var.of_trm e with
+        | Some v -> Poly.(var_strength v <> Some `Anonymous)
+        | None -> true )
+  in
+  let clss =
+    Trm.Map.fold clss Trm.Map.empty ~f:(fun ~key:rep ~data:cls m ->
+        let cls = without_anon_vars cls in
+        if not (List.is_empty cls) then
+          Trm.Map.add ~key:rep ~data:(List.sort ~cmp:Trm.compare cls) m
+        else m )
+  in
   let first = Trm.Map.is_empty clss in
   if not first then Format.fprintf fs "  " ;
   ppx_classes var_strength fs clss ;
@@ -547,7 +564,7 @@ let rec canon r a =
 
 let canon_f r b =
   [%trace]
-    ~call:(fun {pf} -> pf "%a@ %a" Fml.pp b pp r)
+    ~call:(fun {pf} -> pf "%a@ %a" Fml.pp b pp_raw r)
     ~retn:(fun {pf} -> pf "%a" Fml.pp)
   @@ fun () -> Fml.map_trms ~f:(canon r) b
 
@@ -773,7 +790,7 @@ let dnf f =
   Fml.fold_dnf ~meet1 ~join1 ~top ~bot f
 
 let rename r sub =
-  [%Trace.call fun {pf} -> pf "%a" pp r]
+  [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp r]
   ;
   let rep =
     Subst.map_entries ~f:(Trm.map_vars ~f:(Var.Subst.apply sub)) r.rep
@@ -1103,7 +1120,7 @@ let pp_vss fs vss =
     [fv u ⊆ ⋃ⱼ₌₁ⁱ vⱼ] *)
 let solve_for_vars vss r =
   [%Trace.call fun {pf} ->
-    pf "%a@ @[%a@]@ @[%a@]" pp_vss vss pp_classes r pp r ;
+    pf "%a@ @[%a@]" pp_vss vss pp r ;
     invariant r]
   ;
   let wrt = Var.Set.union_list vss in

sledge/src/fol/trm.ml

@@ -136,6 +136,24 @@ end = struct
     | Var {id= i; name= _}, Var {id= j; name= _} -> Int.equal i j
     | _ -> equal x y
 
+  (* nul-terminated string value represented by a concatenation *)
+  let string_of_concat xs =
+    let exception Not_a_string in
+    try
+      let len_1 = Array.length xs - 1 in
+      ( match xs.(len_1) with
+      | Sized {siz= Z o; seq= Z c} when Z.equal Z.one o && Z.equal Z.zero c
+        ->
+          ()
+      | _ -> raise_notrace Not_a_string ) ;
+      Some
+        (String.init len_1 ~f:(fun i ->
+             match xs.(i) with
+             | Sized {siz= Z o; seq= Z c} when Z.equal Z.one o ->
+                 Char.of_int_exn (Z.to_int c)
+             | _ -> raise_notrace Not_a_string ))
+    with _ -> None
+
   let rec ppx strength fs trm =
     let rec pp fs trm =
       let pf fmt = pp_boxed fs fmt in
@@ -149,15 +167,9 @@ end = struct
       | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len
       | Concat [||] -> pf "@<2>⟨⟩"
       | Concat xs -> (
-          let exception Not_a_string in
-          try
-            pf "%S"
-              (String.init (Array.length xs) ~f:(fun i ->
-                   match xs.(i) with
-                   | Sized {siz= Z o; seq= Z c} when Z.equal Z.one o ->
-                       Char.of_int_exn (Z.to_int c)
-                   | _ -> raise_notrace Not_a_string ))
-          with _ -> pf "(%a)" (Array.pp "@,^" pp) xs )
+        match string_of_concat xs with
+        | Some s -> pf "%S" s
+        | None -> pf "(%a)" (Array.pp "@,^" pp) xs )
       | Apply (f, [||]) -> pf "%a" Funsym.pp f
       | Apply
           ( ( (Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr)

sledge/src/fol/var0.ml

@@ -16,13 +16,14 @@ module Make (T : REPR) = struct
   let ppx strength ppf v =
     let id = id v in
     let name = name v in
-    if id = 0 then Trace.pp_styled `Bold "%%%s" ppf name
-    else
-      match strength v with
-      | None -> Format.fprintf ppf "%%%s_%d" name id
-      | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" ppf name id
-      | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" ppf name id
-      | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf
+    let pp_id ppf id = if id <> 0 then Format.fprintf ppf "_%d" id in
+    match strength v with
+    | None ->
+        if id = 0 then Trace.pp_styled `Bold "%%%s" ppf name
+        else Format.fprintf ppf "%%%s%a" name pp_id id
+    | Some `Universal -> Trace.pp_styled `Bold "%%%s%a" ppf name pp_id id
+    | Some `Existential -> Trace.pp_styled `Cyan "%%%s%a" ppf name pp_id id
+    | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf
 
   let pp = ppx (fun _ -> None)
 

sledge/src/llair/exp.ml

@@ -161,7 +161,8 @@ and pp_record fs elts =
   match
     String.init (IArray.length elts) ~f:(fun i ->
         match IArray.get elts i with
-        | Integer {data; _} -> Char.of_int_exn (Z.to_int data)
+        | Integer {data; typ= Integer {byts= 1; _}} ->
+            Char.of_int_exn (Z.to_int data)
         | _ -> raise_notrace (Invalid_argument "not a string") )
   with
   | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)

sledge/src/llair/llair.ml

@@ -284,7 +284,7 @@ let pp_inst fs inst =
         reg msg Loc.pp loc
   | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
   | Intrinsic {reg; name; args; loc} ->
-      pf "@[<2>%aintrinsic %a(%a);@]\t%a"
+      pf "@[<2>%aintrinsic@ %a(@,@[<hv>%a@]);@]\t%a"
         (Option.pp "%a := " Reg.pp)
         reg Intrinsic.pp name (IArray.pp ",@ " Exp.pp) args Loc.pp loc
 

sledge/src/sh.ml

@@ -181,41 +181,46 @@ let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us =
         [%Trace.fprintf
           fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)]
 
-let rec pp_ ?var_strength vs parent_xs parent_ctx fs
+let rec pp_ ?var_strength ?vs ancestor_xs parent_ctx fs
     {us; xs; ctx; pure; heap; djns} =
   Format.pp_open_hvbox fs 0 ;
   let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find v m) var_strength in
-  pp_us ~vs () fs us ;
+  pp_us ~pre:"@<2>∀ " ?vs () fs us ;
+  let vs = Option.value vs ~default:Var.Set.empty in
   let xs_d_vs, xs_i_vs =
     Var.Set.diff_inter
       (Var.Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous)))
       vs
   in
   if not (Var.Set.is_empty xs_i_vs) then (
-    Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.ppx x) xs_i_vs ;
+    Format.fprintf fs "@<3>∃↑ @[%a@] ." (Var.Set.ppx x) xs_i_vs ;
     if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
   if not (Var.Set.is_empty xs_d_vs) then
     Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
   let first =
     if Option.is_some var_strength then
       Context.ppx_diff x fs parent_ctx pure ctx
-    else if Formula.equal Formula.tt pure then true
     else (
-      Format.fprintf fs "@[  %a@]" Formula.pp pure ;
+      Format.fprintf fs "@[  %a@ @<2>∧ %a@]" Context.pp ctx Formula.pp
+        pure ;
       false )
   in
   if List.is_empty heap then
     Format.fprintf fs
       ( if first then if List.is_empty djns then "  emp" else ""
       else "@ @<5>∧ emp" )
-  else pp_heap x ~pre:(if first then "  " else "@ @<2>∧ ") ctx fs heap ;
+  else
+    pp_heap x
+      ~pre:(if first then "  " else "@ @<2>∧ ")
+      (if Option.is_some var_strength then ctx else emp.ctx)
+      fs heap ;
   let first = first && List.is_empty heap in
   List.pp
     ~pre:(if first then "  " else "@ * ")
     "@ * "
     (pp_djn ?var_strength
        (Var.Set.union vs (Var.Set.union us xs))
-       (Var.Set.union parent_xs xs)
+       (Var.Set.union ancestor_xs xs)
        ctx)
     fs djns ;
   Format.pp_close_box fs ()
@@ -230,12 +235,12 @@ and pp_djn ?var_strength vs xs ctx fs = function
                var_strength_ xs var_strength_stem sjn
              in
              Format.fprintf fs "@[<hv 1>(%a)@]"
-               (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) ctx)
+               (pp_ ?var_strength ~vs (Var.Set.union xs sjn.xs) ctx)
                sjn ))
         djn
 
-let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) ctx fs q =
-  pp_ ~var_strength:(var_strength ~xs q) us xs ctx fs q
+let pp_diff_eq ?us ?(xs = Var.Set.empty) ctx fs q =
+  pp_ ~var_strength:(var_strength ~xs q) ?vs:us xs ctx fs q
 
 let pp fs q = pp_diff_eq Context.empty fs q
 
@@ -243,7 +248,7 @@ let pp_djn fs d =
   pp_djn ?var_strength:None Var.Set.empty Var.Set.empty Context.empty fs d
 
 let pp_raw fs q =
-  pp_ ?var_strength:None Var.Set.empty Var.Set.empty Context.empty fs q
+  pp_ ?var_strength:None ?vs:None Var.Set.empty Context.empty fs q
 
 let fv_seg seg = fold_vars_seg ~f:Var.Set.add seg Var.Set.empty
 
@@ -794,5 +799,5 @@ let simplify q =
   q
   |>
   [%Trace.retn fun {pf} q' ->
-    pf "@\n" ;
+    pf "%a" pp_raw q' ;
     invariant q']

sledge/src/test/context_test.ml

@@ -58,8 +58,8 @@ let%test_module _ =
       pp r3 ;
       [%expect
         {|
-        %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %t_1)
-        = g(%y_6, %t_1)
+        %t_1 = g(%y_6, %t_1) = g(%y_6, %t_1) = %z_7 = %x_5 = %w_4 = %v_3
+        = %u_2
 
       {sat= true;
        rep= [[%t_1 ↦ ];

sledge/src/test/fol_test.ml

@@ -112,7 +112,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp r0 ;
-      [%expect {||}]
+      [%expect {| tt |}]
 
     let%test _ = difference r0 (f x) (f x) |> Poly.equal (Some (Z.of_int 0))
     let%test _ = difference r0 !4 !3 |> Poly.equal (Some (Z.of_int 1))
@@ -138,7 +138,7 @@ let%test_module _ =
       pp_raw r2 ;
       [%expect
         {|
-        %x_5 = %y_6 = %z_7 = f(%x_5)
+        %x_5 = f(%x_5) = %z_7 = %y_6
 
       {sat= true;
        rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [f(%x_5) ↦ %x_5]]} |}]
@@ -181,8 +181,8 @@ let%test_module _ =
       pp_raw r3 ;
       [%expect
         {|
-        %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %t_1)
-        = g(%y_6, %t_1)
+        %t_1 = g(%y_6, %t_1) = g(%y_6, %t_1) = %z_7 = %x_5 = %w_4 = %v_3
+        = %u_2
 
       {sat= true;
        rep= [[%t_1 ↦ ];
@@ -228,7 +228,7 @@ let%test_module _ =
       pp_raw r6 ;
       [%expect
         {|
-        1 = %x_5 = %y_6
+        1 = %y_6 = %x_5
 
       {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]} |}]
 
@@ -241,7 +241,7 @@ let%test_module _ =
       pp_raw r7 ;
       [%expect
         {|
-          %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
+          %v_3 = %x_5 ∧ %w_4 = %z_7 = %y_6
     
         {sat= true;
          rep= [[%v_3 ↦ ];
@@ -257,7 +257,7 @@ let%test_module _ =
       pp_raw r7' ;
       [%expect
         {|
-        %v_3 = %w_4 = %x_5 = %y_6 = %z_7
+        %v_3 = %z_7 = %y_6 = %x_5 = %w_4
 
       {sat= true;
        rep= [[%v_3 ↦ ];

sledge/src/test/sh_test.ml

@@ -91,13 +91,11 @@ let%test_module _ =
       pp_djn (dnf q) ;
       [%expect
         {|
-          ( (  0 = %x_6 ∧ emp)
-          ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
-          )
-    
-        ( (∃ %x_6, %x_7 .   (2 = %x_7) ∧ emp)
-        ∨ (∃ %x_6 .   ((1 = %x_6) ∧ (1 = %y_7)) ∧ emp)
-        ∨ (  (0 = %x_6) ∧ emp)
+          ( (  0 = %x_6 ∧ emp) ∨ (  ( (  1 = %y_7 ∧ emp) ∨ (  emp) )) )
+
+        ( (∃ %x_6, %x_7 .   2 = %x_7 ∧ (2 = %x_7) ∧ emp)
+        ∨ (∃ %x_6 .   1 = %y_7 = %x_6 ∧ ((1 = %x_6) ∧ (1 = %y_7)) ∧ emp)
+        ∨ (  0 = %x_6 ∧ (0 = %x_6) ∧ emp)
         ) |}]
 
     let%expect_test _ =
@@ -116,13 +114,13 @@ let%test_module _ =
       pp_djn (dnf q) ;
       [%expect
         {|
-          ( (  0 = _ ∧ emp)
-          ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
-          )
-    
-        ( (∃ %x_6, %x_8, %x_9 .   (2 = %x_9) ∧ emp)
-        ∨ (∃ %x_6, %x_8 .   ((1 = %y_7) ∧ (1 = %x_8)) ∧ emp)
-        ∨ (∃ %x_6 .   (0 = %x_6) ∧ emp)
+          ( (  emp) ∨ (  ( (  1 = %y_7 ∧ emp) ∨ (  emp) )) )
+
+        ( (∃ %x_6, %x_8, %x_9 .   2 = %x_9 ∧ (2 = %x_9) ∧ emp)
+        ∨ (∃ %x_6, %x_8 .
+             1 = %x_8 = %y_7 ∧ ((1 = %y_7) ∧ (1 = %x_8))
+           ∧ emp)
+        ∨ (∃ %x_6 .   0 = %x_6 ∧ (0 = %x_6) ∧ emp)
         ) |}]
 
     let%expect_test _ =
@@ -141,9 +139,7 @@ let%test_module _ =
       pp (simplify q) ;
       [%expect
         {|
-        ( (  0 = _ ∧ emp)
-        ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
-        )
+        ( (  emp) ∨ (  ( (  1 = %y_7 ∧ emp) ∨ (  emp) )) )
 
         ( (  emp) ∨ (  1 = %y_7 ∧ emp) ∨ (  emp) ) |}]
 
@@ -157,7 +153,7 @@ let%test_module _ =
         {|
         ∃ %x_6 .   %x_6 = f(%x_6) ∧ (-1 + %y_7) = f(%y_7) ∧ emp
 
-          ((1 + f(%y_7)) = %y_7) ∧ emp
+          (-1 + %y_7) = f(%y_7) ∧ ((1 + f(%y_7)) = %y_7) ∧ emp
 
           (-1 + %y_7) = f(%y_7) ∧ emp |}]
 
@@ -180,13 +176,18 @@ let%test_module _ =
       [%expect
         {|
         ∃ %a_1, %c_3, %d_4, %e_5 .
-          (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩))
+          (⟨8,%a_1⟩^⟨8,%d_4⟩) = %e_5 ∧ (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩))
         ∧ emp
-        * ( (  (0 ≠ %x_6) ∧ emp)
-          ∨ (∃ %b_2 .   (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩)) ∧ emp)
+        * ( (  tt ∧ (0 ≠ %x_6) ∧ emp)
+          ∨ (∃ %b_2 .
+               (⟨4,%c_3⟩^⟨4,%b_2⟩) = %a_1
+             ∧ (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩))
+             ∧ emp)
           )
 
-          ( (  emp) ∨ (  (0 ≠ %x_6) ∧ emp) )
+          tt ∧ tt
+        ∧ emp
+        * ( (  tt ∧ tt ∧ emp) ∨ (  tt ∧ (0 ≠ %x_6) ∧ emp) )
 
           ( (  emp) ∨ (  (0 ≠ %x_6) ∧ emp) ) |}]
   end )

sledge/src/test/solver_test.ml

@@ -143,7 +143,7 @@ let%test_module _ =
         {|
         ( infer_frame:
             %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 .   %l_6 -[)-> ⟨16,%a_3⟩
-        ) infer_frame:   %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+        ) infer_frame:   (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -158,8 +158,7 @@ let%test_module _ =
             %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
-        ) infer_frame:
-            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+        ) infer_frame:   16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -174,8 +173,7 @@ let%test_module _ =
             %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩
-        ) infer_frame:
-            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+        ) infer_frame:   16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -245,20 +243,12 @@ let%test_module _ =
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame:
-            ( (  %a_3 = _
-               ∧ 0 = %n_9
-               ∧ 16 = %m_8
-               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
-               ∧ emp)
+            ( (  0 = %n_9 ∧ 16 = %m_8 ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 ∧ emp)
             ∨ (  %a_1 = %a_2
                ∧ 2 = %n_9
                ∧ 16 = %m_8
                ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
-            ∨ (  %a_3 = _
-               ∧ 1 = %n_9
-               ∧ 16 = %m_8
-               ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
-               ∧ emp)
+            ∨ (  1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp)
             ) |}]
 
     (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)