Add tagged memory to C rts to cheri can be compiled to C

3 files changed, 1 insertions, 11 deletions

diff --git a/src/anf.ml b/src/anf.ml
index d51d29a3..98ec7d08 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -59,8 +59,6 @@ module Big_int = Nat_big_num
 let anf_error ?loc:(l=Parse_ast.Unknown) message =
   raise (Reporting_basic.err_general l ("\nANF translation: " ^ message))
 
-
-  
 (**************************************************************************)
 (* 1. Conversion to A-normal form (ANF)                                   *)
 (**************************************************************************)
diff --git a/src/c_backend.ml b/src/c_backend.ml
index c2c1fd39..d18ca354 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -60,7 +60,7 @@ open Anf
 
 module Big_int = Nat_big_num
 
-let c_verbosity = ref 1
+let c_verbosity = ref 0
 let opt_ddump_flow_graphs = ref false
 let opt_trace = ref false
 
@@ -1504,7 +1504,6 @@ let rec compile_def ctx = function
   | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) ->
      c_debug (lazy ("Compiling function " ^ string_of_id id));
      let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in
-     if string_of_id id = "fetch_and_execute" then prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)) else ();
      let setup, ctyp, call, cleanup = compile_aexp ctx aexp in
      c_debug (lazy "Compiled aexp");
      let fundef_label = label "fundef_fail_" in
diff --git a/src/specialize.ml b/src/specialize.ml
index de82c920..0ac84e86 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -335,7 +335,6 @@ let specialize_id_fundef instantiations id ast =
        let spec_id = id_of_instantiation id instantiation in
        if IdSet.mem spec_id !spec_ids then [] else
          begin
-           prerr_endline ("specialised fundef " ^ string_of_id id ^ " to " ^ string_of_id spec_id);
            spec_ids := IdSet.add spec_id !spec_ids;
            [DEF_fundef (rename_fundef spec_id fundef)]
          end
@@ -382,10 +381,8 @@ let remove_unused_valspecs env ast =
   let rec remove_unused (Defs defs) id =
     match defs with
     | def :: defs when is_fundef id def ->
-       prerr_endline ("Removing fundef: " ^ string_of_id id);
        remove_unused (Defs defs) id
     | def :: defs when is_valspec id def ->
-       prerr_endline ("Removing valspec: " ^ string_of_id id);
        remove_unused (Defs defs) id
     | DEF_overload (overload_id, overloads) :: defs ->
        begin
@@ -400,10 +397,7 @@ let remove_unused_valspecs env ast =
   List.fold_left (fun ast id -> Defs (remove_unused ast id)) ast (IdSet.elements unused)
 
 let specialize_id id ast =
-  prerr_endline ("specialising: " ^ string_of_id id);
   let instantiations = instantiations_of id ast in
-  List.iter (fun i -> prerr_endline (string_of_instantiation i)) instantiations;
-
   let ast = specialize_id_valspec instantiations id ast in
   let ast = specialize_id_fundef instantiations id ast in
   specialize_id_overloads instantiations id ast
@@ -530,7 +524,6 @@ let specialize_variants ((Defs defs) as ast) env =
   Type_error.check Type_check.initial_env ast
 
 let rec specialize ast env =
-  prerr_endline (Util.log_line __MODULE__ __LINE__ "Performing specialisation pass");
   let ids = polymorphic_functions (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt) ast in
   if IdSet.is_empty ids then
     specialize_variants ast env