src/clight/clightUtils.ml

   1
   2 open Clight
   3
   4
   5 (* TODO: Alignment constraints? *)
   6 let rec size_of_ctype = function
   7   | Tvoid               -> 0
   8   | Tint (I8,_)         -> 1
   9   | Tint (I16,_)        -> 2
  10   | Tint (I32,_)        -> 4
  11   | Tfloat _            -> assert false (* Not supported *)
  12   | Tpointer (sp,_)     -> Memory.size_of_region sp
  13   | Tarray (sp,t,s)     -> s*(size_of_ctype t)
  14   | Tfunction (_,_)     -> assert false (* Not supported *)
  15   | Tstruct (_,lst)     ->
  16       List.fold_left (fun n (_,ty) -> n + (size_of_ctype ty)) 0 lst
  17   | Tunion (_,lst)      ->
  18       List.fold_left
  19         (fun n (_,ty)   ->
  20            let sz = (size_of_ctype ty) in (if n>sz then n else sz)
  21         ) 0 lst
  22   | Tcomp_ptr (sp,_)    -> Memory.size_of_region sp
  23
  24
  25 let rec memory_q_of_ctype = function
  26   | Tvoid               -> assert false
  27   | Tint (I8,Signed)    -> Memory.MQ_int8signed
  28   | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
  29   | Tint (I16,Signed)   -> Memory.MQ_int16signed
  30   | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
  31   | Tint (I32,Signed)   -> Memory.MQ_int32
  32   | Tint (I32,Unsigned) -> assert false (* Not supported *)
  33   | Tfloat _            -> assert false (* Not supported *)
  34   | Tpointer (sp,_)     -> Memory.mq_of_region sp
  35   | Tarray (sp,c,s)     -> Memory.mq_of_region sp
  36   | Tfunction (_,_)     -> assert false (* should not happen thanks to CIL *)
  37   | Tstruct (_,_)       -> assert false (* should not happen thanks to CIL *)
  38   | Tunion (_,_)        -> assert false (* should not happen thanks to CIL *)
  39   | Tcomp_ptr (sp,_)    -> Memory.mq_of_region sp
  40
  41
  42 let is_int_type = function
  43   | Tint (_,_)    -> true
  44   | _ -> false
  45
  46 let is_float_type = function
  47   | Tfloat _  -> true
  48   | _ -> false
  49
  50 let is_pointer_type = function
  51   | Tpointer _ | Tarray _ | Tcomp_ptr _ -> true
  52   | _ -> false
  53
  54 let is_stack_type = function
  55   | Tarray _ | Tstruct _ | Tunion _ -> true
  56   | _ -> false
  57
  58 let is_struct = function
  59   | Tstruct _ | Tunion _ -> true
  60   | _ -> false
  61
  62 let is_ptr_to_struct = function
  63   | Tpointer (_,t) when is_struct t -> true
  64   | Tcomp_ptr _ -> true
  65   | _ -> false
  66
  67 let is_function = function
  68   | Tfunction _ -> true
  69   | _ -> false
  70
  71 let region_of_pointer_type = function
  72   | Tpointer (sp,_) | Tarray (sp,_,_) | Tcomp_ptr (sp,_) -> sp
  73   | _ -> assert false (* do not use on those arguments *)