Fixes #435 and #395: SMT backend crashes

backend/cn/lib/simple_smt.ml

@@ -630,6 +630,40 @@ let get_expr s v : sexp =
   | _ -> raise (UnexpectedSolverResponse res)
 
 
+let is_let (exp : sexp) : (sexp StrMap.t * sexp) option =
+  match exp with
+  | Sexp.List [ Sexp.Atom "let"; Sexp.List binds; body ] ->
+    let add_bind mp bind =
+      match bind with
+      | Sexp.List [ Sexp.Atom x; y ] -> StrMap.add x y mp
+      | _ -> raise (UnexpectedSolverResponse bind)
+    in
+    let su = List.fold_left add_bind StrMap.empty binds in
+    Some (su, body)
+  | _ -> None
+
+
+(** Expand let-definitions in this term.
+    NOTE: this is intended to be used mostly on models generated by the
+    solver (e.g., `get-value` in Z3 sometimes contains `let`).  As such
+    we assume that `forall` and `exist` won't occur, and so we don't need
+    to check for variable capture. *)
+let no_let (exp0 : sexp) : sexp =
+  let rec expand su exp =
+    match is_let exp with
+    | Some (binds, body) ->
+      let binds1 = StrMap.map (expand su) binds in
+      let jn _ x _ = Some x in
+      let su1 = StrMap.union jn binds1 su in
+      expand su1 body
+    | None ->
+      (match exp with
+       | Sexp.List xs -> Sexp.List (List.map (expand su) xs)
+       | Sexp.Atom x -> (match StrMap.find_opt x su with Some e1 -> e1 | None -> exp))
+  in
+  expand StrMap.empty exp0
+
+
 (** Try to decode an s-expression as a boolean
     Throws {!UnexpectedSolverResponse}. *)
 let to_bool (exp : sexp) =

backend/cn/lib/solver.ml

@@ -988,12 +988,16 @@ let rec declare_struct s done_struct name decl =
   else (
     done_struct := SymSet.add name mp;
     let mk_field (l, t) =
+      let rec declare_nested ty =
+        match ty with
+        | Struct name' ->
+          let decl = SymMap.find name' s.globals.struct_decls in
+          declare_struct s done_struct name' decl
+        | Map (_, el) -> declare_nested el
+        | _ -> ()
+      in
       let ty = Memory.bt_of_sct t in
-      (match ty with
-       | Struct name' ->
-         let decl = SymMap.find name' s.globals.struct_decls in
-         declare_struct s done_struct name' decl
-       | _ -> ());
+      declare_nested ty;
       (CN_Names.struct_field_name l, translate_base_type ty)
     in
     let mk_piece (x : Memory.struct_piece) = Option.map mk_field x.member_or_padding in
@@ -1142,7 +1146,7 @@ let model_evaluator solver mo =
          let res = SMT.get_expr s inp in
          pop evaluator 1;
          let ctys = get_ctype_table evaluator in
-         Some (get_ivalue gs ctys (basetype e) res)
+         Some (get_ivalue gs ctys (basetype e) (SMT.no_let res))
        | _ ->
          pop evaluator 1;
          None)