Add interface field to drivers

drivers/c.drv

@@ -141,6 +141,44 @@ static struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
   result.__field_1 = (uint32_t)(r >> 32);
   return result;
 }
+"
+
+  interface
+"
+struct __add32_with_carry_result
+{ uint32_t __field_0;
+  uint32_t __field_1;
+};
+
+static struct __add32_with_carry_result add32_with_carry(uint32_t x, uint32_t y, uint32_t c);
+
+struct __sub32_with_borrow_result
+{ uint32_t __field_0;
+  uint32_t __field_1;
+};
+
+static struct __sub32_with_borrow_result sub32_with_borrow(uint32_t x, uint32_t y, uint32_t b);
+
+struct __mul32_double_result
+{ uint32_t __field_0;
+  uint32_t __field_1;
+};
+
+static struct __mul32_double_result mul32_double(uint32_t x, uint32_t y);
+
+struct __add32_3_result
+{ uint32_t __field_0;
+  uint32_t __field_1;
+};
+
+static struct __add32_3_result add32_3(uint32_t x, uint32_t y, uint32_t z);
+
+struct __lsld32_result
+{ uint32_t __field_0;
+  uint32_t __field_1;
+};
+
+static struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
 "
 
   syntax converter of_int "%1U"
@@ -331,6 +369,70 @@ static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
 }
 "
 
+  interface
+"
+#include \"config.h\"
+#include \"gmp.h\"
+#include \"gmp-impl.h\"
+#include \"longlong.h\"
+
+#undef invert_limb
+
+struct __add64_with_carry_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static struct __add64_with_carry_result
+add64_with_carry(uint64_t x, uint64_t y, uint64_t c);
+
+struct __add64_double_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static struct __add64_double_result
+add64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0);
+
+struct __sub64_with_borrow_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static struct __sub64_with_borrow_result
+sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b);
+
+struct __sub64_double_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static struct __sub64_double_result
+sub64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0);
+
+struct __mul64_double_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static struct __mul64_double_result mul64_double(uint64_t x, uint64_t y);
+
+static uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d);
+
+struct __add64_3_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z);
+
+struct __lsld64_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt);
+"
   syntax converter of_int "%1ULL"
 
   syntax val (+)     "%1 + %2"

src/core/printer.ml

@@ -24,6 +24,8 @@ open Task
 
 type prelude = string list
 type prelude_map = prelude Mid.t
+type interface = string list
+type interface_map = interface Mid.t
 type blacklist = string list
 
 type 'a pp = Pp.formatter -> 'a -> unit
@@ -320,6 +322,8 @@ let print_prelude fmt pl =
   let println fmt s = fprintf fmt "%s@\n" s in
   print_list nothing println fmt pl
 
+let print_interface = print_prelude
+
 let print_prelude_of_theories th_used fmt pm =
   let ht = Hid.create 5 in
   List.iter (fun { th_name = id } ->

src/core/printer.mli

@@ -21,6 +21,8 @@ open Task
 
 type prelude = string list
 type prelude_map = prelude Mid.t
+type interface = string list
+type interface_map = interface Mid.t
 type blacklist = string list
 
 (* Makes it possible to estabilish traceability from names
@@ -59,6 +61,7 @@ val list_printers : unit -> (string * Pp.formatted) list
 
 val print_prelude : prelude Pp.pp
 val print_th_prelude : task -> prelude_map Pp.pp
+val print_interface : interface Pp.pp
 
 val meta_syntax_type : meta
 val meta_syntax_logic : meta

src/driver/driver_ast.ml

@@ -44,6 +44,7 @@ type theory_rules = {
 
 type mo_rule =
   | MRtheory    of th_rule
+  | MRinterface of string
   | MRexception of qualid * string
   | MRval       of qualid * string
 

src/driver/driver_lexer.mll

@@ -24,6 +24,7 @@
         "remove", REMOVE;
         "meta", META;
         "prelude", PRELUDE;
+        "interface", INTERFACE;
         "printer", PRINTER;
 	"steps", STEPS;
 	"model_parser", MODEL_PARSER;

src/driver/driver_parser.mly

@@ -20,6 +20,7 @@
 %token <string> OPERATOR
 %token <string> INPUT (* never reaches the parser *)
 %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER OVERRIDING
+%token INTERFACE
 %token VALID INVALID UNKNOWN FAIL
 %token TIMEOUT OUTOFMEMORY STEPLIMITEXCEEDED TIME STEPS
 %token UNDERSCORE LEFTPAR RIGHTPAR DOT DOTDOT QUOTE EOF
@@ -29,7 +30,7 @@
 %token COMMA CONSTANT
 %token LEFTSQ RIGHTSQ LARROW
 
-%nonassoc SYNTAX REMOVE PRELUDE
+%nonassoc SYNTAX REMOVE PRELUDE INTERFACE
 %nonassoc prec_pty
 
 %start <Driver_ast.file> file
@@ -118,6 +119,7 @@ ident:
 | SYNTAX       { "syntax" }
 | REMOVE       { "remove" }
 | PRELUDE      { "prelude" }
+| INTERFACE    { "interface" }
 | BLACKLIST    { "blacklist" }
 | PRINTER      { "printer" }
 | STEPS        { "steps" }
@@ -199,6 +201,7 @@ module_:
 
 mrule:
 | trule                          { MRtheory $1 }
+| INTERFACE STRING               { MRinterface ($2) }
 | SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) }
 | SYNTAX VAL qualid STRING       { MRval ($3, $4) }
 

src/mlw/cprinter.ml

@@ -362,6 +362,7 @@ type info = Pdriver.printer_args = private {
   env         : Env.env;
   prelude     : Printer.prelude;
   thprelude   : Printer.prelude_map;
+  thinterface : Printer.interface_map;
   blacklist   : Printer.blacklist;
   syntax      : Printer.syntax_map;
   converter   : Printer.syntax_map;

src/mlw/pdriver.ml

@@ -24,6 +24,7 @@ type driver = {
   drv_printer     : string option;
   drv_prelude     : Printer.prelude;
   drv_thprelude   : Printer.prelude_map;
+  drv_thinterface : Printer.interface_map;
   drv_blacklist   : Printer.blacklist;
   drv_syntax      : Printer.syntax_map;
   drv_converter   : Printer.syntax_map;
@@ -34,6 +35,7 @@ type printer_args = {
   env         : Env.env;
   prelude     : Printer.prelude;
   thprelude   : Printer.prelude_map;
+  thinterface : Printer.interface_map;
   blacklist   : Printer.blacklist;
   syntax      : Printer.syntax_map;
   converter   : Printer.syntax_map;
@@ -85,6 +87,7 @@ let load_driver env file extra_files =
   List.iter add_global f.fe_global;
 
   let thprelude = ref Mid.empty in
+  let thinterface = ref Mid.empty in
   let syntax_map = ref Mid.empty in
   let converter_map = ref Mid.empty in
   let literal_map = ref Mid.empty in
@@ -179,6 +182,10 @@ let load_driver env file extra_files =
     with Not_found -> Loc.error ~loc (UnknownExn (!qualid,q))
   in
   let add_local_module loc m = function
+    | MRinterface s ->
+       let th = m.mod_theory in
+       let l = Mid.find_def [] th.th_name !thinterface in
+       thinterface := Mid.add th.th_name (s::l) !thinterface
     | MRexception (q,s) ->
         let xs = find_xs m q in
         add_syntax xs.Ity.xs_name s false
@@ -218,6 +225,7 @@ let load_driver env file extra_files =
     drv_printer     = !printer;
     drv_prelude     = List.rev !prelude;
     drv_thprelude   = Mid.map List.rev !thprelude;
+    drv_thinterface = Mid.map List.rev !thinterface;
     drv_blacklist   = Queue.fold (fun l s -> s :: l) [] blacklist;
     drv_syntax      = !syntax_map;
     drv_converter   = !converter_map;
@@ -273,6 +281,7 @@ let lookup_printer drv =
       env         = drv.drv_env;
       prelude     = drv.drv_prelude;
       thprelude   = drv.drv_thprelude;
+      thinterface = drv.drv_thinterface;
       blacklist   = drv.drv_blacklist;
       syntax      = drv.drv_syntax;
       converter   = drv.drv_converter;

src/mlw/pdriver.mli

@@ -16,6 +16,7 @@ type driver = private {
   drv_printer     : string option;
   drv_prelude     : Printer.prelude;
   drv_thprelude   : Printer.prelude_map;
+  drv_thinterface : Printer.interface_map;
   drv_blacklist   : Printer.blacklist;
   drv_syntax      : Printer.syntax_map;
   drv_converter   : Printer.syntax_map;
@@ -27,6 +28,7 @@ type printer_args = private {
   env         : Env.env;
   prelude     : Printer.prelude;
   thprelude   : Printer.prelude_map;
+  thinterface : Printer.interface_map;
   blacklist   : Printer.blacklist;
   syntax      : Printer.syntax_map;
   converter   : Printer.syntax_map;