SMT: Fix an issue with tuple to struct conversion

src/lib/jib_compile.ml

@@ -266,7 +266,7 @@ module type CONFIG = sig
   val convert_typ : ctx -> typ -> ctyp
   val optimize_anf : ctx -> typ aexp -> typ aexp
   val unroll_loops : int option
-  val make_call_precise : ctx -> id -> bool
+  val make_call_precise : ctx -> id -> ctyp list -> ctyp -> bool
   val ignore_64 : bool
   val struct_value : bool
   val tuple_value : bool
@@ -2137,7 +2137,7 @@ module Make (C : CONFIG) = struct
                   Reporting.unreachable (id_loc id) __POS__ "Invalid cons call"
             end
           | None -> instr :: tail
-          | Some (param_ctyps, ret_ctyp) when C.make_call_precise ctx id ->
+          | Some (param_ctyps, ret_ctyp) when C.make_call_precise ctx id param_ctyps ret_ctyp ->
               if List.compare_lengths args param_ctyps <> 0 then
                 Reporting.unreachable (id_loc id) __POS__
                   ("Function call found with incorrect arity: " ^ string_of_id id);

src/lib/jib_compile.mli

@@ -145,7 +145,7 @@ module type CONFIG = sig
   (** A call is precise if the function arguments match the function
       type exactly. Leaving functions imprecise can allow later passes
       to specialize implementations. *)
-  val make_call_precise : ctx -> id -> bool
+  val make_call_precise : ctx -> id -> ctyp list -> ctyp -> bool
 
   (** If false, will ensure that fixed size bitvectors are
        specifically less that 64-bits. If true this restriction will

src/lib/jib_util.mli

@@ -144,6 +144,7 @@ val full_string_of_ctyp : ctyp -> string
 (** {1. Functions and modules for working with ctyps} *)
 
 val map_ctyp : (ctyp -> ctyp) -> ctyp -> ctyp
+val ctyp_has : (ctyp -> bool) -> ctyp -> bool
 val ctyp_equal : ctyp -> ctyp -> bool
 val ctyp_compare : ctyp -> ctyp -> int
 

src/sail_c_backend/c_backend.ml

@@ -586,7 +586,7 @@ end) : CONFIG = struct
   let optimize_anf ctx aexp = analyze_functions ctx analyze_primop (c_literals ctx aexp)
 
   let unroll_loops = None
-  let make_call_precise _ _ = true
+  let make_call_precise _ _ _ _ = true
   let ignore_64 = false
   let struct_value = false
   let tuple_value = false

src/sail_smt_backend/jib_smt.ml

@@ -1272,7 +1272,16 @@ end) : Jib_compile.CONFIG = struct
 
   let optimize_anf ctx aexp = aexp |> analyze ctx |> smt_literals ctx |> fold_aexp (unroll_static_foreach ctx)
 
-  let make_call_precise _ _ = false
+  (* If a function has a tuple anywhere in its argument or return
+     types we must convert to the exact tuple type expected by the
+     function, otherwise after the tuple to struct conversion we won't
+     be able to apply the right conversions at the SMT level, as the
+     structural tuple types become different nominal struct types we
+     can't convert between. See issue 683 for an example. *)
+  let make_call_precise _ _ param_ctyps ret_ctyp =
+    let has_tuple = ctyp_has (function CT_tup _ -> true | _ -> false) in
+    List.exists has_tuple param_ctyps || has_tuple ret_ctyp
+
   let ignore_64 = true
   let unroll_loops = Some Opts.unroll_limit
   let struct_value = true

src/sail_sv_backend/sail_plugin_sv.ml

@@ -319,7 +319,7 @@ module Verilog_config (C : JIB_CONFIG) : Jib_compile.CONFIG = struct
 
   let unroll_loops = Some 64
   let specialize_calls = false
-  let make_call_precise = C.make_call_precise
+  let make_call_precise ctx id _ _ = C.make_call_precise ctx id
   let ignore_64 = true
   let struct_value = false
   let tuple_value = false

test/smt/option_tuple_i683.unsat.sail

@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+$include <option.sail>
+
+$include <option.sail>
+
+$property
+function prop() -> bool = {
+  match Some(0, 0) {
+    None() => true,
+    Some(a, b) => a == b
+  }
+}