Add SV IR and move Jib SSA file

language/jib.ott

@@ -60,11 +60,16 @@ open import Value2
 
 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 :: '' ::=
@@ -109,6 +114,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
@@ -192,6 +198,10 @@ iannot :: '' ::=
   {{ lem nat * nat * nat }}
   {{ ocaml int * int * int }}
 
+creturn :: 'CR_' ::=
+  | clexp                     :: :: one
+  | ( clexp0 , ... , clexpn ) :: :: multi
+
 instr :: 'I_' ::=
   {{ aux _ iannot }}
 % The following are the minimal set of instructions output by
@@ -201,7 +211,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

@@ -355,7 +355,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

@@ -256,6 +256,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)
@@ -359,6 +360,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), [])
@@ -633,7 +635,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
@@ -1130,8 +1132,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
 
@@ -1441,6 +1446,7 @@ module Make (C : CONFIG) = struct
 
     (* Optimize and compile the expression to ANF. *)
     let aexp = C.optimize_anf ctx (no_shadow (IdSet.union known_ids !guard_bindings) (anf exp)) in
+    prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp));
 
     let setup, call, cleanup = compile_aexp ctx aexp in
     let destructure, destructure_cleanup =
@@ -1809,7 +1815,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)
@@ -1979,7 +1985,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
@@ -1991,7 +1997,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
                         );
                     ]
@@ -2035,7 +2043,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)
@@ -277,8 +283,8 @@ let inline cdefs should_inline instrs =
   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 +320,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 +453,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 +493,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)

src/sail_smt_backend/jib_ssa.ml → src/lib/jib_ssa.ml

@@ -65,21 +65,32 @@
 (*  SUCH DAMAGE.                                                            *)
 (****************************************************************************)
 
-open Libsail
-
 open Ast_util
 open Jib
 open Jib_util
 
-module IntSet = Set.Make (struct
-  type t = int
-  let compare = compare
-end)
+module IntSet = Util.IntSet
 module IntMap = Map.Make (struct
   type t = int
   let compare = compare
 end)
 
+let ssa_name i = function
+  | Name (id, _) -> Name (id, i)
+  | Have_exception _ -> Have_exception i
+  | Current_exception _ -> Current_exception i
+  | Throw_location _ -> Throw_location i
+  | Channel (c, _) -> Channel (c, i)
+  | Return _ -> Return i
+
+let unssa_name = function
+  | Name (id, n) -> (Name (id, -1), n)
+  | Have_exception n -> (Have_exception (-1), n)
+  | Current_exception n -> (Current_exception (-1), n)
+  | Throw_location n -> (Throw_location (-1), n)
+  | Channel (c, n) -> (Channel (c, -1), n)
+  | Return n -> (Return (-1), n)
+
 (**************************************************************************)
 (* 1. Mutable graph type                                                  *)
 (**************************************************************************)
@@ -486,14 +497,6 @@ let rename_variables graph root children =
 
   let phi_zeros = ref NameMap.empty in
 
-  let ssa_name i = function
-    | Name (id, _) -> Name (id, i)
-    | Have_exception _ -> Have_exception i
-    | Current_exception _ -> Current_exception i
-    | Throw_location _ -> Throw_location i
-    | Return _ -> Return i
-  in
-
   let get_count id = match NameMap.find_opt id !counts with Some n -> n | None -> 0 in
   let top_stack id = match NameMap.find_opt id !stacks with Some (x :: _) -> x | Some [] -> 0 | None -> 0 in
   let top_stack_phi id ctyp =
@@ -512,6 +515,7 @@ let rename_variables graph root children =
     | V_id (id, ctyp) ->
         let i = top_stack id in
         V_id (ssa_name i id, ctyp)
+    | V_member (id, ctyp) -> V_member (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_call (id, fs) -> V_call (id, List.map fold_cval fs)
     | V_field (f, field) -> V_field (fold_cval f, field)
@@ -540,13 +544,17 @@ let rename_variables graph root children =
     | CL_tuple (clexp, n) -> CL_tuple (fold_clexp true clexp, n)
     | CL_void -> CL_void
   in
+  let fold_creturn = function
+    | CR_one clexp -> CR_one (fold_clexp false clexp)
+    | CR_multi clexps -> CR_multi (List.map (fold_clexp false) clexps)
+  in
 
   let ssa_instr (I_aux (aux, annot)) =
     let aux =
       match aux with
-      | I_funcall (clexp, extern, id, args) ->
+      | I_funcall (creturn, extern, id, args) ->
           let args = List.map fold_cval args in
-          I_funcall (fold_clexp false clexp, extern, id, args)
+          I_funcall (fold_creturn creturn, extern, id, args)
       | I_copy (clexp, cval) ->
           let cval = fold_cval cval in
           I_copy (fold_clexp false clexp, cval)
@@ -721,7 +729,7 @@ let string_of_node = function
   | phis, CF_block (instrs, terminator) ->
       let string_of_instr instr =
         let buf = Buffer.create 128 in
-        Jib_ir.Flat_ir_formatter.output_instr 0 buf 0 Jib_ir.StringMap.empty instr;
+        (* Jib_ir.Flat_ir_formatter.output_instr 0 buf 0 Jib_ir.StringMap.empty instr; *)
         Buffer.contents buf
       in
       string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (string_of_instr instr)) instrs

src/sail_smt_backend/jib_ssa.mli → src/lib/jib_ssa.mli

@@ -65,19 +65,21 @@
 (*  SUCH DAMAGE.                                                            *)
 (****************************************************************************)
 
-open Libsail
-
 open Array
 open Jib_util
 
+val ssa_name : int -> Jib.name -> Jib.name
+
+val unssa_name : Jib.name -> Jib.name * int
+
 (** A mutable array based graph type, with nodes indexed by integers. *)
 type 'a array_graph
 
 (** Create an empty array_graph, specifying the initial size of the
    underlying array. *)
 val make : initial_size:int -> unit -> 'a array_graph
 
-module IntSet : Set.S with type elt = int
+module IntSet = Util.IntSet
 
 val get_cond : 'a array_graph -> int -> Jib.cval