plugin/arithSig.ml

   1
   2 (** This module defines parameterized arithmetic expressions, i.e. arithmetic
   3     expressions mixed with any other type. For instance, one can define
   4     arithmetic expressions with function calls, arithmetic expressions with top
   5     and bottom (the abstract interpretation constants), etc. *)
   6
   7 (* Note: the feature 'mixed with any other type' is not used anymore. It would
   8    make the code clearer to remove it. *)
   9
  10
  11 module P = struct
  12
  13   type relation = Lt | Gt | Le | Ge
  14
  15   let is_large = function
  16     | Le | Ge -> true
  17     | Lt | Gt -> false
  18
  19   let has_lower_type = function
  20     | Lt | Le -> true
  21     | Gt | Ge -> false
  22
  23   let string_of_relation = function
  24     | Lt -> "<"
  25     | Le -> "<="
  26     | Gt -> ">"
  27     | Ge -> ">="
  28
  29   let mk_strict = function
  30     | Lt | Le -> Lt
  31     | Gt | Ge -> Gt
  32
  33   let mk_large = function
  34     | Lt | Le -> Le
  35     | Gt | Ge -> Ge
  36
  37   let opposite = function
  38     | Lt -> Ge
  39     | Le -> Gt
  40     | Gt -> Le
  41     | Ge -> Lt
  42
  43   type unop = Neg
  44
  45   type binop = Add | Sub | Div | Mul | Mod | Max
  46
  47   let string_of_unop = function
  48     | Neg -> "-"
  49
  50   let string_of_binop = function
  51     | Add -> "+"
  52     | Sub -> "-"
  53     | Div -> "/"
  54     | Mul -> "*"
  55     | Mod -> "%"
  56     | Max -> "max"
  57
  58   type 'a tt =
  59     | A of 'a
  60     | Int of int
  61     | Var of string
  62     | UnOp of unop * 'a tt
  63     | BinOp of binop * 'a tt * 'a tt
  64     | Cond of 'a tt * relation * 'a tt * 'a tt * 'a tt (* ternary expressions *)
  65
  66   let compare compare_a v1 v2 = match v1, v2 with
  67     | A a1, A a2 -> compare_a a1 a2
  68     | A _, _ -> -1
  69     | _, A _ -> 1
  70     | _ -> Pervasives.compare v1 v2
  71
  72   let rec map f = function
  73     | A a -> A (f a)
  74     | Int i -> Int i
  75     | Var x -> Var x
  76     | UnOp (unop, v) -> UnOp (unop, map f v)
  77     | BinOp (binop, v1, v2) -> BinOp (binop, map f v1, map f v2)
  78     | Cond (v1, rel, v2, v3, v4) ->
  79       Cond (map f v1, rel, map f v2, map f v3, map f v4)
  80
  81   let fill_subs v subs = match v, subs with
  82     | A _, _ | Int _, _ | Var _, _ -> v
  83     | UnOp (unop, _), v :: _ -> UnOp (unop, v)
  84     | BinOp (binop, _, _), v1 :: v2 :: _ -> BinOp (binop, v1, v2)
  85     | Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ ->
  86       Cond (t1, rel, t2, tif, telse)
  87     | _ -> raise (Failure "ArithSig.fill_subs") (* wrong number of arguments *)
  88
  89   let subs = function
  90     | A _ | Int _ | Var _ -> []
  91     | UnOp (_, v) -> [v]
  92     | BinOp (_, v1, v2) -> [v1 ; v2]
  93     | Cond (t1, _, t2, tif, telse) -> [t1 ; t2 ; tif ; telse]
  94
  95   let rec fold f v =
  96     let subs_res = List.map (fold f) (subs v) in
  97     f v subs_res
  98
  99   let f_is_independent v subs_res =
 100     let b = match v with A _ -> false | _ -> true in
 101     List.fold_left (&&) true (b :: subs_res)
 102
 103   (** [is_independent v] returns true if and only if the arithmetic expression
 104       [v] does not mention a value of its parameter type. *)
 105
 106   let is_independent v = fold f_is_independent v
 107
 108   let f_replace replacements v subs_res =
 109     let v = match v with
 110       | Var x when List.mem_assoc x replacements -> List.assoc x replacements
 111       | _ -> v in
 112     fill_subs v subs_res
 113
 114   let replace replacements v = fold (f_replace replacements) v
 115
 116 end
 117
 118 include P
 119
 120
 121 module type S = sig
 122   type t
 123
 124   val to_string : t -> string
 125   val to_cil_term : t -> Cil_types.term
 126
 127   val compute : t -> t
 128   val neg : t -> t tt
 129   val addl : t -> t tt -> t tt
 130   val addr : t tt -> t -> t tt
 131   val minusl : t -> t tt -> t tt
 132   val minusr : t tt -> t -> t tt
 133   val mull : t -> t tt -> t tt
 134   val mulr : t tt -> t -> t tt
 135   val divl : t -> t tt -> t tt
 136   val divr : t tt -> t -> t tt
 137   val modl : t -> t tt -> t tt
 138   val modr : t tt -> t -> t tt
 139   val maxl : t -> t tt -> t tt
 140   val maxr : t tt -> t -> t tt
 141   val lel : t -> t tt -> bool
 142   val ler : t tt -> t -> bool
 143   val ltl : t -> t tt -> bool
 144   val ltr : t tt -> t -> bool
 145   val gel : t -> t tt -> bool
 146   val ger : t tt -> t -> bool
 147   val gtl : t -> t tt -> bool
 148   val gtr : t tt -> t -> bool
 149
 150   val compare : t -> t -> int
 151 end