CN: Fix free var calc for lets in Z3 SMT

Commit 2b30e70
introduced a new solver backend for CN. This code included a work-around
for Z3 (Z3Prover/z3#7268), which involved
calculating free variables for expressions. For `(let ((x term)) body)`,
the code correctly looked in `body` but did not look in `term`.

This commit fixes that, whilst tidying up some debugging and logging
code to make future debugging sessions easier.

It does not include a test because this bug was discovered during the
development of a different feature (with file `tests/cn/ptr_diff2.c`)
#494 which will be added in
separately, later.

backend/cn/bin/main.ml

@@ -306,8 +306,8 @@ let verify
   Solver.random_seed := random_seed;
   (match solver_logging with
    | Some d ->
-     Solver.log_to_temp := true;
-     Solver.log_dir := if String.equal d "" then None else Some d
+     Solver.Logger.to_file := true;
+     Solver.Logger.dir := if String.equal d "" then None else Some d
    | _ -> ());
   Solver.solver_path := solver_path;
   Solver.solver_type := solver_type;

backend/cn/lib/pp.ml

@@ -199,7 +199,7 @@ let debug l pp =
     let pp2 =
       if !print_timestamps then (
         let time = Sys.time () in
-        format [ Green ] ("[" ^ Float.to_string time ^ "] ") ^^ pp1)
+        format [ Green ] ("[" ^ Printf.sprintf "%.6f" time ^ "] ") ^^ pp1)
       else
         pp1
     in

backend/cn/lib/simple_smt.ml

@@ -544,32 +544,43 @@ let get_model s =
   | CVC5 -> ans
   | Other -> ans
   | Z3 ->
-    (* Workaround z3 bug #7270: remove `as-array` *)
+    (* Workaround for https://github.com/Z3Prover/z3/issues/7270:
+       remove `as-array` *)
     let rec drop_as_array x =
       match x with
       | Sexp.List [ _; Sexp.Atom "as-array"; f ] -> f
       | Sexp.List xs -> Sexp.List (List.map drop_as_array xs)
       | _ -> x
     in
-    (* Workaround for a z3 bug #7268: rearrange defs in dep. order *)
-    let add_binder bound x =
+    (* Workaround for https://github.com/Z3Prover/z3/issues/7268:
+       rearrange defs in dep. order *)
+    let add_binder (bound, sort_or_terms) x =
       match x with
-      | Sexp.List [ Sexp.Atom v; _ty_or_term ] -> StrSet.add v bound
+      | Sexp.List [ Sexp.Atom v; sort_or_term ] ->
+        (StrSet.add v bound, sort_or_term :: sort_or_terms)
       | _ -> raise (UnexpectedSolverResponse x)
     in
     let add_bound = List.fold_left add_binder in
     let rec free bound vars x =
       match x with
       | Sexp.Atom a -> if StrSet.mem a bound then vars else a :: vars
       | Sexp.List [ Sexp.Atom q; Sexp.List vs; body ]
-        when String.equal q "forall" || String.equal q "exist" || String.equal q "let" ->
-        free (add_bound bound vs) vars body
+        when String.equal q "forall" || String.equal q "exist" ->
+        let bound, _sorts = add_bound (bound, []) vs in
+        free bound vars body
+      | Sexp.List [ Sexp.Atom q; Sexp.List vs; body ] when String.equal q "let" ->
+        let bound_and_let_vars, terms = add_bound (bound, []) vs in
+        (* According to SMTLib spec, scoping for lets is parallel by default,
+         * so we use [bound] instead of [bound_and_let_vars] when gathering the
+         * free variables of the expressions they bind*)
+        let vars = List.fold_left (free bound) vars terms in
+        free bound_and_let_vars vars body
       | Sexp.List xs -> List.fold_left (free bound) vars xs
     in
     let check_def x =
       match x with
       | Sexp.List [ _def_fun; Sexp.Atom name; Sexp.List args; _ret; def ] ->
-        let bound = add_bound StrSet.empty args in
+        let bound, _sorts = add_bound (StrSet.empty, []) args in
         (name, free bound [] def, x)
       | _ -> raise (UnexpectedSolverResponse ans)
     in
@@ -602,7 +613,7 @@ let get_model s =
          | [] -> ()
        in
        arrange (List.map (fun (x, _, _) -> x) defs);
-       list (List.rev !decls))
+       list @@ List.rev !decls)
 
 
 (** Get the values of some s-expressions. Only valid after a [Sat] result.
@@ -819,7 +830,7 @@ type model_evaluator =
    solver, the [command] field expects an expression to evaluate, and gives the value of
    the expression in the context of the model.
 
-   XXX: This does not work correctly with data declarations, because the model does not
+   NOTE: This does not work correctly with data declarations, because the model does not
    contain those. We need to explicitly add them. *)
 let model_eval (cfg : solver_config) (m : sexp) =
   let bad () = raise (UnexpectedSolverResponse m) in

backend/cn/lib/solver.ml

@@ -95,16 +95,24 @@ type solver =
 
 module Debug = struct
   let dump_frame (f : solver_frame) =
-    let dump k _v = Printf.printf "| %s\n%!" (Sym.pp_string k) in
-    SymMap.iter dump f.uninterpreted;
-    Printf.printf "+--------------------\n%!"
+    let to_string = Sexplib.Sexp.to_string_hum in
+    let append str doc = doc ^/^ !^str in
+    let dump_sym k v rest = rest ^/^ bar ^^^ Sym.pp k ^^^ !^"|->" ^^^ !^(to_string v) in
+    let dump_bts _k v =
+      let dump k v rest = rest ^/^ bar ^^^ BT.pp k ^^^ !^"|->" ^^^ !^(to_string v) in
+      BT_Table.fold dump v
+    in
+    !^"# Symbols"
+    |> SymMap.fold dump_sym f.uninterpreted
+    |> append "# Basetypes "
+    |> Int_Table.fold dump_bts f.bt_uninterpreted
+    |> append "+---------------------------------"
 
 
-  let _dump_solver solver =
-    Printf.printf "| Start Solver Dump\n%!";
-    dump_frame !(solver.cur_frame);
-    List.iter dump_frame !(solver.prev_frames);
-    Printf.printf "| End Solver Dump\n%!"
+  let dump_solver solver =
+    !^"\n|~~~~~~ Start Solver Dump ~~~~~~~|"
+    ^/^ separate_map hardline dump_frame (!(solver.cur_frame) :: !(solver.prev_frames))
+    ^/^ !^"|~~~~~~ End Solver Dump ~~~~~~~~~|"
 end
 
 (** Lookup something in one of the existing frames *)
@@ -137,9 +145,17 @@ let get_ctype_table s =
   table
 
 
+let debug_ack_command s cmd =
+  try SMT.ack_command s.smt_solver cmd with
+  | SMT.UnexpectedSolverResponse r ->
+    debug 10 (lazy (!^"failed to ack:" ^/^ !^(Sexplib.Sexp.to_string_hum cmd)));
+    debug 10 (lazy (Debug.dump_solver s));
+    raise (SMT.UnexpectedSolverResponse r)
+
+
 (** Start a new scope. *)
 let push s =
-  SMT.ack_command s.smt_solver (SMT.push 1);
+  debug_ack_command s (SMT.push 1);
   s.prev_frames := !(s.cur_frame) :: !(s.prev_frames);
   s.cur_frame := empty_solver_frame ()
 
@@ -149,7 +165,7 @@ let pop s n =
   if n = 0 then
     ()
   else (
-    SMT.ack_command s.smt_solver (SMT.pop n);
+    debug_ack_command s (SMT.pop n);
     let rec drop count xs =
       match xs with
       | new_cur :: new_rest ->
@@ -167,7 +183,7 @@ let num_scopes s = List.length !(s.prev_frames)
 
 (** Do an ack_style command. These are logged. *)
 let ack_command s cmd =
-  SMT.ack_command s.smt_solver cmd;
+  debug_ack_command s cmd;
   let f = !(s.cur_frame) in
   f.commands <- cmd :: f.commands
 
@@ -394,7 +410,7 @@ and get_value gs ctys bt (sexp : SMT.sexp) =
   | Alloc_id -> Const (Alloc_id (CN_AllocId.from_sexp sexp))
   | CType ->
     (try Const (CType_const (Int_Table.find ctys (Z.to_int (SMT.to_z sexp)))) with
-     | _ -> Const (Default bt))
+     | Not_found -> Const (Default bt))
   | List elT ->
     (match SMT.to_con sexp with
      | con, [] when String.equal con CN_List.nil_name -> Nil elT
@@ -1019,48 +1035,50 @@ let declare_solver_basics s =
   List.iter (declare_datatype_group s) (Option.get s.globals.datatype_order)
 
 
-(** Logging *)
+(* Logging *)
 
-let log_to_temp = ref false (* Should we log to file *)
+module Logger = struct
+  let to_file = ref false
 
-let log_results = ref false (* Do we also want reposnses*)
+  (** NOTE: this interferes with line numbers *)
+  let include_solver_responses = ref false
 
-let log_dir = ref (None : string option) (* Log to this dir *)
+  let dir = ref (None : string option)
 
-let log_counter = ref 0 (* Names of SMT files *)
+  let log_counter = ref 0 (* Names of SMT files *)
 
-(** Pick a logger based on the above settings *)
-let logger lab =
-  let log_id = !log_counter in
-  log_counter := log_id + 1;
-  let get_file suf =
-    let dir =
-      match !log_dir with
-      | Some dir -> dir
-      | None ->
-        let nm = Printf.sprintf "cn_%.3f" (Unix.gettimeofday ()) in
-        let d = Filename.concat (Filename.get_temp_dir_name ()) nm in
-        log_dir := Some d;
-        d
+  (** Pick a logger based on the above settings *)
+  let make prefix =
+    let log_id = !log_counter in
+    log_counter := log_id + 1;
+    let get_file suf =
+      let dir =
+        match !dir with
+        | Some dir -> dir
+        | None ->
+          let nm = Printf.sprintf "cn_%.3f" (Unix.gettimeofday ()) in
+          let d = Filename.concat (Filename.get_temp_dir_name ()) nm in
+          dir := Some d;
+          d
+      in
+      if not (Sys.file_exists dir) then Sys.mkdir dir 0o700 else ();
+      open_out (Filename.concat dir (prefix ^ suf ^ string_of_int log_id ^ ".smt"))
     in
-    if not (Sys.file_exists dir) then Sys.mkdir dir 0o700 else ();
-    open_out (Filename.concat dir (lab ^ suf ^ string_of_int log_id ^ ".smt"))
-  in
-  if !log_to_temp then (
-    let out = get_file "_send_" in
-    if !log_results then
-      { SMT.send = Printf.fprintf out "[->] %s\n%!";
-        SMT.receive = Printf.fprintf out "[<-] %s\n%!";
-        SMT.stop = (fun _ -> close_out out)
-      }
+    if !to_file then (
+      let out = get_file "_send_" in
+      if !include_solver_responses then
+        { SMT.send = Printf.fprintf out "[->] %s\n%!";
+          SMT.receive = Printf.fprintf out "[<-] %s\n%!";
+          SMT.stop = (fun _ -> close_out out)
+        }
+      else
+        { SMT.send = Printf.fprintf out "%s\n%!";
+          SMT.receive = (fun _ -> ());
+          SMT.stop = (fun _ -> close_out out)
+        })
     else
-      { SMT.send = Printf.fprintf out "%s\n%!";
-        SMT.receive = (fun _ -> ());
-        SMT.stop = (fun _ -> close_out out)
-      })
-  else
-    { SMT.send = (fun _ -> ()); SMT.receive = (fun _ -> ()); SMT.stop = (fun _ -> ()) }
-
+      { SMT.send = (fun _ -> ()); SMT.receive = (fun _ -> ()); SMT.stop = (fun _ -> ()) }
+end
 
 let solver_path = ref (None : string option)
 
@@ -1092,7 +1110,7 @@ let make globals =
   cfg
   := { !cfg with
        log =
-         logger
+         Logger.make
            (match !cfg.exts with
             | SMT.Z3 -> "z3"
             | SMT.CVC5 -> "cvc5"
@@ -1112,12 +1130,11 @@ let make globals =
 
 (** Evaluate terms in the context of a model computed by the solver. *)
 let model_evaluator solver mo =
-  (* match None with | None -> fun _ -> None | _ -> *)
   match SMT.to_list mo with
   | None -> failwith "model is an atom"
   | Some defs ->
     let scfg = solver.smt_solver.config in
-    let cfg = { scfg with log = logger "model" } in
+    let cfg = { scfg with log = Logger.make "model" } in
     let s = SMT.new_solver cfg in
     let gs = solver.globals in
     let evaluator =
@@ -1133,7 +1150,7 @@ let model_evaluator solver mo =
       }
     in
     declare_solver_basics evaluator;
-    List.iter (SMT.ack_command s) defs;
+    List.iter (debug_ack_command evaluator) defs;
     fun e ->
       push evaluator;
       let inp = translate_term evaluator e in
@@ -1188,19 +1205,19 @@ let provable ~loc ~solver ~global ~assumptions ~simp_ctxt lc =
     in
     let nlc = SMT.bool_not expr in
     let inc = s1.smt_solver in
-    SMT.ack_command inc (SMT.push 1);
-    SMT.ack_command inc (SMT.assume (SMT.bool_ands (nlc :: extra)));
+    debug_ack_command s1 (SMT.push 1);
+    debug_ack_command s1 (SMT.assume (SMT.bool_ands (nlc :: extra)));
     let res = SMT.check inc in
     (match res with
      | SMT.Unsat ->
-       SMT.ack_command inc (SMT.pop 1);
+       debug_ack_command s1 (SMT.pop 1);
        rtrue ()
      | SMT.Sat ->
        model_from inc;
-       SMT.ack_command inc (SMT.pop 1);
+       debug_ack_command s1 (SMT.pop 1);
        `False
      | SMT.Unknown ->
-       SMT.ack_command inc (SMT.pop 1);
+       debug_ack_command s1 (SMT.pop 1);
        failwith "Unknown")
 
 

backend/cn/lib/solver.mli

@@ -13,9 +13,11 @@ val empty_model : model
    maybe) *)
 val random_seed : int ref
 
-val log_to_temp : bool ref
+module Logger : sig
+  val to_file : bool ref
 
-val log_dir : string option ref
+  val dir : string option ref
+end
 
 val solver_path : string option ref