[sledge] Distinguish globals and functions from variables

Summary:
Global variables and function names in LLAIR are constant and so do
not need to be handled like normal assignable or shadowable
variables. This diff does this by changing the translation from LLAIR
to FOL to map globals and functions to uninterpreted constants instead
of variables.

Reviewed By: jvillard

Differential Revision: D24886571

fbshipit-source-id: efb8c9f49

sledge/src/domain_sh.ml

@@ -23,7 +23,7 @@ let init globals =
   IArray.fold globals Sh.emp ~f:(fun global q ->
       match (global : Llair.GlobalDefn.t) with
       | {name; init= Some (seq, siz)} ->
-          let loc = Term.var (X.global name) in
+          let loc = X.global name in
           let len = Term.integer (Z.of_int siz) in
           let seq = X.term seq in
           Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq})
@@ -114,8 +114,7 @@ let localize_entry globals actuals formals freturn locals shadow pre entry =
   let wrt =
     Term.Set.of_iter
       (Iter.append
-         (Iter.map ~f:(Term.var << X.global)
-            (Llair.Global.Set.to_iter globals))
+         (Iter.map ~f:X.global (Llair.Global.Set.to_iter globals))
          (Iter.map ~f:Term.var (List.to_iter formals)))
   in
   let function_summary_pre = garbage_collect entry ~wrt in

sledge/src/fol/funsym.ml

@@ -32,7 +32,11 @@ let pp ppf f =
   | BitAshr -> pf "ashr"
   | Signed n -> pf "(s%i)" n
   | Unsigned n -> pf "(u%i)" n
-  | Uninterp sym -> pf "%s" sym
+  | Uninterp sym ->
+      if String.is_empty sym then pf ""
+      else if Char.equal sym.[0] '@' || Char.equal sym.[0] '%' then
+        Trace.pp_styled `Bold "%s" ppf sym
+      else pf "%s" sym
 
 let uninterp s = Uninterp s
 

sledge/src/fol/trm.ml

@@ -121,16 +121,16 @@ end = struct
     if x == y then 0
     else
       match (x, y) with
-      | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
-          Int.compare i j
+      | Var {id= 0; name= s}, Var {id= 0; name= t} -> String.compare s t
+      | Var {id= i; name= _}, Var {id= j; name= _} -> Int.compare i j
       | _ -> compare x y
 
   let equal x y =
     x == y
     ||
     match (x, y) with
-    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
-        Int.equal i j
+    | Var {id= 0; name= s}, Var {id= 0; name= t} -> String.equal s t
+    | Var {id= i; name= _}, Var {id= j; name= _} -> Int.equal i j
     | _ -> equal x y
 
   let rec ppx strength fs trm =

sledge/src/fol/var0.ml

@@ -16,15 +16,13 @@ module Make (T : REPR) = struct
   let ppx strength ppf v =
     let id = id v in
     let name = name v in
-    match id with
-    | -1 -> Trace.pp_styled `Bold "%@%s" ppf name
-    | 0 -> Trace.pp_styled `Bold "%%%s" ppf name
-    | _ -> (
+    if id = 0 then Trace.pp_styled `Bold "%%%s" ppf name
+    else
       match strength v with
       | None -> Format.fprintf ppf "%%%s_%d" name id
       | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" ppf name id
       | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" ppf name id
-      | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf )
+      | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf
 
   let pp = ppx (fun _ -> None)
 
@@ -52,7 +50,7 @@ module Make (T : REPR) = struct
     let x' = make ~id:(max + 1) ~name in
     (x', Set.add x' wrt)
 
-  let program ~name ~global = make ~id:(if global then -1 else 0) ~name
+  let program ~name = make ~id:0 ~name
   let identified ~name ~id = make ~id ~name
 
   (** Variable renaming substitutions *)

sledge/src/fol/var_intf.ml

@@ -40,7 +40,7 @@ module type VAR = sig
 
   val id : t -> int
   val name : t -> string
-  val program : name:string -> global:bool -> t
+  val program : name:string -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
   val identified : name:string -> id:int -> t

sledge/src/llair_to_Fol.ml

@@ -9,21 +9,9 @@ open Fol
 module T = Term
 module F = Formula
 
-let func f =
-  let name = Llair.Function.name f in
-  Var.program ~name ~global:true
-
-let global g =
-  let name = Llair.Global.name g in
-  Var.program ~name ~global:true
-
-let globals gs =
-  Var.Set.of_iter (Iter.map ~f:global (Llair.Global.Set.to_iter gs))
-
-let reg r =
-  let name = Llair.Reg.name r in
-  Var.program ~name ~global:false
-
+let uconst name = T.apply (Funsym.uninterp ("@" ^ name)) [||]
+let global g = uconst (Llair.Global.name g)
+let reg r = Var.program ~name:(Llair.Reg.name r)
 let regs rs = Var.Set.of_iter (Iter.map ~f:reg (Llair.Reg.Set.to_iter rs))
 let uap0 f = T.apply f [||]
 let uap1 f a = T.apply f [|a|]
@@ -73,9 +61,8 @@ and term : Llair.Exp.t -> T.t =
       F.inject
         (F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
   (* terms *)
-  | Reg {name; typ= _} -> T.var (Var.program ~name ~global:false)
-  | Global {name; typ= _} -> T.var (Var.program ~name ~global:true)
-  | Function {name; typ= _} -> T.var (Var.program ~name ~global:true)
+  | Reg {name; typ= _} -> T.var (Var.program ~name)
+  | Global {name; typ= _} | Function {name; typ= _} -> uconst name
   | Label {parent; name} ->
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))
   | Integer {typ= _; data} -> T.integer data

sledge/src/llair_to_Fol.mli

@@ -7,9 +7,7 @@
 
 open Fol
 
-val func : Llair.Function.t -> Var.t
-val global : Llair.Global.t -> Var.t
-val globals : Llair.Global.Set.t -> Var.Set.t
+val global : Llair.Global.t -> Term.t
 val reg : Llair.Reg.t -> Var.t
 val regs : Llair.Reg.Set.t -> Var.Set.t
 val term : Llair.Exp.t -> Term.t