Project

General

Profile

Revision fa91d4d0 src/backends/Horn/horn_backend_printers.ml

View differences:

src/backends/Horn/horn_backend_printers.ml
46 46
    | Const_tag t    -> pp_horn_tag fmt t
47 47
    | _              -> assert false
48 48

  
49
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *)
50
(* let rec get_type_cst c = *)
51
(*   match c with *)
52
(*   | Const_int(n) -> new_ty Tint *)
53
(*   | Const_real _ -> new_ty Treal *)
54
(*   (\* | Const_float _ -> new_ty Treal *\) *)
55
(*   | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *)
56
(* 				     get_type_cst (List.hd l))) *)
57
(*   | Const_tag(tag) -> new_ty Tbool *)
58
(*   | Const_string(str) ->  assert false(\* used only for annotations *\) *)
59
(*   | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *)
60

  
61
(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *)
62

  
63
(*
64
let rec get_type v =
65
  match v with
66
  | Cst c -> Typing.type_const Location.dummy_loc c (* get_type_cst c*)
67
  | Access(tab, index) -> begin
68
      let rec remove_link ltype =
69
        match (dynamic_type ltype).tdesc with
70
        | Tlink t -> t
71
        | _ -> ltype
72
      in
73
      match (dynamic_type (remove_link (get_type tab))).tdesc with
74
      | Tarray(size, t) -> remove_link t
75
      | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
76
      | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
77
      | _ -> Format.eprintf "Type of access is not an array "; assert false
78
                          end
79
  | Power(v, n) -> assert false
80
  | LocalVar v -> v.var_type
81
  | StateVar v -> v.var_type
82
  | Fun(n, vl) -> begin match n with
83
                  | "+"
84
                  | "-"
85
                  | "*" -> get_type (List.hd vl)
86
                  | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
87
                  end
88
  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int
89
                                 (Location.dummy_loc)
90
                                 (List.length l),
91
                               get_type (List.hd l)))
92
  | _ -> assert false
93
*)
94

  
95 49
(* Default value for each type, used when building arrays. Eg integer array
96 50
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
97 51
   for the type integer (arrays).
......
111 65
  | Types.Ttuple(l) -> assert false
112 66
  |_ -> assert false
113 67

  
68
let pp_mod pp_val v1 v2 fmt =
69
  if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
70
    (* C semantics: converting it to Euclidian operators
71
       (a mod_M b) - (a < 0 ? abs(b) : 0)            
72
    *)
73
    Format.fprintf fmt "(- (mod %a %a) (ite (< %a 0) (abs %a) 0))"
74
      pp_val v1 pp_val v2 pp_val v1 pp_val v2
75
  else
76
    Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
77

  
78
let pp_div pp_val v1 v2 fmt =
79
  if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
80
    (* C semantics: converting it to Euclidian operators
81
       (a - ((a mod_M b) - (a < 0 ? abs(b) : 0))) div_M b
82
    *)
83
    Format.fprintf fmt "(div (- %a (- (mod %a %a) (ite (< %a 0) (abs %a) 0))) %a)"
84
      pp_val v1 pp_val v1 pp_val v2
85
      pp_val v1 pp_val v2 pp_val v2
86
  else
87
    Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
88

  
114 89

  
115 90
let pp_basic_lib_fun i pp_val fmt vl =
116 91
  match i, vl with
117 92
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
118

  
119 93
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
120 94
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
121 95
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
122 96
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
123 97
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
124 98
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
125
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
126 99
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
127 100
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
128 101
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
129
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
102
  | "mod", [v1; v2] -> pp_mod pp_val v1 v2 fmt
103
  | "/", [v1; v2] -> pp_div pp_val v1 v2 fmt
130 104
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
131 105
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
132 106
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2

Also available in: Unified diff