Refactor Sail->SMT backend and rework Sail->SV to share code (#580)

* Refactor Sail->SMT backend and rework Sail->SV to share code

This commit reworks the Sail->SMT backend to use the new shared primtive generation logic
that Sail->SV uses. Various older features have been removed to simplify the code.

The Sail->SV backend has been refactored to use modules rather than just functions, but this
has left it in quite the broken state for the time being.

There are a few known issues with the Sail->SMT pipeline that pre-date this commit,
for example function arguments with complex constraints are sometimes generalised,
and we would require additional well-formedness checks to be inserted to guard against
this. There is now a small test that demonstrates the lack of these well-formedness
checks in Sail->SMT

Fix path condition computation to use post-dominators in order to handle
cases where the graph has some non-structured control flow

* Add pure if-then-else optimization to Sail->SMT

aarch64_small/armV8_A64_sys_regs.sail

@@ -176,7 +176,7 @@ register SCTLR_EL3 : SCTLR_type /* System Control Register (EL3) */
 
 
 /* CP: added coercion from SCTLR_EL1_type to SCTLR_type for the SCTLR function */
-val cast "SCTLR_EL1_type_to_SCTLR_type" : SCTLR_EL1_type -> SCTLR_type
+val "SCTLR_EL1_type_to_SCTLR_type" : SCTLR_EL1_type -> SCTLR_type
 
 bitfield TCR_EL1_type : bits(64) =
 {

aarch64_small/prelude.sail

@@ -59,17 +59,14 @@ function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
 val pow2_atom = "pow2" : forall 'n. int('n) -> int(2 ^ 'n)
 val pow2_int = "pow2" : int -> int
 
-overload pow2 = {pow2_atom, pow2_int}
-
-
-val cast cast_bool_bit : bool -> bit
+val cast_bool_bit : bool -> bit
 function cast_bool_bit(b) = 
   match b {
     true => b1,
     false => b0
   }
 
-val cast cast_bit_bool : bit -> bool
+val cast_bit_bool : bit -> bool
 function cast_bit_bool (b) = 
   match b {
     bitzero => false,

language/jib.ott

@@ -72,11 +72,16 @@ type iannot = int * ocaml_l
 
 grammar
 
+chan :: 'Chan_' ::=
+  | stdout :: :: stdout
+  | stderr :: :: stderr
+
 name :: '' ::=
   | id nat                :: :: name
   | have_exception nat    :: :: have_exception
   | current_exception nat :: :: current_exception
   | throw_location nat    :: :: throw_location
+  | channel chan nat      :: :: channel
   | return nat            :: :: return
 
 op :: '' ::=
@@ -88,6 +93,7 @@ op :: '' ::=
   | is_empty          :: :: list_is_empty
   | eq                :: :: eq
   | neq               :: :: neq
+  | ite               :: :: ite
 % Integer ops
   | lt                :: :: ilt
   | lteq              :: :: ilteq
@@ -121,6 +127,7 @@ uid :: 'UId_' ::=
 
 cval :: 'V_' ::=
   | name : ctyp                                     :: :: id
+  | id : ctyp                                       :: :: member
   | value : ctyp                                    :: :: lit
   | ( cval0 , ... , cvaln ) ctyp                    :: :: tuple
   | struct { id0 = cval0 , ... , idn = cvaln } ctyp :: :: struct
@@ -205,6 +212,10 @@ iannot :: '' ::=
   {{ lem iannot }}
   {{ ocaml iannot }}
 
+creturn :: 'CR_' ::=
+  | clexp                     :: :: one
+  | ( clexp0 , ... , clexpn ) :: :: multi
+
 instr :: 'I_' ::=
   {{ aux _ iannot }}
 % The following are the minimal set of instructions output by
@@ -214,7 +225,7 @@ instr :: 'I_' ::=
   | jump ( cval ) string                           :: :: jump
   | goto string                                    :: :: goto
   | string :                                       :: :: label
-  | clexp = bool uid ( cval0 , ... , cvaln )       :: :: funcall
+  | creturn = bool uid ( cval0 , ... , cvaln )     :: :: funcall
   | clexp = cval                                   :: :: copy
   | clear ctyp name                                :: :: clear
   | undefined ctyp                                 :: :: undefined

lib/sv/sail.sv

@@ -33,10 +33,6 @@ function automatic bit sail_eq_string(sail_unit s1, sail_unit s2);
    return 0;
 endfunction
 
-function automatic sail_unit sail_concat_str(sail_unit s1, sail_unit s2);
-   return SAIL_UNIT;
-endfunction
-
 `else
 
 function automatic sail_unit sail_print_endline(string s);
@@ -70,10 +66,6 @@ function automatic bit sail_eq_string(string s1, string s2);
    return s1 == s2;
 endfunction
 
-function automatic string sail_concat_str(string s1, string s2);
-   return {s1, s2};
-endfunction
-
 `endif
 
 typedef enum logic [0:0] {SAIL_REAL} sail_real;

src/lib/ast_util.mli

@@ -383,7 +383,7 @@ module Typ : sig
 end
 
 module IdSet : sig
-  include Set.S with type elt = id
+  include Set.S with type elt = id and type t = Set.Make(Id).t
 end
 
 module NexpSet : sig

src/lib/jib_compile.ml

@@ -258,6 +258,7 @@ module type CONFIG = sig
   val use_real : bool
   val branch_coverage : out_channel option
   val track_throw : bool
+  val use_void : bool
 end
 
 module IdGraph = Graph.Make (Id)
@@ -361,6 +362,7 @@ module Make (C : CONFIG) = struct
           ([iinit l ctyp' gs cval], V_id (gs, ctyp'), [iclear ctyp' gs])
         )
         else ([], cval, [])
+    | AV_id (id, Enum typ) -> ([], V_member (id, ctyp_of_typ ctx typ), [])
     | AV_id (id, typ) -> begin
         match Bindings.find_opt id ctx.locals with
         | Some (_, ctyp) -> ([], V_id (name id, ctyp), [])
@@ -635,7 +637,7 @@ module Make (C : CONFIG) = struct
     | AP_id (pid, _) when is_ct_enum ctyp -> begin
         match Env.lookup_id pid ctx.tc_env with
         | Unbound _ -> ([], [idecl l ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx)
-        | _ -> ([ijump l (V_call (Neq, [V_id (name pid, ctyp); cval])) case_label], [], [], ctx)
+        | _ -> ([ijump l (V_call (Neq, [V_member (pid, ctyp); cval])) case_label], [], [], ctx)
       end
     | AP_id (pid, typ) ->
         let id_ctyp = ctyp_of_typ ctx typ in
@@ -871,19 +873,36 @@ module Make (C : CONFIG) = struct
         else if is_dead_aexp else_aexp then compile_aexp ctx then_aexp
         else (
           let if_ctyp = ctyp_of_typ ctx if_typ in
-          let branch_id, on_reached = coverage_branch_reached ctx l in
-          let compile_branch aexp =
-            let setup, call, cleanup = compile_aexp ctx aexp in
-            fun clexp -> coverage_branch_target_taken ctx branch_id aexp @ setup @ [call clexp] @ cleanup
-          in
           let setup, cval, cleanup = compile_aval l ctx aval in
-          ( setup,
-            (fun clexp ->
-              append_into_block on_reached
-                (iif l cval (compile_branch then_aexp clexp) (compile_branch else_aexp clexp) if_ctyp)
-            ),
-            cleanup
-          )
+          match get_attribute "anf_pure" uannot with
+          | Some _ ->
+              let then_gs = ngensym () in
+              let then_setup, then_call, then_cleanup = compile_aexp ctx then_aexp in
+              let else_gs = ngensym () in
+              let else_setup, else_call, else_cleanup = compile_aexp ctx else_aexp in
+              ( setup @ then_setup @ else_setup
+                @ [
+                    idecl l if_ctyp then_gs;
+                    idecl l if_ctyp else_gs;
+                    then_call (CL_id (then_gs, if_ctyp));
+                    else_call (CL_id (else_gs, if_ctyp));
+                  ],
+                (fun clexp -> icopy l clexp (V_call (Ite, [cval; V_id (then_gs, if_ctyp); V_id (else_gs, if_ctyp)]))),
+                [iclear if_ctyp else_gs; iclear if_ctyp then_gs] @ else_cleanup @ then_cleanup @ cleanup
+              )
+          | None ->
+              let branch_id, on_reached = coverage_branch_reached ctx l in
+              let compile_branch aexp =
+                let setup, call, cleanup = compile_aexp ctx aexp in
+                fun clexp -> coverage_branch_target_taken ctx branch_id aexp @ setup @ [call clexp] @ cleanup
+              in
+              ( setup,
+                (fun clexp ->
+                  append_into_block on_reached
+                    (iif l cval (compile_branch then_aexp clexp) (compile_branch else_aexp clexp) if_ctyp)
+                ),
+                cleanup
+              )
         )
     (* FIXME: AE_struct_update could be AV_record_update - would reduce some copying. *)
     | AE_struct_update (aval, fields, typ) ->
@@ -1132,8 +1151,11 @@ module Make (C : CONFIG) = struct
     | (AE_aux (_, { loc = l; _ }) as exp) :: exps ->
         let setup, call, cleanup = compile_aexp ctx exp in
         let rest = compile_block ctx exps in
-        let gs = ngensym () in
-        iblock (setup @ [idecl l CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest
+        if C.use_void then iblock (setup @ [call CL_void] @ cleanup) :: rest
+        else (
+          let gs = ngensym () in
+          iblock (setup @ [idecl l CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest
+        )
 
   let fast_int = function CT_lint when !optimize_aarch64_fast_struct -> CT_fint 64 | ctyp -> ctyp
 
@@ -1825,7 +1847,7 @@ module Make (C : CONFIG) = struct
 
   let rec specialize_variants ctx prior =
     let instantiations = ref CTListSet.empty in
-    let fix_variants ctx var_id = visit_ctyp (new fix_variants_visitor ctx var_id) in
+    let fix_variants ctx var_id = visit_ctyp (new fix_variants_visitor ctx var_id :> common_visitor) in
 
     let specialize_constructor ctx ctor_id =
       visit_cdefs (new specialize_constructor_visitor instantiations ctx ctor_id)
@@ -1995,7 +2017,7 @@ module Make (C : CONFIG) = struct
 
     let precise_call call tail =
       match call with
-      | I_aux (I_funcall (clexp, extern, (id, ctyp_args), args), ((_, l) as aux)) as instr -> begin
+      | I_aux (I_funcall (CR_one clexp, extern, (id, ctyp_args), args), ((_, l) as aux)) as instr -> begin
           match get_function_typ id with
           | None when string_of_id id = "sail_cons" -> begin
               match (ctyp_args, args) with
@@ -2007,7 +2029,9 @@ module Make (C : CONFIG) = struct
                     [
                       iblock
                         (cast
-                        @ [I_aux (I_funcall (clexp, extern, (id, ctyp_args), [V_id (gs, ctyp_arg); tl_arg]), aux)]
+                        @ [
+                            I_aux (I_funcall (CR_one clexp, extern, (id, ctyp_args), [V_id (gs, ctyp_arg); tl_arg]), aux);
+                          ]
                         @ tail @ cleanup
                         );
                     ]
@@ -2051,7 +2075,7 @@ module Make (C : CONFIG) = struct
               [
                 iblock1
                   (casts @ ret_setup
-                  @ [I_aux (I_funcall (clexp, extern, (id, ctyp_args), args), aux)]
+                  @ [I_aux (I_funcall (CR_one clexp, extern, (id, ctyp_args), args), aux)]
                   @ tail @ ret_cleanup @ cleanup
                   );
               ]

src/lib/jib_compile.mli

@@ -158,10 +158,12 @@ module type CONFIG = sig
      for debugging C but we want to turn it off for SMT generation
      where we can't use strings *)
   val track_throw : bool
+
+  val use_void : bool
 end
 
 module IdGraph : sig
-  include Graph.S with type node = id
+  include Graph.S with type node = id and type node_set = IdSet.t
 end
 
 val callgraph : cdef list -> IdGraph.graph

src/lib/jib_optimize.ml

@@ -73,9 +73,9 @@ open Jib_util
 let optimize_unit instrs =
   let unit_cval cval = match cval_ctyp cval with CT_unit -> V_lit (VL_unit, CT_unit) | _ -> cval in
   let unit_instr = function
-    | I_aux (I_funcall (clexp, extern, id, args), annot) as instr -> begin
+    | I_aux (I_funcall (CR_one clexp, extern, id, args), annot) as instr -> begin
         match clexp_ctyp clexp with
-        | CT_unit -> I_aux (I_funcall (CL_void, extern, id, List.map unit_cval args), annot)
+        | CT_unit -> I_aux (I_funcall (CR_one CL_void, extern, id, List.map unit_cval args), annot)
         | _ -> instr
       end
     | I_aux (I_copy (clexp, cval), annot) as instr -> begin
@@ -163,6 +163,7 @@ let unique_per_function_ids cdefs =
 
 let rec cval_subst id subst = function
   | V_id (id', ctyp) -> if Name.compare id id' = 0 then subst else V_id (id', ctyp)
+  | V_member (id, ctyp) -> V_member (id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (op, cvals) -> V_call (op, List.map (cval_subst id subst) cvals)
   | V_field (cval, field) -> V_field (cval_subst id subst cval, field)
@@ -174,6 +175,7 @@ let rec cval_subst id subst = function
 
 let rec cval_map_id f = function
   | V_id (id, ctyp) -> V_id (f id, ctyp)
+  | V_member (id, ctyp) -> V_member (id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (call, cvals) -> V_call (call, List.map (cval_map_id f) cvals)
   | V_field (cval, field) -> V_field (cval_map_id f cval, field)
@@ -259,6 +261,10 @@ let rec clexp_subst id subst = function
   | CL_void -> CL_void
   | CL_rmw _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot substitute into read-modify-write construct"
 
+let creturn_subst id subst = function
+  | CR_one clexp -> CR_one (clexp_subst id subst clexp)
+  | CR_multi clexps -> CR_multi (List.map (clexp_subst id subst) clexps)
+
 let rec find_function fid = function
   | CDEF_aux (CDEF_fundef (fid', heap_return, args, body), _) :: _ when Id.compare fid fid' = 0 ->
       Some (heap_return, args, body)
@@ -271,14 +277,15 @@ let ssa_name i = function
   | Current_exception _ -> Current_exception i
   | Throw_location _ -> Throw_location i
   | Return _ -> Return i
+  | Channel (chan, _) -> Channel (chan, i)
 
 let inline cdefs should_inline instrs =
   let inlines = ref (-1) in
   let label_count = ref (-1) in
 
   let replace_return subst = function
-    | I_aux (I_funcall (clexp, extern, fid, args), aux) ->
-        I_aux (I_funcall (clexp_subst return subst clexp, extern, fid, args), aux)
+    | I_aux (I_funcall (creturn, extern, fid, args), aux) ->
+        I_aux (I_funcall (creturn_subst return subst creturn, extern, fid, args), aux)
     | I_aux (I_copy (clexp, cval), aux) -> I_aux (I_copy (clexp_subst return subst clexp, cval), aux)
     | instr -> instr
   in
@@ -314,7 +321,8 @@ let inline cdefs should_inline instrs =
   in
 
   let inline_instr = function
-    | I_aux (I_funcall (clexp, false, function_id, args), aux) as instr when should_inline (fst function_id) -> begin
+    | I_aux (I_funcall (CR_one clexp, false, function_id, args), aux) as instr when should_inline (fst function_id) ->
+      begin
         match find_function (fst function_id) cdefs with
         | Some (None, ids, body) ->
             incr inlines;
@@ -446,6 +454,7 @@ let remove_tuples cdefs ctx =
         ctyp
   and fix_cval = function
     | V_id (id, ctyp) -> V_id (id, ctyp)
+    | V_member (id, ctyp) -> V_member (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_ctor_kind (cval, ctor, ctyp) -> V_ctor_kind (fix_cval cval, ctor, ctyp)
     | V_ctor_unwrap (cval, ctor, ctyp) -> V_ctor_unwrap (fix_cval cval, ctor, ctyp)
@@ -485,8 +494,12 @@ let remove_tuples cdefs ctx =
     | CL_void -> CL_void
     | CL_rmw (read, write, ctyp) -> CL_rmw (read, write, ctyp)
   in
+  let fix_creturn = function
+    | CR_one clexp -> CR_one (fix_clexp clexp)
+    | CR_multi clexps -> CR_multi (List.map fix_clexp clexps)
+  in
   let rec fix_instr_aux = function
-    | I_funcall (clexp, extern, id, args) -> I_funcall (fix_clexp clexp, extern, id, List.map fix_cval args)
+    | I_funcall (creturn, extern, id, args) -> I_funcall (fix_creturn creturn, extern, id, List.map fix_cval args)
     | I_copy (clexp, cval) -> I_copy (fix_clexp clexp, fix_cval cval)
     | I_init (ctyp, id, cval) -> I_init (ctyp, id, fix_cval cval)
     | I_reinit (ctyp, id, cval) -> I_reinit (ctyp, id, fix_cval cval)