Project

General

Profile

« Previous | Next » 

Revision 84902260

Added by jbraine almost 6 years ago

Arrays

View differences:

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