Revision 84902260
Added by jbraine almost 6 years ago
| src/Makefile | ||
|---|---|---|
| 1 |
OCAMLBUILD=/opt/local/bin/ocamlbuild -classic-display -no-links
|
|
| 1 |
OCAMLBUILD=/usr/bin/ocamlbuild -classic-display -no-links
|
|
| 2 | 2 |
|
| 3 | 3 |
prefix=/usr/local |
| 4 | 4 |
exec_prefix=${prefix}
|
| src/backends/Horn/horn_backend_common.ml | ||
|---|---|---|
| 25 | 25 |
| Types.Treal -> fprintf fmt "Real" |
| 26 | 26 |
| Types.Tconst ty -> pp_print_string fmt ty |
| 27 | 27 |
| Types.Tclock t -> pp_type fmt t |
| 28 |
| Types.Tarray _
|
|
| 29 |
| Types.Tstatic _
|
|
| 28 |
| Types.Tarray(dim,ty) -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
|
|
| 29 |
| Types.Tstatic(d, ty)-> pp_type fmt ty
|
|
| 30 | 30 |
| Types.Tarrow _ |
| 31 | 31 |
| _ -> eprintf "internal error: pp_type %a@." |
| 32 | 32 |
Types.print_ty t; assert false |
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 21 | 21 |
open Machine_code |
| 22 | 22 |
|
| 23 | 23 |
open Horn_backend_common |
| 24 |
|
|
| 24 |
open Types |
|
| 25 | 25 |
|
| 26 | 26 |
(********************************************************************************************) |
| 27 | 27 |
(* Instruction Printing functions *) |
| 28 | 28 |
(********************************************************************************************) |
| 29 | 29 |
|
| 30 | 30 |
let pp_horn_var m fmt id = |
| 31 |
if Types.is_array_type id.var_type |
|
| 31 |
(*if Types.is_array_type id.var_type
|
|
| 32 | 32 |
then |
| 33 | 33 |
assert false (* no arrays in Horn output *) |
| 34 |
else |
|
| 34 |
else*)
|
|
| 35 | 35 |
fprintf fmt "%s" id.var_id |
| 36 | 36 |
|
| 37 | 37 |
(* Used to print boolean constants *) |
| ... | ... | |
| 47 | 47 |
| Const_tag t -> pp_horn_tag fmt t |
| 48 | 48 |
| _ -> assert false |
| 49 | 49 |
|
| 50 |
let rec get_type_cst c = |
|
| 51 |
match c with |
|
| 52 |
| Const_int(n) -> new_ty Tint |
|
| 53 |
| Const_real(x) -> new_ty Treal |
|
| 54 |
| Const_float(f) -> new_ty Treal |
|
| 55 |
| Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type_cst (List.hd l))) |
|
| 56 |
| Const_tag(tag) -> new_ty Tbool |
|
| 57 |
| Const_string(str) -> assert false(* used only for annotations *) |
|
| 58 |
| Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) |
|
| 59 |
|
|
| 60 |
let rec get_type v = |
|
| 61 |
match v with |
|
| 62 |
| Cst c -> get_type_cst c |
|
| 63 |
| Access(tab, index) -> begin |
|
| 64 |
let rec remove_link ltype = match (dynamic_type ltype).tdesc with |
|
| 65 |
| Tlink t -> t |
|
| 66 |
| _ -> ltype |
|
| 67 |
in |
|
| 68 |
match (dynamic_type (remove_link (get_type tab))).tdesc with |
|
| 69 |
| Tarray(size, t) -> remove_link t |
|
| 70 |
| Tvar -> Format.eprintf "Type of access is a variable... "; assert false |
|
| 71 |
| Tunivar -> Format.eprintf "Type of access is a variable... "; assert false |
|
| 72 |
| _ -> Format.eprintf "Type of access is not an array "; assert false |
|
| 73 |
end |
|
| 74 |
| Power(v, n) -> assert false |
|
| 75 |
| LocalVar v -> v.var_type |
|
| 76 |
| StateVar v -> v.var_type |
|
| 77 |
| Fun(n, vl) -> begin match n with |
|
| 78 |
| "+" |
|
| 79 |
| "-" |
|
| 80 |
| "*" -> get_type (List.hd vl) |
|
| 81 |
| _ -> Format.eprintf "Function undealt with : %s" n ;assert false |
|
| 82 |
end |
|
| 83 |
| Array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type (List.hd l))) |
|
| 84 |
| _ -> assert false |
|
| 85 |
|
|
| 86 |
|
|
| 87 |
let rec default_val fmt t = |
|
| 88 |
match (dynamic_type t).tdesc with |
|
| 89 |
| Tint -> fprintf fmt "0" |
|
| 90 |
| Treal -> fprintf fmt "0" |
|
| 91 |
| Tbool -> fprintf fmt "true" |
|
| 92 |
| Tarray(dim, l) -> let valt = array_element_type t in |
|
| 93 |
fprintf fmt "((as const (Array Int "; |
|
| 94 |
begin try |
|
| 95 |
pp_type fmt valt |
|
| 96 |
with |
|
| 97 |
| _ -> fprintf fmt "failed"; end; |
|
| 98 |
fprintf fmt ")) "; |
|
| 99 |
begin try |
|
| 100 |
default_val fmt valt |
|
| 101 |
with |
|
| 102 |
| _ -> fprintf fmt "failed"; end; |
|
| 103 |
fprintf fmt ")" |
|
| 104 |
| Tstruct(l) -> assert false |
|
| 105 |
| Ttuple(l) -> assert false |
|
| 106 |
|_ -> assert false |
|
| 107 |
|
|
| 108 |
|
|
| 50 | 109 |
(* Prints a value expression [v], with internal function calls only. |
| 51 | 110 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
| 52 | 111 |
but an offset suffix may be added for array variables |
| ... | ... | |
| 54 | 113 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
| 55 | 114 |
match v with |
| 56 | 115 |
| Cst c -> pp_horn_const fmt c |
| 57 |
| Array _ |
|
| 58 |
| Access _ -> assert false (* no arrays *) |
|
| 116 |
| Array initlist -> (*Format.fprintf err_formatter "init %a" (pp_horn_val ~is_lhs:is_lhs self pp_var) (List.hd initlist);*) |
|
| 117 |
let rec print tab x = |
|
| 118 |
match tab with |
|
| 119 |
| [] -> default_val fmt (get_type v)(*fprintf fmt "YAY"*) |
|
| 120 |
| 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 ")" |
|
| 121 |
in |
|
| 122 |
print initlist 0 |
|
| 123 |
| 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 ")" |
|
| 59 | 124 |
| Power (v, n) -> assert false |
| 60 | 125 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
| 61 | 126 |
| StateVar v -> |
| 62 | 127 |
if Types.is_array_type v.var_type |
| 63 |
then assert false
|
|
| 128 |
then begin assert false; eprintf "toto called\n";fprintf fmt "TOTO" end
|
|
| 64 | 129 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
| 65 | 130 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
| 66 | 131 |
|
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 316 | 316 |
end |
| 317 | 317 |
| "horn" -> |
| 318 | 318 |
begin |
| 319 |
let source_file = destname ^ ".smt2" in (* Could be changed *) |
|
| 319 |
let source_file = if !Options.dest_file ="" then destname ^ ".smt2" else !Options.dest_file in (* Could be changed *) |
|
| 320 |
Printf.eprintf "\n\nOut = %s\n\nOption is : %s\n\n" source_file !Options.dest_file; |
|
| 320 | 321 |
let source_out = open_out source_file in |
| 321 | 322 |
let fmt = formatter_of_out_channel source_out in |
| 322 | 323 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,"); |
| ... | ... | |
| 355 | 356 |
| _ -> assert false |
| 356 | 357 |
|
| 357 | 358 |
let anonymous filename = |
| 359 |
Printf.eprintf "\n\nAnonymous called with : %s\n" filename; |
|
| 358 | 360 |
let ok_ext, ext = List.fold_left |
| 359 | 361 |
(fun (ok, ext) ext' -> |
| 360 | 362 |
if not ok && Filename.check_suffix filename ext' then |
| ... | ... | |
| 373 | 375 |
Corelang.add_internal_funs (); |
| 374 | 376 |
try |
| 375 | 377 |
Printexc.record_backtrace true; |
| 376 |
Arg.parse Options.options anonymous usage |
|
| 378 |
Printf.eprintf "\nParsing\n"; |
|
| 379 |
Arg.parse Options.options anonymous usage; |
|
| 380 |
Printf.eprintf "\nDest=%s\n" !Options.dest_file |
|
| 377 | 381 |
with |
| 378 | 382 |
| Parse.Syntax_err _ | Lexer_lustre.Error _ |
| 379 | 383 |
| Types.Error (_,_) | Clocks.Error (_,_) |
| src/options.ml | ||
|---|---|---|
| 38 | 38 |
let horntraces = ref false |
| 39 | 39 |
let horn_cex = ref false |
| 40 | 40 |
let horn_query = ref true |
| 41 |
|
|
| 41 |
let dest_file = ref "" |
|
| 42 | 42 |
|
| 43 | 43 |
let options = |
| 44 | 44 |
[ "-d", Arg.Set_string dest_dir, |
| 45 | 45 |
"uses the specified directory as root for generated/imported object and C files (default: .)"; |
| 46 |
"-out", Arg.Set_string dest_file, "Destination file for horn output"; |
|
| 46 | 47 |
"-node", Arg.Set_string main_node, "specifies the main node"; |
| 47 | 48 |
"-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>"; |
| 48 | 49 |
"-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>"; |
| ... | ... | |
| 65 | 66 |
"-print_clocks", Arg.Set print_clocks, "prints node clocks"; |
| 66 | 67 |
"-O", Arg.Set_int optimization, " changes optimization level <default: 2>"; |
| 67 | 68 |
"-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>"; |
| 68 |
"-version", Arg.Unit print_version, " displays the version";] |
|
| 69 |
|
|
| 69 |
"-version", Arg.Unit print_version, " displays the version" |
|
| 70 |
] |
|
| 71 |
|
|
| 70 | 72 |
|
| 71 | 73 |
let get_witness_dir filename = |
| 72 | 74 |
(* Make sure the directory exists *) |
Also available in: Unified diff
Arrays