(* avalues.ml *)
open Values
(* abstraction of sets of machine integers by initialization *)
(* and  simple sign *)
(* complete lattice *)
type t = BOT | NEG | ZERO | POS | INI | ERR | TOP
(* \gamma(BOT)  = {_O_(a)}                                   *)
(* \gamma(NEG)  = [min_int,-1] U {_O_(a)}                    *)
(* \gamma(POS)  = [1,max_int] U {_O_(a)}                     *)
(* \gamma(ZERO) = {0, _O_(a)}                                *)
(* \gamma(INI)  = [min_int,max_int] U {_O_(a)}               *)
(* \gamma(ERR)  = {_O_(i),_O_(a)}                            *)
(* \gamma(TOP)  = [min_int,max_int] U {_O_(a),_O_(i)}        *)
(* infimum *)
let bot () = BOT 
(* bottom is emptyset? *)
let isbotempty () = false (* \gamma(BOT) = {_O_(a)} <> \emptyset *)
(* uninitialization *)
let initerr () = ERR
(* supremum *)
let top () = TOP
(* least upper bound *)
let nat_of_lat u =
		match u with
		| BOT  -> 0
		| NEG  -> 1
		| ZERO -> 2
		| POS  -> 3
		| INI  -> 4
		| ERR  -> 5
		| TOP  -> 6
let select t u v = t.(nat_of_lat u).(nat_of_lat v)
let join_table =
(*          BOT    NEG   ZERO   POS   INI   ERR   TOP  *)
(*BOT*)[|[| BOT ;  NEG ; ZERO ; POS ; INI ; ERR ; TOP |];
(*NEG*)  [| NEG ;  NEG ; INI  ; INI ; INI ; TOP ; TOP |];
(*ZERO*) [| ZERO ; INI ; ZERO ; INI ; INI ; TOP ; TOP |];
(*POS*)  [| POS ;  INI ; INI  ; POS ; INI ; TOP ; TOP |];
(*INI*)  [| INI ;  INI ; INI  ; INI ; INI ; TOP ; TOP |];
(*ERR*)  [| ERR ;  TOP ; TOP  ; TOP ; TOP ; ERR ; TOP |];
(*TOP*)  [| TOP ;  TOP ; TOP  ; TOP ; TOP ; TOP ; TOP |]|]
let join u v = select join_table u v
(* greatest lower bound *)
let meet_table =
(*          BOT   NEG   ZERO   POS   INI   ERR   TOP   *)
(*BOT*)[|[| BOT ; BOT ; BOT  ; BOT ; BOT ;  BOT ; BOT  |];
(*NEG*)  [| BOT ; NEG ; BOT  ; BOT ; NEG ;  BOT ; NEG  |];
(*ZERO*) [| BOT ; BOT ; ZERO ; BOT ; ZERO ; BOT ; ZERO |];
(*POS*)  [| BOT ; BOT ; BOT  ; POS ; POS ;  BOT ; POS  |];
(*INI*)  [| BOT ; NEG ; ZERO ; POS ; INI ;  BOT ; INI  |];
(*ERR*)  [| BOT ; BOT ; BOT  ; BOT ; BOT ;  ERR ; ERR  |];
(*TOP*)  [| BOT ; NEG ; ZERO ; POS ; INI ;  ERR ; TOP  |]|]
let meet u v = select meet_table u v 
(* approximation ordering *)
let leq_table =
(*          BOT     NEG     ZERO    POS     INI     ERR     TOP  *)
(*BOT*)[|[| true ;  true ;  true ;  true ;  true ;  true ;  true |];
(*NEG*)  [| false ; true ;  false ; false ; true ;  false ; true |];
(*ZERO*) [| false ; false ; true ;  false ; true ;  false ; true |];
(*POS*)  [| false ; false ; false ; true ;  true ;  false ; true |];
(*INI*)  [| false ; false ; false ; false ; true ;  false ; true |];
(*ERR*)  [| false ; false ; false ; false ; false ; true ;  true |];
(*TOP*)  [| false ; false ; false ; false ; false ; false ; true |]|]
let leq u v = select leq_table u v 
(* equality *)
let eq u v = (u = v)
(* included in errors? *)
let in_errors v = (leq v ERR)
(* printing *)
let print u = 
  match u with
  | BOT  -> (print_string "BOT")
  | NEG  -> (print_string "NEG")
  | ZERO -> (print_string "ZERO")
  | POS  -> (print_string "POS")
  | INI  -> (print_string "INI")
  | ERR  -> (print_string "ERR")
  | TOP  -> (print_string "TOP")
(* forward abstract semantics of arithmetic expressions *)
let f_NAT s = 
   match (machine_int_of_string s) with
	| (ERROR_NAT INITIALIZATION) -> ERR
	| (ERROR_NAT ARITHMETIC) -> BOT
	| (NAT i) -> if i = 0 then ZERO else if i > 0 then POS else NEG
let f_RANDOM () = INI
let f_UMINUS a = 
   match a with
   | BOT  -> BOT
   | NEG  -> POS
   | ZERO -> ZERO
   | POS  -> NEG
   | INI  -> INI
   | ERR  -> ERR
   | TOP  -> TOP
let f_UPLUS a = a
let f_PLUS_table =
(*     +   BOT   NEG   ZERO   POS   INI    ERR   TOP  *)
(*BOT*)[|[| BOT ; BOT ; BOT  ; BOT ; BOT ; BOT ; BOT |];
(*NEG*)  [| BOT ; NEG ; NEG  ; INI ; INI ; ERR ; TOP |];
(*ZERO*) [| BOT ; NEG ; ZERO ; POS ; INI ; ERR ; TOP |];
(*POS*)  [| BOT ; INI ; POS  ; POS ; INI ; ERR ; TOP |];
(*INI*)  [| BOT ; INI ; INI  ; INI ; INI ; ERR ; TOP |];
(*ERR*)  [| ERR ; ERR ; ERR  ; ERR ; ERR ; ERR ; ERR |];
(*TOP*)  [| ERR ; TOP ; TOP  ; TOP ; TOP ; ERR ; TOP |]|]
let f_PLUS  u v = select f_PLUS_table u v
let f_MINUS_table =
(*     -    BOT   NEG   ZERO   POS   INI    ERR   TOP  *)
(*BOT*)[|[| BOT ; BOT ; BOT  ; BOT ; BOT ; BOT ; BOT |];
(*NEG*)  [| BOT ; INI ; NEG  ; NEG ; INI ; ERR ; TOP |];
(*ZERO*) [| BOT ; POS ; ZERO ; NEG ; INI ; ERR ; TOP |];
(*POS*)  [| BOT ; POS ; POS  ; INI ; INI ; ERR ; TOP |];
(*INI*)  [| BOT ; INI ; INI  ; INI ; INI ; ERR ; TOP |];
(*ERR*)  [| ERR ; ERR ; ERR  ; ERR ; ERR ; ERR ; ERR |];
(*TOP*)  [| ERR ; TOP ; TOP  ; TOP ; TOP ; ERR ; TOP |]|]
let f_MINUS u v = select f_MINUS_table u v
let f_TIMES_table =
(*     *    BOT   NEG    ZERO   POS    INI    ERR   TOP  *)
(*BOT*)[|[| BOT ; BOT ;  BOT  ; BOT ;  BOT ;  BOT ; BOT |];
(*NEG*)  [| BOT ; POS ;  ZERO ; NEG ;  INI ;  ERR ; TOP |];
(*ZERO*) [| BOT ; ZERO ; ZERO ; ZERO ; ZERO ; ERR ; TOP |];
(*POS*)  [| BOT ; NEG ;  ZERO ; POS ;  INI ;  ERR ; TOP |];
(*INI*)  [| BOT ; INI ;  ZERO ; INI ;  INI ;  ERR ; TOP |];
(*ERR*)  [| ERR ; ERR ;  ERR  ; ERR ;  ERR ;  ERR ; ERR |];
(*TOP*)  [| ERR ; TOP ;  TOP  ; TOP ;  TOP ;  ERR ; TOP |]|]
let f_TIMES u v = select f_TIMES_table u v
let f_DIV_table =
(*     /    BOT   NEG   ZERO  POS   INI    ERR   TOP  *)
(*BOT*)[|[| BOT ; BOT ; BOT ; BOT ;  BOT ; BOT ; BOT |];
(*NEG*)  [| BOT ; BOT ; BOT ; BOT ;  BOT ; BOT ; BOT |];
(*ZERO*) [| BOT ; BOT ; BOT ; ZERO ; POS ; ERR ; TOP |];
(*POS*)  [| BOT ; BOT ; BOT ; INI ;  INI ; ERR ; TOP |];
(*INI*)  [| BOT ; BOT ; BOT ; INI ;  INI ; ERR ; TOP |];
(*ERR*)  [| ERR ; ERR ; ERR ; ERR ;  ERR ; ERR ; ERR |];
(*TOP*)  [| ERR ; ERR ; ERR ; TOP ;  TOP ; ERR ; TOP |]|]
let f_DIV   u v = select f_DIV_table u v
let f_MOD_table =
(*    mod   BOT   NEG   ZERO  POS    INI    ERR   TOP  *)
(*BOT*)[|[| BOT ; BOT ; BOT ; BOT  ; BOT  ; BOT ; BOT |];
(*NEG*)  [| BOT ; BOT ; BOT ; BOT  ; BOT  ; BOT ; BOT |];
(*ZERO*) [| BOT ; BOT ; BOT ; ZERO ; ZERO ; ERR ; TOP |];
(*POS*)  [| BOT ; BOT ; BOT ; INI  ; INI  ; ERR ; TOP |];
(*INI*)  [| BOT ; BOT ; BOT ; INI  ; INI  ; ERR ; TOP |];
(*ERR*)  [| ERR ; ERR ; ERR ; ERR  ; ERR  ; ERR ; ERR |];
(*TOP*)  [| ERR ; ERR ; ERR ; TOP  ; TOP  ; ERR ; TOP |]|]
let f_MOD   u v = select f_MOD_table u v
(* forward abstract semantics of boolean expressions *)
let f_EQ_table =
(*    mod   BOT     NEG     ZERO    POS     INI     ERR     TOP   *)
(*BOT*)[|[| false ; false ; false ; false ; false ; false ; false |];
(*NEG*)  [| false ; true  ; false ; false ; true  ; false ; true  |];
(*ZERO*) [| false ; false ; true  ; false ; true  ; false ; true  |];
(*POS*)  [| false ; false ; false ; true  ; true  ; false ; true  |];
(*INI*)  [| false ; true  ; true  ; true  ; true  ; false ; true  |];
(*ERR*)  [| false ; false ; false ; false ; false ; false ; false |];
(*TOP*)  [| false ; true  ; true  ; true  ; true  ; false ; true  |]|]
(* Are there integer values in gamma(u) equal to values in gamma(v)? *)
let f_EQ u v = select f_EQ_table u v
let f_LT_table =
(*    mod   BOT     NEG     ZERO    POS     INI     ERR     TOP   *)
(*BOT*)[|[| false ; false ; false ; false ; false ; false ; false |];
(*NEG*)  [| false ; true  ; true  ; true  ; true  ; false ; true  |];
(*ZERO*) [| false ; false ; true  ; true  ; true  ; false ; true  |];
(*POS*)  [| false ; false ; false ; true  ; true  ; false ; true  |];
(*INI*)  [| false ; true  ; true  ; true  ; true  ; false ; true  |];
(*ERR*)  [| false ; false ; false ; false ; false ; false ; false |];
(*TOP*)  [| false ; true  ; true  ; true  ; true  ; false ; true  |]|]
(* Are there integer values in gamma(u) less than or equal to (<=) *)
(* integer values in gamma(v)?                                     *)
let f_LT u v = select f_LT_table u v