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 !

CodePudding user response：

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]
  (Pos, Neg) -> [Pos, Zero, Neg]
  (Pos, _) -> [Pos]
  (Neg, Pos) -> [Pos, Zero, Neg]
  (Neg, _) -> [Neg]

CodePudding user response：

The functional way to approach this is as follows:

let join : ((sign list) list) -> (sign list) = 
   (* flatten and remove duplicates *)

let add : sign -> sign -> sign list = 
   (* as expected *)

let add_list (sl : sign list) (s : sign) : sign list =
   join (List.map (add s) sl)
      
let add_abstract : (sl0 : sign list) (sl1 : sign list) : sign list =
   join (List.map (add_list sl0) sl1) 

You might have to be more careful with non-commutative operations like substraction and division.