Merge branch 'elias'

domains/congruence.ml

@@ -0,0 +1,146 @@
+open Naked
+open Abstract_syntax_tree
+
+module Congruence : NAKED_VALUE_DOMAIN = struct
+  type t = { multiple : Z.t; offset : Z.t }
+
+  let all_numbers = { multiple = Z.one; offset = Z.zero }
+  let const a = { multiple = Z.zero; offset = a }
+  let rand a b = if Z.equal a b then const a else all_numbers
+  let minus z = { multiple = z.multiple; offset = Z.neg z.offset }
+  let is_only_zero z = Z.equal z.multiple Z.zero && Z.equal z.offset Z.zero
+  let has_zero z = Z.divisible z.offset z.multiple
+
+  let subset z1 z2 =
+    Z.equal z2.multiple Z.zero && Z.equal z1.multiple Z.zero
+    && Z.equal z1.offset z2.offset
+    || (not (Z.equal z2.multiple Z.zero))
+       && (Z.equal z1.multiple Z.zero || Z.divisible z2.multiple z1.multiple)
+       && Z.equal (Z.rem z1.offset z2.multiple) (Z.rem z2.offset z2.multiple)
+
+  let join z1 z2 =
+    {
+      multiple =
+        Z.gcd
+          (Z.gcd z1.multiple z2.multiple)
+          (Z.abs (Z.sub z1.offset z2.offset));
+      offset = z1.offset;
+    }
+
+  let meet z1 z2 =
+    if Z.equal z1.multiple Z.zero then if subset z1 z2 then z1 else raise Absurd
+    else if Z.equal z2.multiple Z.zero then
+      if subset z2 z1 then z2 else raise Absurd
+    else
+      let lcm = Z.lcm z1.multiple z2.multiple in
+      let gcd = Z.gcd z1.multiple z2.multiple in
+      if Z.equal (Z.rem z1.offset gcd) (Z.rem z2.offset gcd) then
+        { multiple = lcm; offset = Z.rem z1.offset gcd }
+      else raise Absurd
+
+  let multiples_of z =
+    if is_only_zero z then z
+    else if
+      (not (Z.equal z.multiple Z.zero))
+      && Z.equal (Z.rem z.offset z.multiple) Z.zero
+    then z
+    else all_numbers
+
+  let divisors_of z = z
+  let remainders z = z
+  let convex_sym z = z
+
+  let binary z1 z2 = function
+    | AST_PLUS ->
+        {
+          multiple = Z.gcd z1.multiple z2.multiple;
+          offset = Z.add z1.offset z2.offset;
+        }
+    | AST_MINUS ->
+        {
+          multiple = Z.gcd z1.multiple z2.multiple;
+          offset = Z.sub z1.offset z2.offset;
+        }
+    | AST_MULTIPLY ->
+        {
+          multiple =
+            Z.gcd
+              (Z.gcd
+                 (Z.mul z1.multiple z2.multiple)
+                 (Z.mul z1.multiple z2.offset))
+              (Z.mul z1.offset z2.multiple);
+          offset = Z.mul z1.offset z2.offset;
+        }
+    | AST_DIVIDE ->
+        if is_only_zero z2 then raise Absurd
+        else if
+          Z.equal z2.multiple Z.zero
+          && Z.divisible z1.offset z2.offset
+          && Z.divisible z1.multiple z2.offset
+        then
+          {
+            multiple = Z.div z1.multiple (Z.abs z2.offset);
+            offset = Z.div z1.offset z2.offset;
+          }
+        else all_numbers
+    | AST_MODULO -> all_numbers
+
+  let compatible z = function AST_EQUAL -> z | _ -> raise NeedTop
+
+  let rec compare z1 z2 = function
+    | AST_EQUAL ->
+        let r = meet z1 z2 in
+        (r, r)
+    | AST_NOT_EQUAL ->
+        if
+          Z.equal z1.multiple Z.zero && Z.equal z2.multiple Z.zero
+          && Z.equal z1.offset z2.offset
+        then raise Absurd
+        else (z1, z2)
+    | AST_LESS ->
+        if
+          Z.equal z1.multiple Z.zero && Z.equal z2.multiple Z.zero
+          && Z.geq z1.offset z2.offset
+        then raise Absurd
+        else (z1, z2)
+    | AST_LESS_EQUAL ->
+        if
+          Z.equal z1.multiple Z.zero && Z.equal z2.multiple Z.zero
+          && Z.gt z1.offset z2.offset
+        then raise Absurd
+        else (z1, z2)
+    | AST_GREATER ->
+        let r1, r2 = compare z2 z1 AST_LESS in
+        (r2, r1)
+    | AST_GREATER_EQUAL ->
+        let r1, r2 = compare z2 z1 AST_LESS_EQUAL in
+        (r2, r1)
+
+  let bwd_binary z1 z2 op r =
+    match op with
+    | AST_PLUS ->
+        (meet z1 (binary r z2 AST_MINUS), meet z2 (binary r z1 AST_MINUS))
+    | AST_MINUS ->
+        (meet z1 (binary r z2 AST_PLUS), meet z2 (binary z1 r AST_MINUS))
+    | AST_MULTIPLY ->
+        if is_only_zero z1 || is_only_zero z2 then
+          if has_zero r then (z1, z2) else raise Absurd
+        else
+          let z2' = meet z2 (binary r z1 AST_DIVIDE) in
+          let z1' = meet z1 (binary r z2 AST_DIVIDE) in
+          if has_zero r then
+            ( (if has_zero z1' then join z1' (const Z.zero) else z1'),
+              if has_zero z2' then join z2' (const Z.zero) else z2' )
+          else (z1', z2')
+    | AST_DIVIDE ->
+        (meet z1 (binary r z2 AST_MULTIPLY), meet z2 (binary z1 r AST_DIVIDE))
+    | AST_MODULO -> (z1, z2)
+
+  let widen = join
+  let narrow = meet
+
+  let print fmt z =
+    Z.pp_print fmt z.multiple;
+    Format.pp_print_string fmt "Z + ";
+    Z.pp_print fmt z.offset
+end