plugin/arith.ml

   1
   2 (** This module provides functions to manipulate parameterized arithmetic
   3     expressions (see the ArithSig module) when instanciaded on a specific
   4     type. *)
   5
   6
   7 module Make (S : ArithSig.S) = struct
   8
   9   include ArithSig.P
  10
  11   let compare = compare S.compare
  12
  13   type t = S.t tt
  14
  15   let fill_subs v subs = ArithSig.fill_subs v subs
  16
  17   let subs v = ArithSig.subs v
  18
  19   let fold f v = ArithSig.fold f v
  20
  21
  22   let f_to_string v subs_res = match v, subs_res with
  23     | A a, _ -> "(A " ^ (S.to_string a) ^ ")"
  24     | Int i, _ -> string_of_int i
  25     | Var x, _ -> x
  26     | UnOp (unop, _), v :: _ -> (string_of_unop unop) ^ "(" ^ v ^ ")"
  27     | BinOp (binop, _, _), v1 :: v2 :: _ ->
  28       "(" ^ v1 ^ ")" ^ (string_of_binop binop) ^ "(" ^ v2 ^ ")"
  29     | Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ ->
  30       Printf.sprintf "(%s %s %s)? (%s) : (%s)"
  31         t1 (string_of_relation rel) t2 tif telse
  32     | UnOp _, _ | BinOp _, _ | Cond _, _ ->
  33       assert false (* wrong number of arguments *)
  34
  35   let to_string v = fold f_to_string v
  36
  37
  38   let is_supported_rel = function
  39     | Cil_types.Lt | Cil_types.Gt | Cil_types.Le | Cil_types.Ge -> true
  40     | _ -> false
  41
  42   let rel_of_cil_binop = function
  43     | Cil_types.Lt -> Lt
  44     | Cil_types.Gt -> Gt
  45     | Cil_types.Le -> Le
  46     | Cil_types.Ge -> Ge
  47     | _ -> raise (Failure "Arith.rel_of_cil_binop")
  48
  49
  50   let cil_binop_of_rel = function
  51     | Lt -> Cil_types.Lt
  52     | Gt -> Cil_types.Gt
  53     | Le -> Cil_types.Le
  54     | Ge -> Cil_types.Ge
  55
  56   let cil_unop_of_unop = function
  57     | Neg -> Cil_types.Neg
  58
  59   let cil_binop_of_binop = function
  60     | Add -> Cil_types.PlusA
  61     | Sub -> Cil_types.MinusA
  62     | Mul -> Cil_types.Mult
  63     | Div -> Cil_types.Div
  64     | Mod -> Cil_types.Mod
  65     (* No direct translation. Handle this case in the calling function. *)
  66     | Max -> assert false
  67
  68
  69   let integer_term term = Logic_const.term term Cil_types.Linteger
  70
  71   let tinteger i =
  72     let cint64 = Cil_types.CInt64 (My_bigint.of_int i, Cil_types.IInt, None) in
  73     let iterm = Cil_types.TConst cint64 in
  74     integer_term iterm
  75
  76   let f_to_cil_term v subs_res = match v, subs_res with
  77     | A a, _ ->  S.to_cil_term a
  78     | Int i, _ -> tinteger i
  79     | Var x, _ ->
  80       Logic_const.tvar (Cil_const.make_logic_var x Cil_types.Linteger)
  81     | UnOp (unop, _), t :: _ ->
  82       integer_term (Cil_types.TUnOp (cil_unop_of_unop unop, t))
  83     | BinOp (Max, _, _), t1 :: t2 :: _ ->
  84       let test = integer_term (Cil_types.TBinOp (Cil_types.Ge, t1, t2)) in
  85       integer_term (Cil_types.Tif (test, t1, t2))
  86     | BinOp (binop, _, _), t1 :: t2 :: _ ->
  87       integer_term (Cil_types.TBinOp (cil_binop_of_binop binop, t1, t2))
  88     | Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ ->
  89       let test =
  90         integer_term (Cil_types.TBinOp (cil_binop_of_rel rel, t1, t2)) in
  91       integer_term (Cil_types.Tif (test, tif, telse))
  92     | _ -> assert false (* wrong number of arguments *)
  93
  94   let to_cil_term v = fold f_to_cil_term v
  95
  96
  97   let cil_rel_of_rel = function
  98     | Lt -> Cil_types.Rlt
  99     | Gt -> Cil_types.Rgt
 100     | Le -> Cil_types.Rle
 101     | Ge -> Cil_types.Rge
 102
 103
 104   let of_int i = Int i
 105   let of_var x = Var x
 106
 107   let apply_unop unop v = UnOp (unop, v)
 108   let apply_binop binop v1 v2 = BinOp (binop, v1, v2)
 109
 110   let int_op_of_rel = function
 111     | Lt -> (<)
 112     | Le -> (<=)
 113     | Gt -> (>)
 114     | Ge -> (>=)
 115
 116   (* The functions below allows to build arithmetic expressions with their usual
 117      operators (add, sub, etc) and with a partial simplification. *)
 118
 119   let rec neg = function
 120     | A a -> S.neg a
 121     | Int i -> Int (-i)
 122     | UnOp (Neg, v) -> v
 123     | BinOp (Add, v1, v2) -> add (neg v1) (neg v2)
 124     | BinOp (Sub, v1, v2) -> minus (neg v1) (neg v2)
 125     | v -> apply_unop Neg v
 126
 127   and add v1 v2 = match v1, v2 with
 128     | Int i1, Int i2 -> Int (i1 + i2)
 129     | Int 0, v | v, Int 0 -> v
 130     | BinOp (Add, Int i1, v), Int i2
 131     | BinOp (Add, v, Int i1), Int i2
 132     | Int i1, BinOp (Add, Int i2, v)
 133     | Int i1, BinOp (Add, v, Int i2) -> add (Int (i1 + i2)) v
 134     | BinOp (Sub, Int i1, v), Int i2
 135     | Int i1, BinOp (Sub, Int i2, v) -> minus (Int (i1 + i2)) v
 136     | BinOp (Sub, v, Int i1), Int i2
 137     | Int i1, BinOp (Sub, v, Int i2) -> add (Int (i1 - i2)) v
 138     | A a, v -> S.addl a v
 139     | v, A a -> S.addr v a
 140     | _ -> apply_binop Add v1 v2
 141
 142   and minus v1 v2 = match v1, v2 with
 143     | A a, v -> S.minusl a v
 144     | v, A a -> S.minusr v a
 145     | Int i1, Int i2 -> Int (i1 - i2)
 146     | _, Int 0 -> v1
 147     | Int 0, _ -> neg v2
 148     | _ -> apply_binop Sub v1 v2
 149
 150   and mul v1 v2 = match v1, v2 with
 151     | A a, v -> S.mull a v
 152     | v, A a -> S.mulr v a
 153     | Int i1, Int i2 -> Int (i1 * i2)
 154     | Int 1, v | v, Int 1 -> v
 155     | Int 0, _ | _, Int 0 -> Int 0
 156     | Int (-1), v | v, Int (-1) -> neg v
 157     | _ -> apply_binop Mul v1 v2
 158
 159   and div v1 v2 = match v1, v2 with
 160     | _, Int 0 -> raise (Invalid_argument "Arith.div")
 161     | A a, v -> S.divl a v
 162     | v, A a -> S.divr v a
 163     | Int i1, Int i2 -> Int (i1 / i2)
 164     | Int 1, v | v, Int 1 -> v
 165     | Int 0, _ -> Int 0
 166     | Int (-1), v | v, Int (-1) -> neg v
 167     | _ -> apply_binop Div v1 v2
 168
 169   and modulo v1 v2 = match v1, v2 with
 170     | _, Int 0 -> raise (Invalid_argument "Arith.modulo")
 171     | A a, v -> S.modl a v
 172     | v, A a -> S.modr v a
 173     | Int i1, Int i2 -> Int (i1 mod i2)
 174     | Int 0, _ | _, Int 1 -> Int 0
 175     | _ -> apply_binop Mod v1 v2
 176
 177   and max v1 v2 = match v1, v2 with
 178     | A a, v -> S.maxl a v
 179     | v, A a -> S.maxr v a
 180     | Int i1, Int i2 -> Int (Pervasives.max i1 i2)
 181     | _ -> apply_binop Max v1 v2
 182
 183   and cond v1 rel v2 v3 v4 = match v1, v2 with
 184     | Int i1, Int i2 when (int_op_of_rel rel) i1 i2 -> v3
 185     | Int _, Int _ -> v4
 186     | _ -> Cond (v1, rel, v2, v3, v4)
 187
 188   let cmp is_large cmpal cmpar int_cmp v1 v2 = match v1, v2 with
 189     | Int i1, Int i2 -> int_cmp i1 i2
 190     | A a, v -> cmpal a v
 191     | v, A a -> cmpar v a
 192     | _ when is_large -> v1 = v2
 193     | _ -> false
 194
 195   let binop_false _ _ = false
 196
 197   let lt = cmp false S.ltl S.ltr (<)
 198   let le = cmp true S.lel S.ler (<=)
 199   let gt = cmp false S.gtl S.gtr (>)
 200   let ge = cmp true S.gel S.ger (>=)
 201
 202   let op_of_unop = function
 203     | Neg -> neg
 204
 205   let op_of_binop = function
 206     | Add -> add
 207     | Sub -> minus
 208     | Mul -> mul
 209     | Div -> div
 210     | Mod -> modulo
 211     | Max -> max
 212
 213   let op_of_relation = function
 214     | Lt -> lt
 215     | Le -> le
 216     | Gt -> gt
 217     | Ge -> ge
 218
 219   let bool_of_cond = op_of_relation
 220
 221   let f_compute v subs_res = match v, subs_res with
 222     | A a, _ -> A (S.compute a)
 223     | UnOp (unop, _), v :: _ -> (op_of_unop unop) v
 224     | BinOp (binop, _, _), v1 :: v2 :: _ -> (op_of_binop binop) v1 v2
 225     | Cond (_, rel, _, _, _), v1 :: v2 :: v3 :: _
 226       when (op_of_relation rel) v1 v2 -> v3
 227     | Cond (_, rel, _, _, _), v1 :: v2 :: _ :: v4 :: _
 228       when (op_of_relation (opposite rel)) v1 v2 -> v4
 229     | _ -> fill_subs v subs_res
 230
 231   (** [compute v] partially simplifies the arithmetic expression [v]. *)
 232
 233   let compute v = fold f_compute v
 234
 235   let abs v = cond (Int 0) Le v v (neg v)
 236
 237   let f_replace_vars replacements v subs_res = match fill_subs v subs_res with
 238     | Var x when Misc.String.Map.mem x replacements ->
 239       Misc.String.Map.find x replacements
 240     | v -> v
 241
 242   let replace_vars replacements = fold (f_replace_vars replacements)
 243
 244 end