From ee7b77cfb19740cae75cd15d0214f9f5410a8f1a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 12 Nov 2020 16:38:55 -0800 Subject: [PATCH] [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 | 5 ++--- sledge/src/fol/funsym.ml | 6 +++++- sledge/src/fol/trm.ml | 8 ++++---- sledge/src/fol/var0.ml | 10 ++++------ sledge/src/fol/var_intf.ml | 2 +- sledge/src/llair_to_Fol.ml | 23 +++++------------------ sledge/src/llair_to_Fol.mli | 4 +--- 7 files changed, 22 insertions(+), 36 deletions(-) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 57de85232..93bcdbc41 100644 --- a/sledge/src/domain_sh.ml +++ b/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 diff --git a/sledge/src/fol/funsym.ml b/sledge/src/fol/funsym.ml index 2d4401b7f..059c135db 100644 --- a/sledge/src/fol/funsym.ml +++ b/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 diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index d00459e33..d292fe294 100644 --- a/sledge/src/fol/trm.ml +++ b/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 = diff --git a/sledge/src/fol/var0.ml b/sledge/src/fol/var0.ml index 1ef6193fb..714c640c6 100644 --- a/sledge/src/fol/var0.ml +++ b/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 *) diff --git a/sledge/src/fol/var_intf.ml b/sledge/src/fol/var_intf.ml index 4e6d8d16c..92d2d0801 100644 --- a/sledge/src/fol/var_intf.ml +++ b/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 diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml index cb80fcf8a..83ed46363 100644 --- a/sledge/src/llair_to_Fol.ml +++ b/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 diff --git a/sledge/src/llair_to_Fol.mli b/sledge/src/llair_to_Fol.mli index ac1c3de82..18bfac78a 100644 --- a/sledge/src/llair_to_Fol.mli +++ b/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