SMT: Add reals and strings to SMT backend

Jib_compile now has an option that lets it generate real value
literals (VL_real), which we don't want for backends (i.e. C), which
don't support them. Reals are encoded as actual reals in SMT, as there
isn't really any nice way to encode them as bitvectors. Currently we
just have the pure real functions, functions between integers and
reals (i.e. floor, to_real, etc) are not supported for now.

Strings are likewise encoded as SMTLIB strings, for similar reasons.

Jib_smt has ctx.use_real and ctx.use_string which are set when we
generate anything real or string related, so we can keep the logic as
Arrays+Bitvectors for most Sail that doesn't require either.

7 files changed, 98 insertions, 29 deletions

diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index ad60d224..f8cb3bcd 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -160,7 +160,8 @@ type ctx =
     optimize_anf : ctx -> typ aexp -> typ aexp;
     specialize_calls : bool;
     ignore_64 : bool;
-    struct_value : bool
+    struct_value : bool;
+    use_real : bool;
   }
 
 let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env =
@@ -176,7 +177,8 @@ let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env =
     optimize_anf = optimize_anf;
     specialize_calls = false;
     ignore_64 = false;
-    struct_value = false
+    struct_value = false;
+    use_real = false;
   }
 
 let ctyp_of_typ ctx typ = ctx.convert_typ ctx typ
@@ -232,10 +234,13 @@ let rec compile_aval l ctx = function
   | AV_lit (L_aux (L_false, _), _) -> [], V_lit (VL_bool false, CT_bool), []
 
   | AV_lit (L_aux (L_real str, _), _) ->
-     let gs = ngensym () in
-     [iinit CT_real gs (V_lit (VL_string str, CT_string))],
-     V_id (gs, CT_real),
-     [iclear CT_real gs]
+     if ctx.use_real then
+       [], V_lit (VL_real str, CT_real), []
+     else
+       let gs = ngensym () in
+       [iinit CT_real gs (V_lit (VL_string str, CT_string))],
+       V_id (gs, CT_real),
+       [iclear CT_real gs]
 
   | AV_lit (L_aux (L_unit, _), _) -> [], V_lit (VL_unit, CT_unit), []
 
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index b882f2f9..70a0b322 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -96,7 +96,9 @@ type ctx =
        be ignored. *)
     ignore_64 : bool;
     (** If false (default) we won't generate any V_struct values *)
-    struct_value : bool
+    struct_value : bool;
+    (** Allow real literals *)
+    use_real : bool;
   }
 
 val initial_ctx :
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 99938365..c03b8934 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -92,6 +92,9 @@ type ctx = {
        the global path conditional of the containing block in the
        control flow graph *)
     pathcond : smt_exp;
+    (* Set if we need to use strings *)
+    use_string : bool ref;
+    use_real : bool ref
   }
 
 (* These give the default bounds for various SMT types, stored in the
@@ -114,6 +117,8 @@ let initial_ctx () = {
     ast = Defs [];
     events = ref EventMap.empty;
     pathcond = Bool_lit true;
+    use_string = ref false;
+    use_real = ref false;
   }
 
 let event_stack ctx ev =
@@ -162,7 +167,12 @@ let rec smt_ctyp ctx = function
      ctx.tuple_sizes := IntSet.add (List.length ctyps) !(ctx.tuple_sizes);
      Tuple (List.map (smt_ctyp ctx) ctyps)
   | CT_vector (_, ctyp) -> Array (Bitvec !vector_index, smt_ctyp ctx ctyp)
-  | CT_string -> Bitvec 64
+  | CT_string ->
+     ctx.use_string := true;
+     String
+  | CT_real ->
+     ctx.use_real := true;
+     Real
   | CT_ref ctyp ->
      begin match CTMap.find_opt ctyp ctx.register_map with
      | Some regs -> Bitvec (required_width (Big_int.of_int (List.length regs)))
@@ -231,8 +241,16 @@ let smt_value ctx vl ctyp =
   | VL_bit Sail2_values.B0, CT_bit -> Bin "0"
   | VL_bit Sail2_values.B1, CT_bit -> Bin "1"
   | VL_unit, _ -> Var "unit"
-  | VL_string _, _ -> Var "unit" (* FIXME: String support *)
-  | vl, _ -> failwith ("Cannot translate literal to SMT " ^ string_of_value vl)
+  | VL_string str, _ ->
+     ctx.use_string := true;
+     String_lit (String.escaped str)
+  | VL_real str, _ ->
+     ctx.use_real := true;
+     if str.[0] = '-' then
+       Fn ("-", [Real_lit (String.sub str 1 (String.length str - 1))])
+     else
+       Real_lit str
+  | vl, _ -> failwith ("Cannot translate literal to SMT: " ^ string_of_value vl)
 
 let zencode_ctor ctor_id unifiers =
   match unifiers with
@@ -883,9 +901,18 @@ let builtin_compare_bits fn ctx v1 v2 ret_ctyp =
 
   | _ -> builtin_type_error ctx fn [v1; v2] (Some ret_ctyp)
 
+(* ***** Real number operations: lib/real.sail ***** *)
+
+let builtin_sqrt_real ctx root v =
+  ctx.use_real := true;
+  let smt = smt_cval ctx v in
+  [Declare_const (root, Real);
+   Assert (Fn ("and", [Fn ("=", [smt; Fn ("*", [Var root; Var root])]);
+                       Fn (">=", [Var root; Real_lit "0.0"])]))]
+
 let smt_builtin ctx name args ret_ctyp =
   match name, args, ret_ctyp with
-  | "eq_bits", [v1; v2], _ -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+  | "eq_bits", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
   | "eq_anything", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
 
   (* lib/flow.sail *)
@@ -954,6 +981,23 @@ let smt_builtin ctx name args ret_ctyp =
   | "get_slice_int", [v1; v2; v3], ret_ctyp -> builtin_get_slice_int ctx v1 v2 v3 ret_ctyp
   | "set_slice", [v1; v2; v3; v4; v5], ret_ctyp -> builtin_set_slice_bits ctx v1 v2 v3 v4 v5 ret_ctyp
 
+  (* string builtins *)
+  | "concat_str", [v1; v2], CT_string -> ctx.use_string := true; Fn ("str.++", [smt_cval ctx v1; smt_cval ctx v2])
+  | "eq_string", [v1; v2], CT_bool -> ctx.use_string := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+
+  (* lib/real.sail *)
+  (* Note that sqrt_real is special and is handled by smt_instr. *)
+  | "eq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+  | "neg_real", [v], CT_real -> ctx.use_real := true; Fn ("-", [smt_cval ctx v])
+  | "add_real",  [v1; v2], CT_real -> ctx.use_real := true; Fn ("+", [smt_cval ctx v1; smt_cval ctx v2])
+  | "sub_real",  [v1; v2], CT_real -> ctx.use_real := true; Fn ("-", [smt_cval ctx v1; smt_cval ctx v2])
+  | "mult_real", [v1; v2], CT_real -> ctx.use_real := true; Fn ("*", [smt_cval ctx v1; smt_cval ctx v2])
+  | "div_real",  [v1; v2], CT_real -> ctx.use_real := true; Fn ("/", [smt_cval ctx v1; smt_cval ctx v2])
+  | "lt_real",   [v1; v2], CT_bool -> ctx.use_real := true; Fn ("<", [smt_cval ctx v1; smt_cval ctx v2])
+  | "gt_real",   [v1; v2], CT_bool -> ctx.use_real := true; Fn (">", [smt_cval ctx v1; smt_cval ctx v2])
+  | "lteq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn ("<=", [smt_cval ctx v1; smt_cval ctx v2])
+  | "gteq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn (">=", [smt_cval ctx v1; smt_cval ctx v2])
+
   | _ -> failwith ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp)
 
 let rec smt_conversion ctx from_ctyp to_ctyp x =
@@ -1288,8 +1332,15 @@ let smt_instr ctx =
   | I_aux (I_funcall (CL_id (id, ret_ctyp), extern, function_id, args), (_, l)) ->
      if Env.is_extern function_id ctx.tc_env "c" && not extern then
        let name = Env.get_extern function_id ctx.tc_env "c" in
-       let value = smt_builtin ctx name args ret_ctyp in
-       [define_const ctx id ret_ctyp value]
+       if name = "sqrt_real" then
+         begin match args with
+         | [v] -> builtin_sqrt_real ctx (zencode_name id) v
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for sqrt_real"
+         end
+       else
+         let value = smt_builtin ctx name args ret_ctyp in
+         [define_const ctx id ret_ctyp value]
      else if extern && string_of_id function_id = "internal_vector_init" then
        [declare_const ctx id ret_ctyp]
      else if extern && string_of_id function_id = "internal_vector_update" then
@@ -1360,6 +1411,10 @@ let smt_instr ctx =
 
   | I_aux (I_undefined ctyp, _) -> []
 
+  (* I_jump and I_goto will only appear as terminators for basic blocks. *)
+  | I_aux ((I_jump _ | I_goto _), _) -> []
+
+
   | instr ->
      failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr))
 
@@ -1404,7 +1459,7 @@ let optimize_smt stack =
        | Some n -> Hashtbl.replace uses var (n + 1)
        | None -> Hashtbl.add uses var 1
        end
-    | Hex _ | Bin _ | Bool_lit _ -> ()
+    | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
     | Fn (f, exps) ->
        List.iter uses_in_exp exps
     | Ite (cond, t, e) ->
@@ -1613,7 +1668,11 @@ let smt_cdef props lets name_file ctx all_cdefs = function
         let out_chan = open_out fname in
         if prop_type = "counterexample" then
           output_string out_chan "(set-option :produce-models true)\n";
-        output_string out_chan "(set-logic QF_AUFBVDT)\n";
+
+        if !(ctx.use_string) || !(ctx.use_real) then
+          output_string out_chan "(set-logic ALL)\n"
+        else
+          output_string out_chan "(set-logic QF_AUFBVDT)\n";
 
         List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") (smt_header ctx all_cdefs);
 
@@ -1679,7 +1738,7 @@ let generate_smt props name_file env ast =
           env
       in
       let t = Profile.start () in
-      let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true; struct_value = true } ast in
+      let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true; struct_value = true; use_real = true } ast in
       Profile.finish "Compiling to Jib IR" t;
       cdefs
     in
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index c8027ee5..9a9a3361 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -125,7 +125,7 @@ let reachable roots graph =
   IntSet.iter reachable' roots; !visited
 
 exception Not_a_DAG of int;;
-  
+
 let topsort graph =
   let marked = ref IntSet.empty in
   let temp_marked = ref IntSet.empty in
@@ -193,6 +193,7 @@ type cf_node =
   | CF_guard of cval
   | CF_start of ctyp NameMap.t
 
+(* For now we only generate CFGs for flat lists of instructions *)
 let control_flow_graph instrs =
   let module StringMap = Map.Make(String) in
   let labels = ref StringMap.empty in
@@ -215,7 +216,7 @@ let control_flow_graph instrs =
   let rec cfg preds instrs =
     let before, after = instr_split_at cf_split instrs in
     let last = match after with
-      | I_aux ((I_label _ | I_goto _ | I_jump _), _) :: _ -> []
+      | I_aux (I_label _, _) :: _ -> []
       | instr :: _ -> [instr]
       | _ -> []
     in
@@ -227,11 +228,6 @@ let control_flow_graph instrs =
          [n]
     in
     match after with
-    | I_aux (I_if (cond, then_instrs, else_instrs, _), _) :: after ->
-       let t = cfg preds then_instrs in
-       let e = cfg preds else_instrs in
-       cfg (t @ e) after
-
     | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after ->
        cfg [] after
 
@@ -249,11 +245,8 @@ let control_flow_graph instrs =
     | I_aux (I_label label, _) :: after ->
        cfg (StringMap.find label !labels :: preds) after
 
-    | I_aux (I_block instrs, _) :: after ->
-       let m = cfg preds instrs in
-       cfg m after
-
-    | _ :: after -> assert false
+    | I_aux (_, (_, l)) :: after ->
+       Reporting.unreachable l __POS__ "Could not add instruction to control-flow graph"
 
     | [] -> preds
   in
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index c98c325c..378f5fae 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -259,6 +259,7 @@ let string_of_value = function
   | VL_bit Sail2_values.B0 -> "UINT64_C(0)"
   | VL_bit Sail2_values.B1 -> "UINT64_C(1)"
   | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
+  | VL_real str -> str
   | VL_string str -> "\"" ^ str ^ "\""
 
 let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 72421b8a..7f485447 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -54,6 +54,8 @@ open Ast_util
 type smt_typ =
   | Bitvec of int
   | Bool
+  | String
+  | Real
   | Datatype of string * (string * (string * smt_typ) list) list
   | Tuple of smt_typ list
   | Array of smt_typ * smt_typ
@@ -89,6 +91,8 @@ type smt_exp =
   | Bool_lit of bool
   | Hex of string
   | Bin of string
+  | Real_lit of string
+  | String_lit of string
   | Var of string
   | Fn of string * smt_exp list
   | Ite of smt_exp * smt_exp * smt_exp
@@ -145,7 +149,7 @@ let rec simp_smt_exp vars = function
      | Some exp -> simp_smt_exp vars exp
      | None -> Var v
      end
-  | (Hex _ | Bin _ | Bool_lit _ as exp) -> exp
+  | (Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
   | Fn (f, exps) ->
      let exps = List.map (simp_smt_exp vars) exps in
      simp_fn (Fn (f, exps))
@@ -184,6 +188,8 @@ let rec pp_smt_exp =
   let open PPrint in
   function
   | Bool_lit b -> string (string_of_bool b)
+  | Real_lit str -> string str
+  | String_lit str -> string ("\"" ^ str ^ "\"")
   | Hex str -> string ("#x" ^ str)
   | Bin str -> string ("#b" ^ str)
   | Var str -> string str
@@ -201,6 +207,8 @@ let rec pp_smt_typ =
   let open PPrint in
   function
   | Bool -> string "Bool"
+  | String -> string "String"
+  | Real -> string "Real"
   | Bitvec n -> string (Printf.sprintf "(_ BitVec %d)" n)
   | Datatype (name, _) -> string name
   | Tuple tys -> pp_sfun ("Tup" ^ string_of_int (List.length tys)) (List.map pp_smt_typ tys)
diff --git a/src/value2.lem b/src/value2.lem
index 0e65e91f..0afaa2d1 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -59,4 +59,5 @@ type vl =
   | VL_unit
   | VL_int of integer
   | VL_string of string
+  | VL_real of string
   | VL_null (* Used for unitialized values and null pointers in C compilation *)