Merge branch 'feature/eva/backward-logical-operators' into 'master'

[Eva] Backward operators for the logical conjunction LAnd and disjunction LOr

See merge request frama-c/frama-c!3034

src/plugins/value/values/cvalue_backward.ml

@@ -228,6 +228,34 @@ let backward_bor ~v1 ~v2 ~res =
   in
   backward_bor_aux v1 v2, backward_bor_aux v2 v1
 
+let backward_land ~v1 ~v2 ~res =
+  if V.is_zero res then
+    match V.contains_zero v1, V.contains_zero v2 with
+    | true, true -> None
+    | false, false -> Some (V.bottom, V.bottom)
+    | true, false -> Some (V.singleton_zero, v2)
+    | false, true -> Some (v1, V.singleton_zero)
+  else if V.contains_zero res then
+    None
+  else
+    let v1' = V.(diff v1 singleton_zero)
+    and v2' = V.(diff v2 singleton_zero) in
+    if V.equal v1 v1' && V.equal v2 v2' then None else Some (v1', v2')
+
+let backward_lor ~v1 ~v2 ~res =
+  if V.is_zero res then
+    if V.is_zero v1 && V.is_zero v2
+    then None
+    else Some (V.singleton_zero, V.singleton_zero)
+  else if V.contains_zero res then
+    None
+  else
+    match V.is_zero v1, V.is_zero v2 with
+    | false, false -> None
+    | true, true -> Some (V.bottom, V.bottom)
+    | true, false -> Some (v1, V.diff v2 V.singleton_zero)
+    | false, true -> Some (V.diff v1 V.singleton_zero, v2)
+
 let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
   let typ = Cil.unrollType typ_res in
   match binop, typ with
@@ -303,6 +331,9 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
 
   | BOr, TInt _ -> Some (backward_bor ~v1 ~v2 ~res:res_value)
 
+  | LAnd, TInt _ -> backward_land ~v1 ~v2 ~res:res_value
+  | LOr, TInt _ -> backward_lor ~v1 ~v2 ~res:res_value
+
   | _, _ -> None
 
 let backward_unop ~typ_arg op ~arg:_ ~res =

tests/value/backward_arith.i

 /* run.config*
+   STDOPT: +"-keep-logical-operators"
 */
 
 /* Test the soundness of arithmetic backward propagators.  */
@@ -26,8 +27,52 @@ void unsigned_neg () {
     Frama_C_show_each_smaller_than_minus_ten_but_zero(x); /* <= 4294967286 but 0 */
 }
 
+void logical_operators () {
+  unsigned int x = nondet;
+  unsigned int y = nondet;
+  unsigned int a = x % 10;
+  unsigned int b = x % 10;
+
+  // Logical conjunction LAnd.
+  if (x < 11 && y < 21)
+    Frama_C_show_each("0..10", x, "0..20", y);
+  else
+    Frama_C_show_each("top", x, "top", y);
+  if (a < 10 && y < 10)
+    Frama_C_show_each("0..9", a, "0..9", y);
+  else
+    Frama_C_show_each("0..9", a, "10..max", y);
+  if (a > 10 && y < 10)
+    Frama_C_show_each("bottom", a, y);
+  else
+    Frama_C_show_each("0..9", a, "top", y);
+  if (a > 10 && b > 10)
+    Frama_C_show_each("bottom", a, b);
+  else
+    Frama_C_show_each("0..9", a, "0..9", b);
+
+  // Logical disjunction LOr.
+  if (x > 10 || y > 20)
+    Frama_C_show_each("top", x, "top", y);
+  else
+    Frama_C_show_each("0..10", x, "0..20", y);
+  if (a > 10 || y > 10)
+    Frama_C_show_each("0..9", a, "11..max", y);
+  else
+    Frama_C_show_each("0..9", a, "0..10", y);
+  if (a < 10 || y > 10)
+    Frama_C_show_each("0..9", a, "top", y);
+  else
+    Frama_C_show_each("bottom", a, y);
+  if (a > 10 || b > 10)
+    Frama_C_show_each("bottom", a, b);
+  else
+    Frama_C_show_each("0..9", a, "0..9", b);
+}
+
 
 int main () {
   unsigned_neg ();
+  logical_operators ();
   return 0;
 }

tests/value/oracle/backward_arith.res.oracle

@@ -5,42 +5,83 @@
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
 [eva] computing for function unsigned_neg <- main.
-  Called from tests/value/backward_arith.i:31.
-[eva] tests/value/backward_arith.i:12: Frama_C_show_each_ten: {10}
-[eva] tests/value/backward_arith.i:14: 
+  Called from tests/value/backward_arith.i:75.
+[eva] tests/value/backward_arith.i:13: Frama_C_show_each_ten: {10}
+[eva] tests/value/backward_arith.i:15: 
   Frama_C_show_each_not_ten: [0..4294967295]
-[eva] tests/value/backward_arith.i:16: 
+[eva] tests/value/backward_arith.i:17: 
   Frama_C_show_each_greater_than_ten_or_zero: [0..4294967295]
-[eva] tests/value/backward_arith.i:18: 
+[eva] tests/value/backward_arith.i:19: 
   Frama_C_show_each_smaller_than_ten_but_zero: [1..10]
-[eva] tests/value/backward_arith.i:20: Frama_C_show_each_minus_ten: {4294967286}
-[eva] tests/value/backward_arith.i:22: 
+[eva] tests/value/backward_arith.i:21: Frama_C_show_each_minus_ten: {4294967286}
+[eva] tests/value/backward_arith.i:23: 
   Frama_C_show_each_not_minus_ten: [0..4294967295]
-[eva] tests/value/backward_arith.i:24: 
+[eva] tests/value/backward_arith.i:25: 
   Frama_C_show_each_greater_than_minus_ten_or_zero: [0..4294967295]
-[eva] tests/value/backward_arith.i:26: 
+[eva] tests/value/backward_arith.i:27: 
   Frama_C_show_each_smaller_than_minus_ten_but_zero: [1..4294967286]
 [eva] Recording results for unsigned_neg
 [eva] Done for function unsigned_neg
+[eva] computing for function logical_operators <- main.
+  Called from tests/value/backward_arith.i:76.
+[eva] tests/value/backward_arith.i:38: 
+  Frama_C_show_each: {{ "0..10" }}, [0..10], {{ "0..20" }}, [0..20]
+[eva] tests/value/backward_arith.i:40: 
+  Frama_C_show_each: {{ "top" }}, [0..4294967295], {{ "top" }}, [0..4294967295]
+[eva] tests/value/backward_arith.i:42: 
+  Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "0..9" }}, [0..9]
+[eva] tests/value/backward_arith.i:44: 
+  Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "10..max" }}, [10..4294967295]
+[eva] tests/value/backward_arith.i:48: 
+  Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "top" }}, [0..4294967295]
+[eva] tests/value/backward_arith.i:52: 
+  Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "0..9" }}, [0..9]
+[eva] tests/value/backward_arith.i:56: 
+  Frama_C_show_each: {{ "top" }}, [0..4294967295], {{ "top" }}, [0..4294967295]
+[eva] tests/value/backward_arith.i:58: 
+  Frama_C_show_each: {{ "0..10" }}, [0..10], {{ "0..20" }}, [0..20]
+[eva] tests/value/backward_arith.i:60: 
+  Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "11..max" }}, [11..4294967295]
+[eva] tests/value/backward_arith.i:62: 
+  Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "0..10" }}, [0..10]
+[eva] tests/value/backward_arith.i:64: 
+  Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "top" }}, [0..4294967295]
+[eva] tests/value/backward_arith.i:70: 
+  Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "0..9" }}, [0..9]
+[eva] Recording results for logical_operators
+[eva] Done for function logical_operators
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function logical_operators:
+  x ∈ [--..--]
+  y ∈ [--..--]
+  a ∈ [0..9]
+  b ∈ [0..9]
 [eva:final-states] Values at end of function unsigned_neg:
   x ∈ [--..--]
   minus_ten ∈ {4294967286}
 [eva:final-states] Values at end of function main:
   __retres ∈ {0}
+[from] Computing for function logical_operators
+[from] Done for function logical_operators
 [from] Computing for function unsigned_neg
 [from] Done for function unsigned_neg
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function logical_operators:
+  NO EFFECTS
 [from] Function unsigned_neg:
   NO EFFECTS
 [from] Function main:
   \result FROM \nothing
 [from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function logical_operators:
+    x; y; a; b
+[inout] Inputs for function logical_operators:
+    nondet
 [inout] Out (internal) for function unsigned_neg:
     x; minus_ten
 [inout] Inputs for function unsigned_neg: