(* 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
(* backward abstract interpretation of arithmetic expressions *)
exception Error_f_NAT of string
let remove_zeros i =
  let l = (String.length i) in
  if l = 0 then raise (Error_f_NAT "empty integer")
  else if l = 1 then i
  else if (String.get i 0) = '0' then String.sub i 1  (l - 1)
  else i
let b_NAT i p =
  let i' = (remove_zeros i) in
  if i' = "0" then
    match p with
    | BOT  -> false
    | NEG  -> false
    | ZERO -> true
    | POS  -> false
    | INI  -> true
    | ERR  -> false
    | TOP  -> true
  else
    match p with
    | BOT  -> false
    | NEG  -> false
    | ZERO -> false
    | POS  -> true
    | INI  -> true
    | ERR  -> false
    | TOP  -> true
let b_RANDOM p =
  match p with
  | BOT -> false
  | ERR -> false
  | _   -> true
let b_UMINUS q p =
  match p with
  | BOT  -> BOT
  | NEG  -> meet q POS
  | ZERO -> meet q ZERO
  | POS  -> meet q NEG
  | INI  -> meet q INI
  | ERR  -> BOT
  | TOP  -> meet q INI
let b_UPLUS q p =
  match p with
  | BOT -> BOT
  | ERR -> BOT
  | TOP -> meet q INI
  | _   -> meet q p
exception Error_b_PLUS of string
let nat_of_lat' u =
  match u with
  | NEG  -> 0
  | ZERO -> 1
  | POS  -> 2
  | INI  -> 3
  | TOP  -> 4
  | _    -> raise (Error_b_PLUS "impossible selection")
let select' t u v = t.(nat_of_lat' u).(nat_of_lat' v)
let b_PLUS_NEG_table =
(*             NEG         ZERO         POS         INI          TOP      *)
(*NEG*)[|[| (NEG,NEG) ;  (NEG,ZERO) ; (NEG,POS) ; (NEG,INI) ;  (NEG,INI)  |];
(*ZERO*) [| (ZERO,NEG) ; (BOT,BOT) ;  (BOT,BOT) ; (ZERO,NEG) ; (ZERO,NEG) |];
(*POS*)  [| (POS,NEG) ;  (BOT,BOT) ;  (BOT,BOT) ; (POS,NEG) ;  (POS,NEG)  |];
(*INI*)  [| (INI,NEG) ;  (NEG,ZERO) ; (NEG,POS) ; (INI,INI) ;  (INI,INI)  |];
(*TOP*)  [| (INI,NEG) ;  (NEG,ZERO) ; (NEG,POS) ; (INI,INI) ;  (INI,INI)  |]|]
let b_PLUS_ZERO_table =
(*NEG*)[|[| (BOT,BOT) ; (BOT,BOT) ;   (NEG,POS) ; (NEG,POS) ;   (NEG,POS)   |];
(*ZERO*) [| (BOT,BOT) ; (ZERO,ZERO) ; (BOT,BOT) ; (ZERO,ZERO) ; (ZERO,ZERO) |];
(*POS*)  [| (POS,NEG) ; (BOT,BOT) ;   (BOT,BOT) ; (POS,NEG) ;   (POS,NEG)   |];
(*INI*)  [| (POS,NEG) ; (ZERO,ZERO) ; (NEG,POS) ; (INI,INI) ;   (INI,INI)   |];
(*TOP*)  [| (POS,NEG) ; (ZERO,ZERO) ; (NEG,POS) ; (INI,INI) ;   (INI,INI)   |]|]
let b_PLUS_POS_table =
(*NEG*)[|[| (BOT,BOT) ; (BOT,BOT) ;  (NEG,POS) ;  (NEG,POS) ;  (NEG,POS)  |];
(*ZERO*) [| (BOT,BOT) ; (BOT,BOT) ;  (ZERO,POS) ; (ZERO,POS) ; (ZERO,POS) |];
(*POS*)  [| (POS,NEG) ; (POS,ZERO) ; (POS,INI) ;  (POS,INI) ;  (POS,INI)  |];
(*INI*)  [| (POS,NEG) ; (POS,ZERO) ; (INI,POS) ;  (INI,INI) ;  (INI,INI)  |];
(*TOP*)  [| (POS,NEG) ; (POS,ZERO) ; (INI,POS) ;  (INI,INI) ;  (INI,INI)  |]|]
let b_PLUS q1 q2 p = 
  if (q1=BOT)||(q1=ERR)||(q2=BOT)||(q2=ERR)||(p=BOT)||(p=ERR) then
    (BOT,BOT)
  else if (p=INI)||(p=TOP) then
    ((meet q1 INI),(meet q2 INI))
  else if p = NEG then  select' b_PLUS_NEG_table q1 q2
  else if p = ZERO then select' b_PLUS_ZERO_table q1 q2
  else if p = POS then  select' b_PLUS_POS_table q1 q2
  else raise (Error_b_PLUS "impossible case")
let b_MINUS q1 q2 p = 
  let r1,r2 = b_PLUS q1 (f_UMINUS q2) p in
    r1,(f_UMINUS  r2)
exception Error_b_TIMES of string
let b_TIMES_NEG_table =
(*             NEG         ZERO         POS         INI          TOP      *)
(*NEG*)[|[| (BOT,BOT) ; (BOT,BOT) ; (BOT,BOT) ; (NEG,INI) ; (NEG,INI) |];
(*ZERO*) [| (BOT,BOT) ; (BOT,BOT) ; (BOT,BOT) ; (BOT,BOT) ; (BOT,BOT) |];
(*POS*)  [| (POS,NEG) ; (BOT,BOT) ; (BOT,BOT) ; (POS,NEG) ; (POS,NEG) |];
(*INI*)  [| (INI,NEG) ; (BOT,BOT) ; (NEG,POS) ; (INI,INI) ; (INI,INI) |];
(*TOP*)  [| (INI,NEG) ; (BOT,BOT) ; (NEG,POS) ; (INI,INI) ; (INI,INI) |]|]
let b_TIMES_ZERO_table =
(*NEG*)[|[| (BOT,BOT) ;  (NEG,ZERO) ;  (BOT,BOT) ;  (NEG,ZERO) ; (NEG,ZERO) |];
(*ZERO*) [| (ZERO,NEG) ; (ZERO,ZERO) ; (ZERO,POS) ; (ZERO,INI) ; (ZERO,INI) |];
(*POS*)  [| (BOT,BOT) ;  (POS,ZERO) ;  (BOT,BOT) ;  (POS,ZERO) ; (POS,ZERO) |];
(*INI*)  [| (ZERO,NEG) ; (INI,ZERO) ;  (ZERO,POS) ; (INI,INI) ;  (INI,INI)  |];
(*TOP*)  [| (ZERO,NEG) ; (INI,ZERO) ;  (ZERO,POS) ; (INI,INI) ;  (INI,INI)  |]|]
let b_TIMES_POS_table =
(*NEG*)[|[| (BOT,BOT) ; (BOT,BOT) ; (BOT,BOT) ; (NEG,NEG) ; (NEG,NEG) |];
(*ZERO*) [| (BOT,BOT) ; (BOT,BOT) ; (BOT,BOT) ; (BOT,BOT) ; (BOT,BOT) |];
(*POS*)  [| (POS,NEG) ; (BOT,BOT) ; (POS,POS) ; (POS,POS) ; (POS,POS) |];
(*INI*)  [| (POS,NEG) ; (BOT,BOT) ; (POS,POS) ; (INI,INI) ; (INI,INI) |];
(*TOP*)  [| (POS,NEG) ; (BOT,BOT) ; (POS,POS) ; (INI,INI) ; (INI,INI) |]|]
let b_TIMES q1 q2 p = 
  if (q1=BOT)||(q1=ERR)||(q2=BOT)||(q2=ERR)||(p=BOT)||(p=ERR) then
    (BOT,BOT)
  else if (p=INI)||(p=TOP) then
    ((meet q1 INI),(meet q2 INI))
  else if p = NEG then  select' b_TIMES_NEG_table q1 q2
  else if p = ZERO then select' b_TIMES_ZERO_table q1 q2
  else if p = POS then  select' b_TIMES_POS_table q1 q2
  else raise (Error_b_TIMES "impossible case")
let smash x y = if (x=BOT)||(y=BOT) then (BOT,BOT) else (x,y)
let b_DIV q1 q2 p = 
  if (q1=BOT)||(q1=NEG)||(q1=ERR)||
     (q2=BOT)||(q2=NEG)||(q2=ZERO)||(q2=ERR)||
(p=BOT)||(p=NEG)||(p=ERR) then
(BOT,BOT)
  else if p = POS then
     (smash (meet q1 POS) (meet q2 POS))
  else
     (smash (meet q1 INI) (meet q2 POS))
let b_MOD = b_DIV
(* boolean expressions *)
let a_EQ p1 p2 = 
  let p = (meet p1 (meet p2 (f_RANDOM ()))) in
    (p,p)
let a_LT_table =[|
(*     <      BOT       NEG       ZERO       POS        INI        ERR       TOP    *)
(*BOT*) [|(BOT,BOT);(BOT,BOT);(BOT,BOT) ;(BOT,BOT) ;(BOT,BOT) ;(BOT,BOT);(BOT,BOT) |];
(*NEG*) [|(BOT,BOT);(NEG,NEG);(NEG,ZERO);(NEG,POS) ;(NEG,INI) ;(BOT,BOT);(NEG,INI) |];
(*ZERO*)[|(BOT,BOT);(BOT,BOT);(BOT,BOT) ;(ZERO,POS);(ZERO,POS);(BOT,BOT);(ZERO,POS)|];
(*POS*) [|(BOT,BOT);(BOT,BOT);(BOT,BOT) ;(POS,POS) ;(POS,POS) ;(BOT,BOT);(POS,POS) |];
(*INI*) [|(BOT,BOT);(NEG,NEG);(NEG,ZERO);(INI,POS) ;(INI,INI) ;(BOT,BOT);(INI,INI) |];
(*ERR*) [|(BOT,BOT);(BOT,BOT);(BOT,BOT) ;(BOT,BOT) ;(BOT,BOT) ;(BOT,BOT);(BOT,BOT) |];
(*TOP*) [|(BOT,BOT);(NEG,NEG);(NEG,ZERO);(INI,POS) ;(INI,INI) ;(BOT,BOT);(INI,INI) |]
|]
let a_LT   u v = select a_LT_table u v