making library statically link to horn backend

autom4te.cache/requests

@@ -14,63 +14,63 @@
                         'configure.ac'
                       ],
                       {
-                        '_AM_MAKEFILE_INCLUDE' => 1,
-                        'AM_ENABLE_MULTILIB' => 1,
+                        'AM_PROG_MOC' => 1,
+                        'AM_XGETTEXT_OPTION' => 1,
+                        'AC_CANONICAL_BUILD' => 1,
                         'm4_sinclude' => 1,
-                        'AC_CONFIG_FILES' => 1,
-                        'AM_AUTOMAKE_VERSION' => 1,
-                        'AM_CONDITIONAL' => 1,
+                        'AM_PROG_CC_C_O' => 1,
+                        '_AM_MAKEFILE_INCLUDE' => 1,
+                        'AM_PROG_F77_C_O' => 1,
+                        'm4_include' => 1,
+                        'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
                         '_AM_COND_IF' => 1,
-                        'AM_POT_TOOLS' => 1,
+                        '_LT_AC_TAGCONFIG' => 1,
                         'AM_PROG_AR' => 1,
-                        'AM_PROG_F77_C_O' => 1,
+                        'AM_CONDITIONAL' => 1,
+                        'AM_MAINTAINER_MODE' => 1,
                         'LT_INIT' => 1,
-                        'AC_LIBSOURCE' => 1,
-                        'AC_REQUIRE_AUX_FILE' => 1,
-                        'AC_SUBST_TRACE' => 1,
-                        'AM_GNU_GETTEXT' => 1,
-                        '_AM_SUBST_NOTMAKE' => 1,
+                        '_AM_COND_ELSE' => 1,
+                        'AC_CONFIG_LIBOBJ_DIR' => 1,
+                        '_AM_COND_ENDIF' => 1,
+                        'AM_SILENT_RULES' => 1,
                         'AM_PROG_CXX_C_O' => 1,
-                        'AC_DEFINE_TRACE_LITERAL' => 1,
-                        'AM_PROG_MOC' => 1,
+                        'AC_INIT' => 1,
+                        'AC_CONFIG_FILES' => 1,
+                        'AM_NLS' => 1,
+                        'AC_CANONICAL_TARGET' => 1,
+                        'AC_CANONICAL_HOST' => 1,
+                        'm4_pattern_allow' => 1,
+                        'AM_GNU_GETTEXT' => 1,
                         'AC_FC_PP_SRCEXT' => 1,
-                        'AM_MAKEFILE_INCLUDE' => 1,
+                        'AC_FC_FREEFORM' => 1,
+                        'AC_FC_PP_DEFINE' => 1,
+                        'LT_SUPPORTED_TAG' => 1,
+                        'AM_PATH_GUILE' => 1,
+                        'AM_ENABLE_MULTILIB' => 1,
+                        'AM_POT_TOOLS' => 1,
+                        'sinclude' => 1,
+                        'AC_DEFINE_TRACE_LITERAL' => 1,
                         'm4_pattern_forbid' => 1,
-                        'AC_CANONICAL_BUILD' => 1,
-                        'AC_SUBST' => 1,
-                        'AC_CONFIG_SUBDIRS' => 1,
                         'AC_CONFIG_HEADERS' => 1,
-                        'AC_CONFIG_AUX_DIR' => 1,
-                        'AC_CONFIG_LIBOBJ_DIR' => 1,
-                        'AC_FC_PP_DEFINE' => 1,
+                        'AC_REQUIRE_AUX_FILE' => 1,
                         'AC_CONFIG_LINKS' => 1,
-                        'AH_OUTPUT' => 1,
-                        '_LT_AC_TAGCONFIG' => 1,
-                        'AM_XGETTEXT_OPTION' => 1,
-                        'AM_SILENT_RULES' => 1,
-                        'AC_CANONICAL_HOST' => 1,
-                        'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
-                        '_m4_warn' => 1,
-                        'AC_INIT' => 1,
-                        'm4_include' => 1,
-                        'AM_MAINTAINER_MODE' => 1,
-                        'AM_NLS' => 1,
-                        'AC_FC_SRCEXT' => 1,
+                        'AC_SUBST_TRACE' => 1,
+                        'AC_LIBSOURCE' => 1,
                         'AC_PROG_LIBTOOL' => 1,
-                        'AM_PATH_GUILE' => 1,
-                        'AC_CANONICAL_SYSTEM' => 1,
-                        'include' => 1,
+                        'AC_FC_SRCEXT' => 1,
+                        'AM_AUTOMAKE_VERSION' => 1,
                         'LT_CONFIG_LTDL_DIR' => 1,
+                        'AM_MAKEFILE_INCLUDE' => 1,
+                        'include' => 1,
                         'AM_INIT_AUTOMAKE' => 1,
-                        '_AM_COND_ENDIF' => 1,
-                        'AM_PROG_FC_C_O' => 1,
-                        'sinclude' => 1,
-                        'm4_pattern_allow' => 1,
-                        'AM_PROG_CC_C_O' => 1,
-                        'AC_FC_FREEFORM' => 1,
-                        'LT_SUPPORTED_TAG' => 1,
-                        '_AM_COND_ELSE' => 1,
-                        'AC_CANONICAL_TARGET' => 1
+                        'AC_CANONICAL_SYSTEM' => 1,
+                        '_AM_SUBST_NOTMAKE' => 1,
+                        'AC_SUBST' => 1,
+                        'AC_CONFIG_SUBDIRS' => 1,
+                        'AH_OUTPUT' => 1,
+                        'AC_CONFIG_AUX_DIR' => 1,
+                        '_m4_warn' => 1,
+                        'AM_PROG_FC_C_O' => 1
                       }
                     ], 'Autom4te::Request' )
            );

src/backends/C/c_backend.ml

@@ -29,7 +29,7 @@ let gen_files funs basename prog machines dependencies =
   let destname = !Options.dest_dir ^ "/" ^ basename in
   let source_main_file = destname ^ "_main.c" in (* Could be changed *)
   let makefile_file = destname ^ ".makefile" in (* Could be changed *)
-  
+
   let print_header, print_lib_c, print_main_c, print_makefile = funs in
 
   (* Generating H file *)
@@ -38,7 +38,7 @@ let gen_files funs basename prog machines dependencies =
   let header_fmt = formatter_of_out_channel header_out in
   print_header header_fmt basename prog machines dependencies;
   close_out header_out;
-  
+
   (* Generating Lib C file *)
   let source_lib_file = destname ^ ".c" in (* Could be changed *)
   let source_lib_out = open_out source_lib_file in
@@ -63,7 +63,7 @@ let gen_files funs basename prog machines dependencies =
 
       (* Generating Main C file *)
       print_main_c source_main_fmt m basename prog machines dependencies;
-      
+
       (* Generating Makefile *)
       print_makefile basename main_node dependencies makefile_fmt;
 
@@ -86,13 +86,13 @@ let translate_to_c basename prog machines dependencies =
     let module SourceMain = C_backend_main.Main (SourceMainMod) in
     let module Makefile = C_backend_makefile.Main (MakefileMod) in
 
-    let funs = 
-      Header.print_alloc_header, 
-      Source.print_lib_c, 
-      SourceMain.print_main_c, 
-      Makefile.print_makefile 
+    let funs =
+      Header.print_alloc_header,
+      Source.print_lib_c,
+      SourceMain.print_main_c,
+      Makefile.print_makefile
     in
-    gen_files funs basename prog machines dependencies 
+    gen_files funs basename prog machines dependencies
 
   end
   | "acsl" -> begin
@@ -107,13 +107,13 @@ let translate_to_c basename prog machines dependencies =
     let module SourceMain = C_backend_main.Main (SourceMainMod) in
     let module Makefile = C_backend_makefile.Main (MakefileMod) in
 
-    let funs = 
-      Header.print_alloc_header, 
+    let funs =
+      Header.print_alloc_header,
       Source.print_lib_c,
       SourceMain.print_main_c,
-      Makefile.print_makefile 
+      Makefile.print_makefile
     in
-    gen_files funs basename prog machines dependencies 
+    gen_files funs basename prog machines dependencies
 
   end
   | "c" -> begin

src/backends/Horn/horn_backend.ml

@@ -48,6 +48,15 @@ if !Options.main_node <> "" then
     )
 end
 
+
+let load_file f =
+  let ic = open_in f in
+  let n = in_channel_length ic in
+  let s = String.create n in
+  really_input ic s 0 n;
+  close_in ic;
+  (s)
+
 let print_type_definitions fmt =
   let cpt_type = ref 0 in
   Hashtbl.iter (fun typ decl ->
@@ -68,8 +77,25 @@ let print_type_definitions fmt =
     | _        -> ()) type_table
 
 
-let translate fmt basename prog machines =
+
+
+let print_dep fmt prog =
+  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,");
+  fprintf fmt "; Statically linked libraries@";
+  let dependencies = Corelang.get_dependencies prog in
+  List.iter
+    (fun dep ->
+      let (local, s) = Corelang.dependency_of_top dep in
+      let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in
+      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);
+      let horn = load_file basename in
+      fprintf fmt "@.%s@." horn;
+    )
+    dependencies
+
+let translate fmt basename prog machines=
   (* We print typedef *)
+  print_dep fmt prog;
   print_type_definitions fmt;
   List.iter (print_machine machines fmt) (List.rev machines);
   main_print machines fmt

src/compiler_common.ml

@@ -10,7 +10,7 @@
 (********************************************************************)
 
 open Utils
-open Format 
+open Format
 open LustreSpec
 open Corelang
 
@@ -50,7 +50,7 @@ let parse_header own filename =
       close_in h_in;
       header
     with
-    | (Parse.Error err) as exc -> 
+    | (Parse.Error err) as exc ->
       Parse.report_error err;
       raise exc
     | Corelang.Error (loc, err) as exc -> (
@@ -68,7 +68,7 @@ let parse_source source_name =
   Location.init lexbuf source_name;
 
   (* Parsing *)
-  Log.report ~level:1 
+  Log.report ~level:1
     (fun fmt -> fprintf fmt ".. parsing source file %s@," source_name);
   try
     let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in
@@ -76,7 +76,7 @@ let parse_source source_name =
     close_in s_in;
     prog
   with
-  | (Parse.Error err) as exc -> 
+  | (Parse.Error err) as exc ->
     Parse.report_error err;
     raise exc
   | Corelang.Error (loc, err) as exc ->
@@ -115,9 +115,9 @@ let force_stateful_decls decls =
       Location.pp_loc loc;
     raise exc
 
-let type_decls env decls =  
+let type_decls env decls =
   Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
-  let new_env = 
+  let new_env =
     begin
       try
 	Typing.type_prog env decls
@@ -126,13 +126,13 @@ let type_decls env decls =
 	  Types.pp_error err
 	  Location.pp_loc loc;
 	raise exc
-    end 
+    end
   in
   if !Options.print_types then
     Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
   new_env
-      
-let clock_decls env decls = 
+
+let clock_decls env decls =
   Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ ");
   let new_env =
     begin
@@ -221,7 +221,7 @@ let check_compatibility (prog, computed_types_env, computed_clocks_env) (header,
 let is_stateful topdecl =
   match topdecl.top_decl_desc with
   | Node nd -> (match nd.node_stateless with Some b -> not b | None -> not nd.node_dec_stateless)
-  | ImportedNode nd -> not nd.nodei_stateless 
+  | ImportedNode nd -> not nd.nodei_stateless
   | _ -> false
 
 
@@ -248,4 +248,3 @@ let import_dependencies prog =
     Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
     deps
   end
-

src/main_lustre_compiler.ml

@@ -15,7 +15,7 @@ open Log
 open Utils
 open LustreSpec
 open Compiler_common
- 
+
 exception StopPhase1 of program
 
 let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
@@ -88,14 +88,14 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
   end
 
 
-let functional_backend () = 
+let functional_backend () =
   match !Options.output with
   | "horn" | "lustre" | "acsl" -> true
   | _ -> false
 
 (* From prog to prog *)
 let stage1 prog dirname basename =
-  (* Removing automata *) 
+  (* Removing automata *)
   let prog = expand_automata prog in
 
   Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
@@ -137,12 +137,12 @@ let stage1 prog dirname basename =
        exported as a lusi *)
     raise (StopPhase1 prog);
 
- (* Optimization of prog: 
-     - Unfold consts 
+ (* Optimization of prog:
+     - Unfold consts
      - eliminate trivial expressions
  *)
   (*
-  let prog = 
+  let prog =
     if !Options.const_unfold || !Options.optimization >= 5 then
       begin
 	Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
@@ -193,7 +193,7 @@ let stage1 prog dirname basename =
 	!Options.main_node
 	orig prog type_env clock_env
     end;
-  
+
   (* Computes and stores generic calls for each node,
      only useful for ANSI C90 compliant generic node compilation *)
   if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
@@ -233,7 +233,7 @@ let stage1 prog dirname basename =
   prog, dependencies
 
 (* from source to machine code, with optimization *)
-let stage2 prog =    
+let stage2 prog =
   (* Computation of node equation scheduling. It also breaks dependency cycles
      and warns about unused input or memory variables *)
   Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
@@ -245,7 +245,7 @@ let stage2 prog =
   Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
 
 
-  (* TODO Salsa optimize prog: 
+  (* TODO Salsa optimize prog:
      - emits warning for programs with pre inside expressions
      - make sure each node arguments and memory is bounded by a local annotation
      - introduce fresh local variables for each real pure subexpression
@@ -269,7 +269,7 @@ let stage2 prog =
       machine_code
   in
   (* Optimize machine code *)
-  let machine_code, removed_table = 
+  let machine_code, removed_table =
     if !Options.optimization >= 2 && !Options.output <> "horn" then
       begin
 	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: constants inlining@,");
@@ -277,9 +277,9 @@ let stage2 prog =
       end
     else
       machine_code, IMap.empty
-  in  
+  in
   (* Optimize machine code *)
-  let machine_code = 
+  let machine_code =
     if !Options.optimization >= 3 && !Options.output <> "horn" then
       begin
 	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
@@ -290,10 +290,10 @@ let stage2 prog =
     else
       machine_code
   in
-  
+
   (* Salsa optimize machine code *)
   (*
-  let machine_code = 
+  let machine_code =
     if !Options.salsa_enabled then
       begin
 	check_main ();
@@ -305,11 +305,11 @@ let stage2 prog =
 	    | Const c when Types.is_real_type c.const_type  ->
 	      (c.const_id, c.const_value) :: accu
 	    | _ -> accu
-	) [] (Corelang.get_consts prog) 
+	) [] (Corelang.get_consts prog)
 	in
-	List.map 
-	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) 
-	  machine_code 
+	List.map
+	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)
+	  machine_code
       end
     else
       machine_code
@@ -325,7 +325,7 @@ let stage2 prog =
 let stage3 prog machine_code dependencies basename =
   let basename    =  Filename.basename basename in
   match !Options.output with
-    "C" -> 
+    "C" ->
       begin
 	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
 	C_backend.translate_to_c
@@ -387,8 +387,8 @@ let rec compile_source dirname basename extension =
     else
       prog
   in
-  let prog, dependencies = 
-    try 
+  let prog, dependencies =
+    try
       stage1 prog dirname basename
     with StopPhase1 prog -> (
       if !Options.lusi then
@@ -404,8 +404,8 @@ let rec compile_source dirname basename extension =
     )
   in
 
-  let machine_code = 
-    stage2 prog 
+  let machine_code =
+    stage2 prog
   in
   if Scopes.Plugin.show_scopes () then
     begin
@@ -415,16 +415,16 @@ let rec compile_source dirname basename extension =
 	Format.printf "Possible scopes are:@   ";
       Format.printf "@[<v>%a@ @]@.@?" Scopes.print_scopes all_scopes;
       exit 0
-	
+
     end;
 
-  let machine_code = 
+  let machine_code =
     if Scopes.Plugin.is_active () then
       Scopes.Plugin.process_scopes !Options.main_node prog machine_code
     else
       machine_code
   in
-  
+
   stage3 prog machine_code dependencies basename;
   Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
     (* We stop the process here *)
@@ -457,14 +457,14 @@ let _ =
   try
     Printexc.record_backtrace true;
 
-    let options = Options.options @ 
+    let options = Options.options @
       List.flatten (
 	List.map Options.plugin_opt [
 	  Scopes.Plugin.name, Scopes.Plugin.activate, Scopes.Plugin.options
 	]
       )
     in
-    
+
     Arg.parse options anonymous usage
   with
   | Parse.Error _