整數區間的邏輯計算

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)