diff --git a/backend/cn/core_to_mucore.ml b/backend/cn/core_to_mucore.ml index a81525ea4..ce302303f 100644 --- a/backend/cn/core_to_mucore.ml +++ b/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 diff --git a/backend/cn/main.ml b/backend/cn/main.ml index 647fb277d..eeaaec540 100644 --- a/backend/cn/main.ml +++ b/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 diff --git a/backend/cn/setup.ml b/backend/cn/setup.ml index 1fdf214e8..1ad3c554d 100644 --- a/backend/cn/setup.ml +++ b/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 + diff --git a/backend/cn/sym.ml b/backend/cn/sym.ml index 0cd23a349..e846d4b6a 100644 --- a/backend/cn/sym.ml +++ b/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 diff --git a/runtime/libcore/std_inner_arg_temps.core b/runtime/libcore/std_inner_arg_temps.core index 22dd9421d..87d4b7383 100644 --- a/runtime/libcore/std_inner_arg_temps.core +++ b/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 diff --git a/tests/cn/builtin_ctz.c b/tests/cn/builtin_ctz.c index c19c346fe..cb86099d2 100644 --- a/tests/cn/builtin_ctz.c +++ b/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;