CN: more steps towards handling GCC builtins

This is so far work in progress.

This config ought to permit core-peval to unfold some of the proxy
wrappers in the core stdlib, but it doesn't seem to be working yet.

backend/cn/core_to_mucore.ml

@@ -1423,7 +1423,7 @@ let normalise_file (markers_env, ail_prog) file =
 
  let env = List.fold_left register_glob env globs in
 
- Print.debug 3 (lazy (Print.item "stdlib symbols" (Print.list Sym.pp
+ Print.debug 3 (lazy (Print.item "stdlib symbols" (Print.list Sym.pp_debug
  (List.map fst (Pmap.bindings_list file.mi_stdlib)))));
 
  Print.debug 3 (lazy (Print.item "stdlib symbols in fmap" (Print.list Sym.pp

backend/cn/main.ml

@@ -61,6 +61,7 @@ let frontend incl_dirs incl_files astprints filename state_file =
  Cerb_global.set_cerb_conf "Cn" false Random false Basic false false false false false;
  Ocaml_implementation.set Ocaml_implementation.HafniumImpl.impl;
  Switches.set ["inner_arg_temps"; "at_magic_comments"; "warn_mismatched_magic_comments"];
+ Core_peval.config_unfold_stdlib := Sym.has_id_with Setup.unfold_stdlib_name;
  let@ stdlib = load_core_stdlib () in
  let@ impl = load_core_impl stdlib impl_name in
  let conf = Setup.conf incl_dirs incl_files astprints in

backend/cn/setup.ml

@@ -1,4 +1,5 @@
 open Cerb_backend.Pipeline
+module StringSet = Set.Make(String)
 
 
 let io = default_io_helpers
@@ -52,3 +53,10 @@ let conf incl_dirs incl_files astprints =
  ; cpp_cmd = with_cn_keywords (cpp_str incl_dirs incl_files)
  ; cpp_stderr = true
  }
+
+let unfold_proxies = StringSet.of_list [
+ "ffs_proxy"; "ffsl_proxy"; "ffsll_proxy"; "ctz_proxy";
+ ]
+
+let unfold_stdlib_name s = StringSet.mem s unfold_proxies
+

backend/cn/sym.ml

@@ -44,6 +44,10 @@ let has_id = function
  | _ -> 
  None
 
+let has_id_with f sym = match has_id sym with
+ | None -> false
+ | Some str -> f str
+
 
 module StringHash =
  Hashtbl.Make(struct

runtime/libcore/std_inner_arg_temps.core

@@ -751,7 +751,7 @@ builtin bswap16 (integer): eff loaded integer
 builtin bswap32 (integer): eff loaded integer
 builtin bswap64 (integer): eff loaded integer
 
-proc [ailname = " "] ctz_proxy (n_: loaded integer): eff loaded integer :=
+proc [ailname = "__builtin_ctz"] ctz_proxy (n_: loaded integer): eff loaded integer :=
  case n_ of
  | Specified (n: integer) =>
  if n = 0 then

tests/cn/builtin_ctz.c

@@ -5,6 +5,7 @@ f (unsigned int x) {
  unsigned int y;
 
  y = __builtin_ctz(x);
+ y = __builtin_ffs(x);
 
  if (y < 10) {
  return 1;