From 05e1e52f0abd5dceed6f73e2200b62d6b54c5961 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 8 Feb 2021 13:11:06 -0800
Subject: [PATCH] [sledge] Improve tracing, comments, assertions for function
 call

Summary:
Add assertion to detect if the variable a function call modifies
appears in the actual parameters. In this case, the implementation is
incomplete.

Reviewed By: jvillard

Differential Revision: D26250527

fbshipit-source-id: d2e81a467
---
 sledge/src/control.ml      |  2 +-
 sledge/src/domain_sh.ml    | 34 ++++++++++++++++++++--------------
 sledge/src/llair/llair.ml  | 14 ++++++++++++++
 sledge/src/llair/llair.mli |  1 +
 4 files changed, 36 insertions(+), 15 deletions(-)

diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 2ffc12acb..19a08e855 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -313,7 +313,7 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
     let Llair.{callee; actuals; areturn; return; recursive} = call in
     let Llair.{name; formals; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
-      pf "@ %a from %a with state@ %a" Llair.Function.pp name
+      pf "@[<2>@ %a from %a with state@]@;<1 2>%a" Llair.Func.pp_call call
         Llair.Function.pp return.dst.parent.name Dom.pp state]
     ;
     let dnf_states =
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index efd29e7b0..3173ce687 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -141,41 +141,47 @@ type from_call = {areturn: Var.t option; unshadow: Var.Subst.t; frame: Sh.t}
     equations between each formal and actual, and quantify fresh vars. *)
 let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
   [%Trace.call fun {pf} ->
-    pf
-      "@ @[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \
-       globals: {@[%a@]}@ q: %a@]"
-      (IArray.pp ",@ " Llair.Exp.pp)
-      actuals
-      (IArray.pp ",@ " Llair.Reg.pp)
-      formals Llair.Reg.Set.pp locals Llair.Global.Set.pp globals pp q]
+    pf "@ @[<hv>locals: {@[%a@]}@ globals: {@[%a@]}@ q: %a@]"
+      Llair.Reg.Set.pp locals Llair.Global.Set.pp globals pp q ;
+    assert (
+      (* modifs do not appear in actuals (otherwise incomplete) *)
+      let fv_actuals =
+        actuals
+        |> IArray.to_iter
+        |> Iter.map ~f:X.term
+        |> Iter.flat_map ~f:Term.vars
+      in
+      not
+        (Option.exists areturn ~f:(fun modif ->
+             Iter.exists ~f:(Var.equal (X.reg modif)) fv_actuals )) )]
   ;
   let actuals = IArray.map ~f:X.term actuals in
   let areturn = Option.map ~f:X.reg areturn in
   let formals = IArray.map ~f:X.reg formals in
   let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let modifs = Var.Set.of_option areturn in
-  (* quantify modifs, their current value will be overwritten and so does
-     not need to be saved in the freshening renaming *)
+  (* quantify modifs, their current values will be overwritten and so should
+     not be saved and restored on return *)
   let q = Sh.exists modifs q in
   (* save current values of shadowed formals and locals with a renaming *)
   let formals_freturn_locals =
     Iter.fold ~f:Var.Set.add (IArray.to_iter formals) freturn_locals
   in
-  let q', shadow = Sh.freshen q ~wrt:formals_freturn_locals in
+  let q, shadow = Sh.freshen q ~wrt:formals_freturn_locals in
   let unshadow = Var.Subst.invert shadow in
   assert (Var.Set.disjoint modifs (Var.Subst.domain shadow)) ;
   (* pass arguments by conjoining equations between formals and actuals *)
-  let entry = and_eqs shadow formals actuals q' in
+  let entry = and_eqs shadow formals actuals q in
   (* note: locals and formals are in scope *)
   assert (Var.Set.subset formals_freturn_locals ~of_:entry.us) ;
   (* simplify *)
   let entry = simplify entry in
   ( if not summaries then (entry, {areturn; unshadow; frame= Sh.emp})
   else
-    let q'', frame =
-      localize_entry globals actuals formals freturn locals shadow q' entry
+    let q, frame =
+      localize_entry globals actuals formals freturn locals shadow q entry
     in
-    (q'', {areturn; unshadow; frame}) )
+    (q, {areturn; unshadow; frame}) )
   |>
   [%Trace.retn fun {pf} (entry, {unshadow; frame}) ->
     pf "@[<v>unshadow: %a@ frame: %a@ entry: %a@]" Var.Subst.pp unshadow pp
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index e2a28d456..4b8913605 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -599,6 +599,20 @@ module Func = struct
   let iter_term func ~f = fold_cfg ~f:(fun blk () -> f blk.term) func ()
   let entry_cfg func = fold_cfg ~f:(fun blk cfg -> blk :: cfg) func []
 
+  let pp_call fs call =
+    let {callee; actuals; areturn; _} = call in
+    let {name; formals; freturn; _} = callee in
+    let pp_arg fs (actual, formal) =
+      Format.fprintf fs "@[%a / %a@]" Exp.pp actual Reg.pp formal
+    in
+    let pp_args fs (actuals, formals) =
+      IArray.pp ",@ " pp_arg fs (IArray.combine_exn actuals formals)
+    in
+    Format.fprintf fs "%a%a(@[%a@])"
+      (Option.pp "%a := " pp_arg)
+      (Option.map2 (fun a f -> (Exp.reg a, f)) areturn freturn)
+      Function.pp name pp_args (actuals, formals)
+
   let pp fs func =
     let {name; formals; freturn; entry; loc; _} = func in
     let {cmnd; term; sort_index; _} = entry in
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 9103f8ab9..de61bdaf4 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -201,6 +201,7 @@ module Func : sig
   type t = func [@@deriving compare, equal, hash]
 
   val pp : t pp
+  val pp_call : t call pp
 
   include Invariant.S with type t := t