Arrays

src/Makefile

-OCAMLBUILD=/opt/local/bin/ocamlbuild -classic-display -no-links 
+OCAMLBUILD=/usr/bin/ocamlbuild -classic-display -no-links 
 
 prefix=/usr/local
 exec_prefix=${prefix}

src/backends/Horn/horn_backend_common.ml

@@ -25,8 +25,8 @@ let rec pp_type fmt t =
   | Types.Treal           -> fprintf fmt "Real"
   | Types.Tconst ty       -> pp_print_string fmt ty
   | Types.Tclock t        -> pp_type fmt t
-  | Types.Tarray _
-  | Types.Tstatic _
+  | Types.Tarray(dim,ty)   -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
+  | Types.Tstatic(d, ty)-> pp_type fmt ty
   | Types.Tarrow _
   | _                     -> eprintf "internal error: pp_type %a@."
     Types.print_ty t; assert false

src/backends/Horn/horn_backend_printers.ml

@@ -21,17 +21,17 @@ open Corelang
 open Machine_code
 
 open Horn_backend_common
-
+open Types
 
 (********************************************************************************************)
 (*                    Instruction Printing functions                                        *)
 (********************************************************************************************)
 
 let pp_horn_var m fmt id =
-  if Types.is_array_type id.var_type
+  (*if Types.is_array_type id.var_type
   then
     assert false (* no arrays in Horn output *)
-  else
+  else*)
     fprintf fmt "%s" id.var_id
 
 (* Used to print boolean constants *)
@@ -47,6 +47,65 @@ let rec pp_horn_const fmt c =
     | Const_tag t    -> pp_horn_tag fmt t
     | _              -> assert false
 
+let rec get_type_cst c =
+  match c with
+  | Const_int(n) -> new_ty Tint
+  | Const_real(x) -> new_ty Treal
+  | Const_float(f) -> new_ty Treal
+  | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type_cst (List.hd l)))
+  | Const_tag(tag) -> new_ty Tbool
+  | Const_string(str) ->  assert false(* used only for annotations *)
+  | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l))
+
+let rec get_type v = 
+  match v with
+  | Cst c -> get_type_cst c             
+  | Access(tab, index) -> begin
+                           let rec remove_link ltype = match (dynamic_type ltype).tdesc with 
+                             | Tlink t -> t
+                             | _ -> ltype
+                           in
+                            match (dynamic_type (remove_link (get_type tab))).tdesc with
+                            | Tarray(size, t) -> remove_link t
+                            | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
+                            | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
+                            | _ -> Format.eprintf "Type of access is not an array "; assert false
+                          end
+  | Power(v, n) -> assert false
+  | LocalVar v -> v.var_type
+  | StateVar v -> v.var_type
+  | Fun(n, vl) -> begin match n with
+                  | "+" 
+                  | "-" 
+                  | "*" -> get_type (List.hd vl)
+                  | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
+                  end
+  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type (List.hd l)))
+  | _ -> assert false
+
+
+let rec default_val fmt t =
+  match (dynamic_type t).tdesc with
+  | Tint -> fprintf fmt "0"
+  | Treal -> fprintf fmt "0"
+  | Tbool -> fprintf fmt "true"
+  | Tarray(dim, l) -> let valt = array_element_type t in
+                      fprintf fmt "((as const (Array Int ";
+                      begin try
+                        pp_type fmt valt
+                      with
+                      | _ -> fprintf fmt "failed"; end;
+                      fprintf fmt ")) ";
+                      begin try
+                        default_val fmt valt
+                      with
+                      | _ -> fprintf fmt "failed"; end;
+                      fprintf fmt ")"
+  | Tstruct(l) -> assert false
+  | Ttuple(l) -> assert false
+  |_ -> assert false
+
+
 (* Prints a value expression [v], with internal function calls only.
    [pp_var] is a printer for variables (typically [pp_c_var_read]),
    but an offset suffix may be added for array variables
@@ -54,13 +113,19 @@ let rec pp_horn_const fmt c =
 let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
   match v with
     | Cst c         -> pp_horn_const fmt c
-    | Array _
-    | Access _ -> assert false (* no arrays *)
+    | Array initlist       -> (*Format.fprintf err_formatter "init %a" (pp_horn_val ~is_lhs:is_lhs self pp_var) (List.hd initlist);*)
+                              let rec print tab x =
+                                match tab with
+                                | [] -> default_val fmt (get_type v)(*fprintf fmt "YAY"*)
+                                | h::t -> fprintf fmt "(store "; print t (x+1); fprintf fmt " %i " x; pp_horn_val ~is_lhs:is_lhs self pp_var fmt h; fprintf fmt ")" 
+                              in
+                              print initlist 0
+    | Access(tab,index)      -> fprintf fmt "(select "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt tab; fprintf fmt " "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt index; fprintf fmt ")"
     | Power (v, n)  -> assert false
     | LocalVar v    -> pp_var fmt (rename_machine self v)
     | StateVar v    ->
       if Types.is_array_type v.var_type
-      then assert false
+      then begin assert false; eprintf "toto called\n";fprintf fmt "TOTO" end
       else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
     | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
 

src/main_lustre_compiler.ml

@@ -316,7 +316,8 @@ let rec compile_source dirname basename extension =
       end
     | "horn" ->
       begin
-	let source_file = destname ^ ".smt2" in (* Could be changed *)
+	let source_file = if !Options.dest_file ="" then destname ^ ".smt2" else !Options.dest_file in (* Could be changed *)
+        Printf.eprintf "\n\nOut = %s\n\nOption is : %s\n\n" source_file !Options.dest_file;
 	let source_out = open_out source_file in
 	let fmt = formatter_of_out_channel source_out in
 	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
@@ -355,6 +356,7 @@ let compile dirname basename extension =
   | _        -> assert false
 
 let anonymous filename =
+  Printf.eprintf "\n\nAnonymous called with : %s\n" filename;
   let ok_ext, ext = List.fold_left
     (fun (ok, ext) ext' ->
       if not ok && Filename.check_suffix filename ext' then
@@ -373,7 +375,9 @@ let _ =
   Corelang.add_internal_funs ();
   try
     Printexc.record_backtrace true;
-    Arg.parse Options.options anonymous usage
+    Printf.eprintf "\nParsing\n";
+    Arg.parse Options.options anonymous usage;
+    Printf.eprintf "\nDest=%s\n" !Options.dest_file
   with
   | Parse.Syntax_err _ | Lexer_lustre.Error _
   | Types.Error (_,_) | Clocks.Error (_,_)

src/options.ml

@@ -38,11 +38,12 @@ let traces = ref false
 let horntraces = ref false
 let horn_cex = ref false
 let horn_query = ref true
-
+let dest_file = ref ""
 
 let options =
   [ "-d", Arg.Set_string dest_dir,
     "uses the specified directory as root for generated/imported object and C files (default: .)";
+    "-out", Arg.Set_string dest_file, "Destination file for horn output";
     "-node", Arg.Set_string main_node, "specifies the main node";
     "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
     "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
@@ -65,8 +66,9 @@ let options =
     "-print_clocks", Arg.Set print_clocks, "prints node clocks";
     "-O", Arg.Set_int optimization, " changes optimization level <default: 2>";
     "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
-    "-version", Arg.Unit print_version, " displays the version";]
-
+    "-version", Arg.Unit print_version, " displays the version"
+    ]
+ 
 
 let get_witness_dir filename =
   (* Make sure the directory exists *)