From 07d4c4b7de97e91894ab206f450a13b30a9260c5 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@cl.cam.ac.uk>
Date: Wed, 16 Aug 2023 10:50:48 +0100
Subject: [PATCH] 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             | 2 +-
 backend/cn/main.ml                       | 1 +
 backend/cn/setup.ml                      | 8 ++++++++
 backend/cn/sym.ml                        | 4 ++++
 runtime/libcore/std_inner_arg_temps.core | 2 +-
 tests/cn/builtin_ctz.c                   | 1 +
 6 files changed, 16 insertions(+), 2 deletions(-)

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;