Add support for EF_runtime externals

Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.

4 files changed, 11 insertions, 2 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index e4001e6b..418fa702 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -1090,6 +1090,7 @@ let convertFundef loc env fd =
 (** External function declaration *)
 
 let re_builtin = Str.regexp "__builtin_"
+let re_runtime = Str.regexp "__i64_"
 
 let convertFundecl env (sto, id, ty, optinit) =
   let (args, res, cconv) =
@@ -1102,6 +1103,7 @@ let convertFundecl env (sto, id, ty, optinit) =
   let ef =
     if id.name = "malloc" then EF_malloc else
     if id.name = "free" then EF_free else
+    if Str.string_match re_runtime id.name 0 then EF_runtime(id'', sg) else
     if Str.string_match re_builtin id.name 0
     && List.mem_assoc id.name builtins.functions
     then EF_builtin(id'', sg)
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7e966ffe..36f7bf7d 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -536,6 +536,7 @@ Definition do_external (ef: external_function):
   match ef with
   | EF_external name sg => do_external_function name sg ge
   | EF_builtin name sg => do_external_function name sg ge
+  | EF_runtime name sg => do_external_function name sg ge
   | EF_vload chunk => do_ef_volatile_load chunk
   | EF_vstore chunk => do_ef_volatile_store chunk
   | EF_malloc => do_ef_malloc
@@ -558,6 +559,8 @@ Proof with try congruence.
   eapply do_external_function_sound; eauto.
 (* EF_builtin *)
   eapply do_external_function_sound; eauto.
+(* EF_runtime *)
+  eapply do_external_function_sound; eauto.
 (* EF_vload *)
   unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
   mydestr. destruct p as [[w'' t''] v]; mydestr.
@@ -604,6 +607,8 @@ Proof.
   eapply do_external_function_complete; eauto.
 (* EF_builtin *)
   eapply do_external_function_complete; eauto.
+(* EF_runtime *)
+  eapply do_external_function_complete; eauto.
 (* EF_vload *)
   inv H; unfold do_ef_volatile_load.
   exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index ed19e178..42892901 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -258,7 +258,7 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | External(EF_external(_,_), args, res, cconv) ->
+  | External((EF_external _ | EF_runtime _), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
                 (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
   | External(_, _, _, _) ->
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index bb6576aa..d5853e38 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -264,6 +264,8 @@ let rec expr p (prec, e) =
                 (camlstring_of_coqstring txt) exprlist (false, args)
   | Ebuiltin(EF_external(id, sg), _, args, _) ->
       fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
+  | Ebuiltin(EF_runtime(id, sg), _, args, _) ->
+      fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
   | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) ->
       extended_asm p txt None args clob
   | Ebuiltin(EF_debug(kind,txt,_),_,args,_) ->
@@ -427,7 +429,7 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | External(EF_external(_,_), args, res, cconv) ->
+  | External((EF_external _ | EF_runtime _), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
                 (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
   | External(_, _, _, _) ->