整数区间的逻辑计算

Question

计算逻辑运算的规则是什么？ （与或异或）两个整数间隔？

给定两个时间间隔[A，B]并[c，d] i的要计算[A，B] XOR并[c，d]

我假设的结果是多个范围

我看着在filib ++并阅读WIKI，但发现只是算术操作。支持

谁能教我

Answer 1

您可以找到“按位和”，“按位异或”并在Frama-C最新版本间隔之间“按位或”实现方式，在文件的src/AI/IVAL。毫升。实际上，这些函数对类型为Ival.t的值进行操作，该值代表一小组整数值，具有同余信息的区间或浮点区间。您只会对Top _, Top _（对应于具有同余信息的整数间隔）的情况感兴趣。函数将结果计算为Ival.t，可能是过度逼近的，但其中包含所有值x op y，其中x在第一个区间中，y在第二个区间中。

正如评论所说，pos_max_land的算法对于精度来说是最优的，但对于整数的位数没有最好的复杂度。在完成写入函数后，我只理解了这一点，对于这个用例，整数的宽度不超过64，所以我没有打算写更快的版本。

src/ai/ival.ml文件在LGPL 2.1下许可。如果你做了一些很酷的事情，我会很乐意听到它。

(* [different_bits min max] returns an overapproximation of the mask 
    of the bits that can be different for different numbers 
    in the interval [min]..[max] *) 
let different_bits min max = 
    let x = Int.logxor min max in 
    next_pred_power_of_two x 

(* [pos_max_land min1 max1 min2 max2] computes an upper bound for 
    [x1 land x2] where [x1] is in [min1]..[max1] and [x2] is in [min2]..[max2]. 
    Precondition : [min1], [max1], [min2], [max2] must all have the 
    same sign. 
    Note: the algorithm below is optimal for the problem as stated. 
    It is possible to compute this optimal solution faster but it does not 
    seem worth the time necessary to think about it as long as integers 
    are at most 64-bit. *) 
let pos_max_land min1 max1 min2 max2 = 
    let x1 = different_bits min1 max1 in 
    let x2 = different_bits min2 max2 in 
(*  Format.printf "pos_max_land %a %a -> %a | %a %a -> %a@." 
     Int.pretty min1 Int.pretty max1 Int.pretty x1 
     Int.pretty min2 Int.pretty max2 Int.pretty x2; *) 
    let fold_maxs max1 p f acc = 
    let rec aux p acc = 
     let p = Int.shift_right p Int.one in 
     if Int.is_zero p 
     then f max1 acc 
     else if Int.is_zero (Int.logand p max1) 
     then aux p acc 
     else 
     let c = Int.logor (Int.sub max1 p) (Int.pred p) in 
     aux p (f c acc) 
    in aux p acc 
    in 
    let sx1 = Int.succ x1 in 
    let n1 = fold_maxs max1 sx1 (fun _ y -> succ y) 0 in 
    let maxs1 = Array.make n1 sx1 in 
    let _ = fold_maxs max1 sx1 (fun x i -> Array.set maxs1 i x; succ i) 0 in 
    fold_maxs max2 (Int.succ x2) 
    (fun max2 acc -> 
     Array.fold_left 
     (fun acc max1 -> Int.max (Int.logand max1 max2) acc) 
     acc 
     maxs1) 
    (Int.logand max1 max2) 

let bitwise_or v1 v2 = 
    if is_bottom v1 || is_bottom v2 
    then bottom 
    else 
    match v1, v2 with 
     Float _, _ | _, Float _ -> top 
    | Set s1, Set s2 -> 
     apply2_v Int.logor s1 s2 
    | Set s, v | v, Set s when Array.length s = 1 && Int.is_zero s.(0) -> v 
    | Top _, _ | _, Top _ -> 
     (match min_and_max v1 with 
      Some mn1, Some mx1 when Int.ge mn1 Int.zero -> 
      (match min_and_max v2 with 
       Some mn2, Some mx2 when Int.ge mn2 Int.zero -> 
       let new_max = next_pred_power_of_two (Int.logor mx1 mx2) in 
       let new_min = Int.max mn1 mn2 in (* Or can only add bits *) 
       inject_range (Some new_min) (Some new_max) 
      | _ -> top) 
     | _ -> top) 

let bitwise_xor v1 v2 = 
    if is_bottom v1 || is_bottom v2 
    then bottom 
    else 
    match v1, v2 with 
    | Float _, _ | _, Float _ -> top 
    | Set s1, Set s2 -> apply2_v Int.logxor s1 s2 
    | Top _, _ | _, Top _ -> 
     (match min_and_max v1 with 
     | Some mn1, Some mx1 when Int.ge mn1 Int.zero -> 
      (match min_and_max v2 with 
      | Some mn2, Some mx2 when Int.ge mn2 Int.zero -> 
       let new_max = next_pred_power_of_two (Int.logor mx1 mx2) in 
       let new_min = Int.zero in 
       inject_range (Some new_min) (Some new_max) 
      | _ -> top) 
     | _ -> top)