Project

General

Profile

« Previous | Next » 

Revision 84902260

Added by jbraine almost 6 years ago

Arrays

View differences:

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

  

Also available in: Unified diff