Pseudocode algorithm for variables' signs static analysis - Check the sign of each operation

Question

I want to do static sign analysis on variables (ints only).

Example : I have the possible signs of two variables and the operation

A Positive + A positive = A positive [Pos] + [Pos] -> [Pos]

A Positive or Zero + A positive = A Positive [Pos; Zero] + [Pos] -> [Pos]

A Positive or Zero or Negative * Zero = Zero [Pos; Zero; Neg] * [Zero] -> [Zero]

Etc...

My variables' signs are coded as Lists / Arrays.

A positive or zero variable will be coded as [Pos; Zero] A negative variables will be coded as [Neg] A positive, negative or zero variable will be coded as [Pos; Neg; Zero] Order doesn't matter [Pos; Zero] is the same as [Zero; Pos]

I need to do this in OCAML, but you can help in any language / pseudocode.

Here is my idea :

let sign_operation (op:op) (l_expr: sign list) (r_expr: sign list): sign list = 
  match op with 
  | Add -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Pos]
      | [Pos], [Zero] -> [Pos]
      | [Zero], [Pos] -> [Pos]
      | [Pos], [Neg] -> [Neg;Zero;Pos]
      | [Neg], [Pos] -> [Neg;Zero;Pos]
      | [Neg], [Zero] -> [Neg]
      | [Zero], [Neg] -> [Neg]
      | [Neg], [Neg] -> [Neg]
      | [Zero], [Zero] -> [Zero]
      | _ -> failwith "no")

  | Sub -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Neg;Zero;Pos]
      | [Pos], [Zero] -> [Pos]
      | [Zero], [Pos] -> [Neg]
      | [Pos], [Neg] -> [Pos]
      | [Neg], [Pos] -> [Neg]
      | [Neg], [Zero] -> [Neg]
      | [Zero], [Neg] -> [Pos]
      | [Neg], [Neg] -> [Neg;Zero;Pos]
      | [Zero], [Zero] -> [Zero]
      | _ -> failwith "no")

  | Mul -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Pos]
      | [Pos], [Zero] -> [Zero]
      | [Zero], [Pos] -> [Zero]
      | [Pos], [Neg] -> [Neg]
      | [Neg], [Pos] -> [Neg]
      | [Neg], [Zero] -> [Zero]
      | [Zero], [Neg] -> [Zero]
      | [Neg], [Neg] -> [Pos]
      | [Zero], [Zero] -> [Zero]
      | [Neg;Zero;Pos], [Zero] -> [Zero]
      | [Zero], [Neg;Zero;Pos] -> [Zero]
      | _ , [Zero] -> [Zero]
      | [Zero] , _ -> [Zero]
      | _ -> failwith "no")

  | Div -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Pos]
      | [Pos], [Zero] -> [Error]
      | [Zero], [Pos] -> [Zero]
      | [Pos], [Neg] -> [Neg]
      | [Neg], [Pos] -> [Neg]
      | [Neg], [Zero] -> [Error]
      | [Zero], [Neg] -> [Zero]
      | [Neg], [Neg] -> [Pos]
      | [Zero], [Zero] -> [Error]
      | [Neg;Zero;Pos], [Zero] -> [Error]
      | [Zero], [Neg;Zero;Pos] -> [Zero]
      | _ -> [Error])

  | Mod -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Pos]
      | [Pos], [Zero] -> [Error]
      | [Zero], [Pos] -> [Zero]
      | [Pos], [Neg] -> [Error]
      | [Neg], [Pos] -> [Error]
      | [Neg], [Zero] -> [Error]
      | [Zero], [Neg] -> [Error]
      | [Neg], [Neg] -> [Error]
      | [Zero], [Zero] -> [Error]
      | _ -> [Error])

This doesn't work for any variable with two or more possible signs.

If I have a variable [Pos; Zero; Neg] Minus [Pos; Zero], this won't be matched in my patterns. Trying every possible permutation in every possible order will be too long.

Can you suggest a better way to do this ?

Sorry if I couldn't get myself understood well, feel free to ask any question and thank you !

Answer 1

In your question, you write

A Positive or Zero + A positive = A Positive [Pos; Zero] + [Pos] -> [Pos]

How do you know this? Did you attend a school that taught you specifically what you get if you add a positive-or-zero number to something? Of course not. You broke it down into simpler cases, reasoning as follows:

1. The first number might be positive. In that case, I know that Pos+Pos = Pos
2. The first number might be zero. In that case, I know that Zero+Pos = Pos.
3. Therefore, across all values that the first number might hold, the result is either Pos or Pos.
4. Of course, we can simplify that to always being Pos.

Write a program that reasons in the same way. Instead of looking at a pair of lists of signs all at once, write a function for each operation that handles just a single sign for each operand, yielding a list of possible results. Call that function on each possible pair of signs represented by the input lists, then combine the results.

For example.

signOp Add x y = case (x, y) of
  (Zero, r) -> [r]
  (l, Zero) -> [l]
  _ | x == y -> [x]
    | otherwise -> [Pos, Zero, Neg]