More work on experimental C backend

2 files changed, 153 insertions, 11 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 1527c99b..028f0146 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -58,9 +58,16 @@ let zencode_id = function
   | Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l)
   | Id_aux (DeIid str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
 
+let lvar_typ = function
+  | Local (_, typ) -> typ
+  | Register typ -> typ
+  | _ -> assert false
+                                    
 type aexp =
   | AE_val of aval
   | AE_app of id * aval list * typ
+  | AE_cast of aexp * typ
+  | AE_assign of id * aexp
   | AE_let of id * aexp * aexp * typ
   | AE_block of aexp list * aexp * typ
   | AE_return of aval * typ
@@ -73,6 +80,8 @@ and aval =
 
 let rec map_aval f = function
   | AE_val v -> AE_val (f v)
+  | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ)
+  | AE_assign (id, aexp) -> AE_assign (id, map_aval f aexp)
   | AE_app (id, vs, typ) -> AE_app (id, List.map f vs, typ)
   | AE_let (id, aexp1, aexp2, typ) -> AE_let (id, map_aval f aexp1, map_aval f aexp2, typ)
   | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ)
@@ -80,6 +89,8 @@ let rec map_aval f = function
 
 let rec map_functions f = function
   | AE_app (id, vs, typ) -> f id vs typ
+  | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ)
+  | AE_assign (id, aexp) -> AE_assign (id, map_functions f aexp)
   | AE_let (id, aexp1, aexp2, typ) -> AE_let (id, map_functions f aexp1, map_functions f aexp2, typ)
   | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ)
   | AE_val _ | AE_return _ as v -> v
@@ -106,6 +117,10 @@ let pp_annot typ doc =
 
 let rec pp_aexp = function
   | AE_val v -> pp_aval v
+  | AE_cast (aexp, typ) ->
+     pp_annot typ (string "$" ^^ pp_aexp aexp)
+  | AE_assign (id, aexp) ->
+     pp_id id ^^ string " := " ^^ pp_aexp aexp
   | AE_app (id, args, typ) ->
      pp_annot typ (pp_id ~color:Util.red id ^^ parens (separate_map (comma ^^ space) pp_aval args))
   | AE_let (id, binding, body, typ) -> group
@@ -153,7 +168,7 @@ let rec split_block = function
 let rec anf (E_aux (e_aux, _) as exp) =
   let to_aval = function
     | AE_val v -> (v, fun x -> x)
-    | AE_app (_, _, typ) | AE_let (_, _, _, typ) | AE_return (_, typ) as aexp ->
+    | AE_app (_, _, typ) | AE_let (_, _, _, typ) | AE_return (_, typ) | AE_cast (_, typ) as aexp ->
        let id = gensym () in
        (AV_id (id, Local (Immutable, typ)), fun x -> AE_let (id, aexp, x, typ_of exp))
   in
@@ -166,12 +181,26 @@ let rec anf (E_aux (e_aux, _) as exp) =
      let alast = anf last in
      AE_block (aexps, alast, typ_of exp)
 
+  | E_assign (LEXP_aux (LEXP_id id, _), exp) ->
+     let aexp = anf exp in
+     AE_assign (id, aexp)
+              
   | E_app (id, exps) ->
      let aexps = List.map anf exps in
      let avals = List.map to_aval aexps in
      let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in
      wrap (AE_app (id, List.map fst avals, typ_of exp))
 
+  | E_throw exp ->
+     let aexp = anf exp in
+     let aval, wrap = to_aval aexp in
+     wrap (AE_app (mk_id "throw", [aval], unit_typ))
+          
+  | E_return exp ->
+     let aexp = anf exp in
+     let aval, wrap = to_aval aexp in
+     wrap (AE_app (mk_id "return", [aval], unit_typ))
+     
   | E_id id ->
      let lvar = Env.lookup_id id (env_of exp) in
      AE_val (AV_id (zencode_id id, lvar))
@@ -189,7 +218,7 @@ let rec anf (E_aux (e_aux, _) as exp) =
      let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in
      wrap (AE_val (AV_tuple (List.map fst avals)))
 
-  | E_cast (typ, exp) -> anf exp
+  | E_cast (typ, exp) -> AE_cast (anf exp, typ)
 
   | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ ->
      (* Should be re-written by type checker *)
@@ -199,7 +228,10 @@ let rec anf (E_aux (e_aux, _) as exp) =
      (* Interpreter specific *)
      failwith "encountered E_internal_value when converting to ANF"
 
-
+  | E_sizeof _ | E_constraint _ ->
+     (* Sizeof nodes removed by sizeof rewriting pass *)
+     failwith "encountered E_sizeof or E_constraint node when converting to ANF"
+              
 let max_int64 = Big_int.of_int64 Int64.max_int
 let min_int64 = Big_int.of_int64 Int64.min_int
 
@@ -227,6 +259,16 @@ let stack_typ (Typ_aux (typ_aux, _) as typ) =
      end
   | _ -> None
 
+let heap_typ (Typ_aux (typ_aux, _) as typ) =
+  match typ_aux with
+  | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" ->
+     Some "mpz_t"
+  | Typ_id id when string_of_id id = "int" ->
+     Some "mpz_t"
+  | Typ_app (id, _) when string_of_id id = "vector" ->
+     Some "sail_bv"
+  | _ -> None
+
 let is_stack_typ typ = match stack_typ typ with
   | Some _ -> true
   | None -> false
@@ -237,7 +279,7 @@ let literal_to_cstring (L_aux (l_aux, _) as lit) =
      Some (Big_int.to_string n ^ "L")
   | L_hex str when String.length str <= 16 ->
      let padding = 16 - String.length str in
-     Some ("0x" ^ String.make padding '0' ^ str ^ "L")
+     Some ("0x" ^ String.make padding '0' ^ str ^ "ul")
   | _ -> None
 
 let c_literals =
@@ -256,8 +298,8 @@ let mask m =
   if Big_int.less_equal m (Big_int.of_int 64) then
     let n = Big_int.to_int m in
     if n mod 4 == 0
-    then "0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ "L"
-    else "0b" ^ String.make (64 - n) '0' ^ String.make n '1' ^ "L"
+    then "0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ "ul"
+    else "0b" ^ String.make (64 - n) '0' ^ String.make n '1' ^ "ul"
   else
     failwith "Tried to create a mask literal for a vector greater than 64 bits."
 
@@ -273,7 +315,7 @@ let c_aval = function
   | AV_id (id, lvar) as v ->
      begin
        match lvar with
-       | Local (Immutable, typ) when is_stack_typ typ ->
+       | Local (_, typ) when is_stack_typ typ ->
           AV_C_fragment (string_of_id id, typ)
        | _ -> v
      end
@@ -287,7 +329,7 @@ let c_fragment_string = function
   | AV_C_fragment (str, _) -> str
   | _ -> assert false
 
-let analyze_primop id args typ =
+let analyze_primop' id args typ =
   let no_change = AE_app (id, args, typ) in
 
   (* primops add_range and add_atom *)
@@ -319,7 +361,6 @@ let analyze_primop id args typ =
       in
       match nexp_simp n with
       | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) ->
-         print_endline "small";
          let x, y = c_aval x, c_aval y in
          if is_c_fragment x && is_c_fragment y then
            AE_val (AV_C_fragment ("(" ^ c_fragment_string x ^ " + " ^ c_fragment_string y ^ ") & " ^ mask n, typ))
@@ -331,10 +372,111 @@ let analyze_primop id args typ =
   else
     no_change
 
-let compile_exp exp =
+let analyze_primop id args typ =
+  let no_change = AE_app (id, args, typ) in
+  try analyze_primop' id args typ with
+  | Failure _ -> no_change
+
+type allocation =
+  | Stack of string
+  | Heap of string
+
+let string_of_allocation = function
+  | Stack str -> "S$" ^ str
+  | Heap str -> "H$" ^ str
+
+let choose_allocation typ =
+  match stack_typ typ with
+  | Some str -> Stack str
+  | None ->
+     match heap_typ typ with
+     | Some str -> Heap str
+     | _ -> failwith "don't know where to allocate type"
+
+type ccall =
+  | CCallH of (string -> string)
+  | CCallS of string
+                     
+let compile_funcall env id args typ =
+  let setup = ref [] in
+  let cleanup = ref [] in
+
+  let _, Typ_aux (fn_typ, _) = Env.get_val_spec id env in
+  let arg_typs, ret_typ = match fn_typ with
+    | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
+    | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+    | _ -> assert false
+  in
+  let arg_allocs = List.map choose_allocation arg_typs in
+  print_endline (Util.string_of_list ", " string_of_allocation arg_allocs);
+
+  let setup_arg alloc aval =
+    match alloc, aval with
+    | Heap str_h, AV_C_fragment (c, typ) ->
+       let Some str_s = stack_typ typ in
+       let g = gensym () in
+       setup := (str_h ^ " " ^ string_of_id g ^ ";") :: !setup;
+       setup := Printf.sprintf "init_%s_of_%s(%s, %s);" str_h str_s (string_of_id g) c :: !setup;
+       cleanup := Printf.sprintf "clear_%s(%s);" str_h (string_of_id g) :: !cleanup;
+       string_of_id g
+    | Stack str_h, AV_C_fragment (c, typ) -> c
+    | Heap str_h, AV_id (id, typ) ->
+       begin
+         match choose_allocation (lvar_typ typ) with
+         | Heap _ -> string_of_id id
+         | Stack str_s ->
+            let g = gensym () in
+            setup := (str_h ^ " " ^ string_of_id g ^ ";") :: !setup;
+            setup := Printf.sprintf "init_%s_of_%s(%s, %s);" str_h str_s (string_of_id g) (string_of_id id) :: !setup;
+            cleanup := Printf.sprintf "clear_%s(%s);" str_h (string_of_id g) :: !cleanup;
+            string_of_id g         
+       end
+    | Stack str_s, AV_id (id, typ) -> string_of_id id
+    | _, AV_id _ -> "AV_id"
+    | _, AV_lit _ -> "AV_lit"
+  in
+  
+  let str_args = List.map2 setup_arg arg_allocs args in
+
+  match choose_allocation ret_typ with
+  | Heap str_h ->
+     let call ret = Printf.sprintf "sail_%s(%s, %s);" (string_of_id id) ret (String.concat ", " str_args) in
+     (List.rev !setup, str_h, CCallH call, !cleanup)
+  | Stack str_s ->
+     let call = Printf.sprintf "sail_%s(%s);" (string_of_id id) (String.concat ", " str_args) in
+     (List.rev !setup, str_s, CCallS call, !cleanup)
+       
+let rec compile_aexp env = function
+  | AE_let (id, binding, body, typ) ->
+     let setup, ctyp, call, cleanup = compile_aexp env binding in
+     let letb1, letb1c = match call with
+       | CCallH f -> f (string_of_id id), [Printf.sprintf "clear_%s(%s);" ctyp (string_of_id id)]
+       | CCallS str -> string_of_id id ^ " = " ^ str, []    
+     in
+     let letb2 = setup @ [ctyp ^ " " ^ string_of_id id ^ ";"; letb1] @ cleanup in
+     let setup, ctyp, call, cleanup = compile_aexp env body in
+     letb2 @ setup, ctyp, call, cleanup @ letb1c
+  
+  | AE_app (id, vs, typ) ->
+     compile_funcall env id vs typ
+
+  | AE_val (AV_C_fragment (c, typ)) ->
+     let Some ctyp = stack_typ typ in
+     [], ctyp, CCallS c, []
+
+let print_compiled (setup, ctyp, call, cleanup) =
+  List.iter print_endline setup;
+  begin match call with
+  | CCallH f -> print_endline (f ("?" ^ ctyp))
+  | CCallS str -> print_endline ("?" ^ ctyp ^ " = " ^ str)
+  end;
+  List.iter print_endline cleanup
+                     
+let compile_exp env exp =
   let aexp = anf exp in
   let aexp = c_literals aexp in
   let aexp = map_functions analyze_primop aexp in
+  print_compiled (compile_aexp env aexp);
   aexp
 
 
diff --git a/src/isail.ml b/src/isail.ml
index 235e46a2..07a72bd2 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -296,7 +296,7 @@ let handle_input' input =
                vs_ids := Initial_check.val_spec_ids !interactive_ast
             | ":compile" ->
                let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord arg) in
-               let anf = C_backend.compile_exp exp in
+               let anf = C_backend.compile_exp !interactive_env exp in
                print_endline (Pretty_print_sail.to_string (C_backend.pp_aexp anf))
             | ":u" | ":unload" ->
                interactive_ast := Ast.Defs [];