From 009f3b651cfe0fc90746e22f3f3364acf5ba43a4 Mon Sep 17 00:00:00 2001
From: Radu Grigore <rgrigore@fb.com>
Date: Wed, 2 Dec 2020 01:13:55 -0800
Subject: [PATCH] [topl] Small steps in Pulse

Summary:
A Topl "small step" is a call to a method that is of interest to the
automaton. When such a call of interest is made, the topl component of
PulseAbductiveDomain.t is updated.  This means that intra-procedural
Topl should now work entirely inside Pulse, without instrumenting Sil.

Main TODOs:
 - add error extraction
 - implement inter-procedural (PulseTopl.large_step)

Reviewed By: jvillard

Differential Revision: D25028286

fbshipit-source-id: e31a96d13
---
 infer/src/IR/Binop.ml                   |   3 +
 infer/src/IR/Binop.mli                  |   2 +
 infer/src/istd/IList.ml                 |   8 +
 infer/src/istd/IList.mli                |   3 +
 infer/src/pulse/Pulse.ml                |  14 +-
 infer/src/pulse/PulseAbductiveDomain.ml |   6 +-
 infer/src/pulse/PulseFormula.ml         |   2 +-
 infer/src/pulse/PulseInterproc.ml       |  10 +-
 infer/src/pulse/PulseOperations.ml      |   4 +-
 infer/src/pulse/PulsePathCondition.ml   |   7 +
 infer/src/pulse/PulsePathCondition.mli  |   2 +
 infer/src/pulse/PulseTopl.ml            | 229 ++++++++++++++++++++++--
 infer/src/pulse/PulseTopl.mli           |   2 +-
 infer/src/topl/ToplAst.ml               |   2 +-
 infer/src/topl/ToplAutomaton.ml         |  27 +++
 infer/src/topl/ToplAutomaton.mli        |   8 +
 infer/src/topl/ToplMonitor.ml           |  20 +--
 infer/src/topl/ToplParser.mly           |   4 +-
 infer/src/topl/ToplUtils.ml             |   6 +
 infer/src/topl/ToplUtils.mli            |   2 +
 20 files changed, 309 insertions(+), 52 deletions(-)

diff --git a/infer/src/IR/Binop.ml b/infer/src/IR/Binop.ml
index f55f99c70..1661749c4 100644
--- a/infer/src/IR/Binop.ml
+++ b/infer/src/IR/Binop.ml
@@ -158,3 +158,6 @@ let str pe binop =
         to_string binop )
   | _ ->
       to_string binop
+
+
+let pp f binop = Format.fprintf f "%s" (to_string binop)
diff --git a/infer/src/IR/Binop.mli b/infer/src/IR/Binop.mli
index 6a029bdad..00da711d3 100644
--- a/infer/src/IR/Binop.mli
+++ b/infer/src/IR/Binop.mli
@@ -37,6 +37,8 @@ type t =
 
 val str : Pp.env -> t -> string
 
+val pp : Formatter.t -> t -> unit
+
 val equal : t -> t -> bool
 
 val injective : t -> bool
diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml
index 9fb82d9f4..9f8146e7d 100644
--- a/infer/src/istd/IList.ml
+++ b/infer/src/istd/IList.ml
@@ -212,6 +212,14 @@ let fold2_result ~init ~f l1 l2 =
 
 let eval_until_first_some thunks = List.find_map thunks ~f:(fun f -> f ())
 
+let rec product = function
+  | [] ->
+      [[]]
+  | xs :: xss ->
+      let yss = product xss in
+      List.concat_map ~f:(fun x -> List.map ~f:(fun ys -> x :: ys) yss) xs
+
+
 let move_last_to_first =
   let rec move_last_to_first_helper l rev_acc =
     match l with
diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli
index b70e41d46..0abba83db 100644
--- a/infer/src/istd/IList.mli
+++ b/infer/src/istd/IList.mli
@@ -53,6 +53,9 @@ val force_until_first_some : 'a option lazy_t list -> 'a option
 val eval_until_first_some : (unit -> 'a option) list -> 'a option
 (** given a list of functions taking unit, evaluate and return the first one to return [Some x] *)
 
+val product : 'a list list -> 'a list list
+(** n-ary cartesian product *)
+
 val pp_print_list :
      max:int
   -> ?pp_sep:(Format.formatter -> unit -> unit)
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 38f198955..992cbd457 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -92,14 +92,14 @@ module PulseTransferFunctions = struct
         Ok exec_state
 
 
-  let topl_small_step arguments (return, _typ) exec_state_res =
+  let topl_small_step procname arguments (return, _typ) exec_state_res =
     let arguments =
       List.map arguments ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload} -> fst arg_payload)
     in
     let return = Var.of_id return in
     let do_astate astate =
       let return = Option.map ~f:fst (Stack.find_opt return astate) in
-      let topl_event = PulseTopl.Call {return; arguments} in
+      let topl_event = PulseTopl.Call {return; arguments; procname} in
       AbductiveDomain.Topl.small_step topl_event astate
     in
     let do_one_exec_state (exec_state : Domain.t) : Domain.t =
@@ -125,8 +125,9 @@ module PulseTransferFunctions = struct
             :: rev_func_args ) )
     in
     let func_args = List.rev rev_func_args in
+    let callee_pname = proc_name_of_call call_exp in
     let model =
-      match proc_name_of_call call_exp with
+      match callee_pname with
       | Some callee_pname ->
           PulseModels.dispatch tenv callee_pname func_args
           |> Option.map ~f:(fun model -> (model, callee_pname))
@@ -153,7 +154,12 @@ module PulseTransferFunctions = struct
           r
     in
     let exec_state_res =
-      if Topl.is_deep_active () then topl_small_step func_args ret exec_state_res
+      if Topl.is_deep_active () then
+        match callee_pname with
+        | Some callee_pname ->
+            topl_small_step callee_pname func_args ret exec_state_res
+        | None ->
+            (* skip, as above for non-topl *) exec_state_res
       else exec_state_res
     in
     match get_out_of_scope_object call_exp actuals flags with
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index b2185c3a7..055382c74 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -86,9 +86,9 @@ type t =
   ; path_condition: PathCondition.t }
 [@@deriving yojson_of]
 
-let pp f {post; pre; path_condition; skipped_calls} =
-  F.fprintf f "@[<v>%a@;%a@;PRE=[%a]@;skipped_calls=%a@]" PathCondition.pp path_condition
-    PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls
+let pp f {post; pre; topl; path_condition; skipped_calls} =
+  F.fprintf f "@[<v>%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp path_condition
+    PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls PulseTopl.pp_state topl
 
 
 let set_path_condition path_condition astate = {astate with path_condition}
diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml
index 5d4f3c31c..a8e83e69f 100644
--- a/infer/src/pulse/PulseFormula.ml
+++ b/infer/src/pulse/PulseFormula.ml
@@ -1289,7 +1289,7 @@ type t =
 let ttrue = {known= Formula.ttrue; pruned= Atom.Set.empty; both= Formula.ttrue}
 
 let pp_with_pp_var pp_var fmt {known; pruned; both} =
-  F.fprintf fmt "@[known=%a,@;pruned=%a,@;both=%a@]@." (Formula.pp_with_pp_var pp_var) known
+  F.fprintf fmt "@[known=%a,@;pruned=%a,@;both=%a@]" (Formula.pp_with_pp_var pp_var) known
     (Atom.Set.pp_with_pp_var pp_var) pruned (Formula.pp_with_pp_var pp_var) both
 
 
diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml
index e093bfd75..0b6cb2c20 100644
--- a/infer/src/pulse/PulseInterproc.ml
+++ b/infer/src/pulse/PulseInterproc.ml
@@ -115,14 +115,6 @@ let visit call_state ~pre ~addr_callee ~addr_hist_caller =
       ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } )
 
 
-let pp f {AbductiveDomain.pre; post; topl; path_condition; skipped_calls} =
-  F.fprintf f "COND:@\n  @[%a@]@\n" PathCondition.pp path_condition ;
-  F.fprintf f "PRE:@\n  @[%a@]@\n" BaseDomain.pp (pre :> BaseDomain.t) ;
-  F.fprintf f "POST:@\n  @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t) ;
-  F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" SkippedCalls.pp skipped_calls ;
-  F.fprintf f "TOPL:@\n @[%a@]@\n" PulseTopl.pp_state topl
-
-
 (* {3 reading the pre from the current state} *)
 
 let add_call_to_trace proc_name call_location caller_history in_call =
@@ -542,7 +534,7 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
 let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post
     ~captured_vars_with_actuals ~formals ~actuals astate =
   L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name
-    (Pp.seq ~sep:"," Var.pp) formals pp pre_post ;
+    (Pp.seq ~sep:"," Var.pp) formals AbductiveDomain.pp pre_post ;
   let empty_call_state =
     {astate; subst= AddressMap.empty; rev_subst= AddressMap.empty; visited= AddressSet.empty}
   in
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index cd0dfa453..ffebf78a1 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -180,7 +180,9 @@ let realloc_pvar pvar location astate =
 let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate
 
 let havoc_id id loc_opt astate =
-  if Stack.mem (Var.of_id id) astate then write_id id (AbstractValue.mk_fresh (), loc_opt) astate
+  (* Topl needs to track the return value of a method; even if nondet now, it may be pruned later. *)
+  if Topl.is_deep_active () || Stack.mem (Var.of_id id) astate then
+    write_id id (AbstractValue.mk_fresh (), loc_opt) astate
   else astate
 
 
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
index 048c70431..f5a37cba5 100644
--- a/infer/src/pulse/PulsePathCondition.ml
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -230,6 +230,13 @@ type operand = Formula.operand =
   | LiteralOperand of IntLit.t
   | AbstractValueOperand of AbstractValue.t
 
+let pp_operand f = function
+  | LiteralOperand i ->
+      IntLit.pp f i
+  | AbstractValueOperand v ->
+      AbstractValue.pp f v
+
+
 let eval_citv_binop binop_addr bop op_lhs op_rhs citvs =
   let citv_of_op op citvs =
     match op with
diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli
index 0e13de008..abf64ba10 100644
--- a/infer/src/pulse/PulsePathCondition.mli
+++ b/infer/src/pulse/PulsePathCondition.mli
@@ -45,6 +45,8 @@ val and_callee :
 
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
 
+val pp_operand : Formatter.t -> operand -> unit
+
 val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> t -> t * new_eqs
 
 val eval_unop : AbstractValue.t -> Unop.t -> AbstractValue.t -> t -> t * new_eqs
diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml
index 765c0d9a9..74522a618 100644
--- a/infer/src/pulse/PulseTopl.ml
+++ b/infer/src/pulse/PulseTopl.ml
@@ -7,34 +7,237 @@
 
 open! IStd
 open PulseBasicInterface
+module L = Logging
 
 type value = AbstractValue.t
 
-type event = Call of {return: value option; arguments: value list}
+type event = Call of {return: value option; arguments: value list; procname: Procname.t}
 
-type vertex = string
+let pp_comma_seq f xs = Pp.comma_seq ~print_env:Pp.text_break f xs
 
-type register = string
+let pp_event f (Call {return; arguments; procname}) =
+  let procname = Procname.hashable_name procname (* as in [static_match] *) in
+  Format.fprintf f "@[call@ %a=%s(%a)@]" (Pp.option AbstractValue.pp) return procname
+    (pp_comma_seq AbstractValue.pp) arguments
+
+
+type vertex = ToplAutomaton.vindex
+
+type register = ToplAst.register_name
 
 type configuration = {vertex: vertex; memory: (register * value) list}
 
-(** Let P be the [path_condition] in the enclosing pulse state, and let Q be the [path_condition] in
-    the [simple_state] below. Then, the facts we know are P∧Q, and it should be that ∃V P∧Q,
-    where V are the abstract values mentioned in the pre/post-configurations of the simple state, is
-    equivalent to P. In other words, the facts in Q should not constrain program variables but may
-    constrain Topl registers. *)
+type predicate = Binop.t * PathCondition.operand * PathCondition.operand
+
 type simple_state =
   { pre: configuration  (** at the start of the procedure *)
   ; post: configuration  (** at the current program point *)
-  ; path_condition: PathCondition.t }
+  ; pruned: predicate list  (** path-condition for the automaton *) }
+
+(* TODO(rgrigore): use Formula.Atom.Set for [pruned]?? *)
 
 (* TODO: include a hash of the automaton in a summary to avoid caching problems. *)
+(* TODO: limit the number of simple_states to some configurable number (default ~5) *)
 type state = simple_state list
 
-let start () = (* TODO *) []
+let pp_predicate f (op, l, r) =
+  Format.fprintf f "@[%a%a%a@]" PathCondition.pp_operand l Binop.pp op PathCondition.pp_operand r
 
-let small_step _condition _event state = (* TODO *) state
 
-let large_step ~substitution:_ ~condition:_ ~callee_prepost:_ _state = (* TODO *) []
+let pp_mapping f (x, value) = Format.fprintf f "@[%s↦%a@]@," x AbstractValue.pp value
+
+let pp_memory f memory = Format.fprintf f "@[<2>[%a]@]" (pp_comma_seq pp_mapping) memory
+
+let pp_configuration f {vertex; memory} =
+  Format.fprintf f "@[{topl-config@;vertex=%d@;memory=%a}@]" vertex pp_memory memory
+
+
+let pp_simple_state f {pre; post; pruned} =
+  Format.fprintf f "@[<2>{topl-simple-state@;pre=%a@;post=%a@;pruned=(%a)}@]" pp_configuration pre
+    pp_configuration post (Pp.seq ~sep:"∧" pp_predicate) pruned
+
+
+let pp_state f = Format.fprintf f "@[<2>[ %a]@]" (pp_comma_seq pp_simple_state)
+
+let start () =
+  let a = Topl.automaton () in
+  let starts = ToplAutomaton.starts a in
+  let mk_memory =
+    let registers = ToplAutomaton.registers a in
+    fun () -> List.map ~f:(fun r -> (r, AbstractValue.mk_fresh ())) registers
+  in
+  let configurations = List.map ~f:(fun vertex -> {vertex; memory= mk_memory ()}) starts in
+  List.map ~f:(fun c -> {pre= c; post= c; pruned= []}) configurations
+
+
+let get env x =
+  match List.Assoc.find env ~equal:String.equal x with
+  | Some v ->
+      v
+  | None ->
+      L.die InternalError "TOPL: Cannot find %s. Should be caught by static checks" x
+
+
+let set = List.Assoc.add ~equal:String.equal
+
+let eval_guard memory tcontext guard =
+  let operand_of_value (value : ToplAst.value) : PathCondition.operand =
+    match value with
+    | Constant (LiteralInt x) ->
+        LiteralOperand (IntLit.of_int x)
+    | Register reg ->
+        AbstractValueOperand (get memory reg)
+    | Binding v ->
+        AbstractValueOperand (get tcontext v)
+  in
+  let conjoin_predicate pruned (predicate : ToplAst.predicate) =
+    match predicate with
+    | Binop (binop, l, r) ->
+        let l = operand_of_value l in
+        let r = operand_of_value r in
+        let binop = ToplUtils.binop_to binop in
+        (binop, l, r) :: pruned
+    | Value v ->
+        let v = operand_of_value v in
+        let one = PathCondition.LiteralOperand IntLit.one in
+        (Binop.Ne, v, one) :: pruned
+  in
+  List.fold ~init:[] ~f:conjoin_predicate guard
+
 
-let pp_state _formatter _state = (* TODO *) ()
+let apply_action tcontext assignments memory =
+  let apply_one memory (register, variable) = set memory register (get tcontext variable) in
+  List.fold ~init:memory ~f:apply_one assignments
+
+
+type tcontext = (ToplAst.variable_name * AbstractValue.t) list
+
+let pp_tcontext f tcontext =
+  Format.fprintf f "@[[%a]@]" (pp_comma_seq (Pp.pair ~fst:String.pp ~snd:AbstractValue.pp)) tcontext
+
+
+(** Returns a list of transitions whose pattern matches (e.g., event type matches). Each match
+    produces a tcontext (transition context), which matches transition-local variables to abstract
+    values. *)
+let static_match (Call {return; arguments; procname} as event) :
+    (ToplAutomaton.transition * tcontext) list =
+  (* TODO(rgrigore): if both [Topl.evaluate_static_guard] and [PulseTopl.static_match] remain, try to factor code. *)
+  let rev_arguments = List.rev arguments in
+  let procname = Procname.hashable_name procname in
+  let match_one t =
+    let ret c = Some (t, c) in
+    let f label =
+      let match_name () : bool =
+        let re = Str.regexp label.ToplAst.procedure_name in
+        Str.string_match re procname 0
+      in
+      let match_args () : (ToplAutomaton.transition * tcontext) option =
+        let match_formals formals =
+          let bind ~init rev_formals =
+            let f tcontext variable value = (variable, value) :: tcontext in
+            match List.fold2 ~init ~f rev_formals rev_arguments with
+            | Ok c ->
+                ret c
+            | Unequal_lengths ->
+                None
+          in
+          match (List.rev formals, return) with
+          | [], Some _ ->
+              None
+          | rev_formals, None ->
+              bind ~init:[] rev_formals
+          | r :: rev_formals, Some v ->
+              bind ~init:[(r, v)] rev_formals
+        in
+        Option.value_map ~default:(ret []) ~f:match_formals label.ToplAst.arguments
+      in
+      if match_name () then match_args () else None
+    in
+    let result = Option.value_map ~default:(ret []) ~f t.ToplAutomaton.label in
+    let pp_second pp f (_, x) = pp f x in
+    L.d_printfln "@[<2>PulseTopl.static_match:@;transition %a@;event %a@;result %a@]"
+      ToplAutomaton.pp_transition t pp_event event
+      (Pp.option (pp_second pp_tcontext))
+      result ;
+    result
+  in
+  ToplAutomaton.tfilter_map (Topl.automaton ()) ~f:match_one
+
+
+let conjoin_pruned path_condition pruned =
+  let f path_condition (op, l, r) =
+    let path_condition, _new_eqs = PathCondition.prune_binop ~negated:false op l r path_condition in
+    path_condition
+  in
+  List.fold ~init:path_condition ~f pruned
+
+
+let is_unsat path_condition pruned =
+  PathCondition.is_unsat_cheap (conjoin_pruned path_condition pruned)
+
+
+let negate_predicate =
+  Binop.(
+    function
+    | Eq, l, r ->
+        (Ne, l, r)
+    | Ne, l, r ->
+        (Eq, l, r)
+    | Ge, l, r ->
+        (Lt, r, l)
+    | Gt, l, r ->
+        (Le, r, l)
+    | Le, l, r ->
+        (Gt, r, l)
+    | Lt, l, r ->
+        (Ge, r, l)
+    | _ ->
+        L.die InternalError
+          "PulseTopl.negate_predicate should handle all outputs of ToplUtils.binop_to")
+
+
+let skip_pruned_of_nonskip_pruned nonskip_list =
+  IList.product (List.map ~f:(List.map ~f:negate_predicate) nonskip_list)
+
+
+let small_step path_condition event simple_states =
+  let tmatches = static_match event in
+  let evolve_transition memory (transition, tcontext) : (configuration * predicate list) list =
+    match transition.ToplAutomaton.label with
+    | None ->
+        (* "any" transition *)
+        [({vertex= transition.ToplAutomaton.target; memory}, [])]
+    | Some label ->
+        let pruned = eval_guard memory tcontext label.ToplAst.condition in
+        let memory = apply_action tcontext label.ToplAst.action memory in
+        [({vertex= transition.ToplAutomaton.target; memory}, pruned)]
+  in
+  let evolve_state_cond ({vertex; memory}, pruned) =
+    let path_condition = conjoin_pruned path_condition pruned in
+    let simplify result =
+      (* TODO(rgrigore): Remove from extra_pruned what is implied by path_condition *)
+      let f (_configuration, extra_pruned) = not (is_unsat path_condition extra_pruned) in
+      List.filter ~f result
+    in
+    let tmatches =
+      List.filter ~f:(fun (t, _) -> Int.equal vertex t.ToplAutomaton.source) tmatches
+    in
+    let nonskip = simplify (List.concat_map ~f:(evolve_transition memory) tmatches) in
+    let skip =
+      let nonskip_pruned_list = List.map ~f:snd nonskip in
+      let skip_pruned_list = skip_pruned_of_nonskip_pruned nonskip_pruned_list in
+      let f pruned = ({vertex; memory}, pruned) in
+      simplify (List.map ~f skip_pruned_list)
+    in
+    let add_old_pruned (configuration, extra_pruned) = (configuration, extra_pruned @ pruned) in
+    List.map ~f:add_old_pruned (List.rev_append nonskip skip)
+  in
+  let evolve_simple_state {pre; post; pruned} =
+    List.map ~f:(fun (post, pruned) -> {pre; post; pruned}) (evolve_state_cond (post, pruned))
+  in
+  let result = List.concat_map ~f:evolve_simple_state simple_states in
+  L.d_printfln "@[<2>PulseTopl.small_step:@;%a@ -> %a@]" pp_state simple_states pp_state result ;
+  result
+
+
+let large_step ~substitution:_ ~condition:_ ~callee_prepost:_ _state = (* TODO *) []
diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli
index 965b14f43..cffd8bef0 100644
--- a/infer/src/pulse/PulseTopl.mli
+++ b/infer/src/pulse/PulseTopl.mli
@@ -9,7 +9,7 @@ open! IStd
 
 type value = PulseAbstractValue.t
 
-type event = Call of {return: value option; arguments: value list}
+type event = Call of {return: value option; arguments: value list; procname: Procname.t}
 
 type state
 
diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml
index cbf50082b..ac6a2048d 100644
--- a/infer/src/topl/ToplAst.ml
+++ b/infer/src/topl/ToplAst.ml
@@ -13,7 +13,7 @@ type register_name = string
 
 type variable_name = string
 
-type constant = Exp.t
+type constant = LiteralInt of int
 
 type value = Constant of constant | Register of register_name | Binding of variable_name
 
diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml
index 4c68dcdb8..cbac3abac 100644
--- a/infer/src/topl/ToplAutomaton.ml
+++ b/infer/src/topl/ToplAutomaton.ml
@@ -169,3 +169,30 @@ let get_start_error_pairs a =
 let pp_message_of_state fmt (a, i) =
   let property, state = vname a i in
   Format.fprintf fmt "property %s reaches state %s" property state
+
+
+let starts a =
+  (* TODO(rgrigore): cache *)
+  let f i (_property, vname) = if String.equal vname "start" then Some i else None in
+  Array.to_list (Array.filter_mapi ~f a.states)
+
+
+let registers a =
+  (* TODO(rgrigore): cache *)
+  let do_assignment acc (r, _v) = String.Set.add acc r in
+  let do_action acc = List.fold ~init:acc ~f:do_assignment in
+  let do_value acc = ToplAst.(function Register r -> String.Set.add acc r | _ -> acc) in
+  let do_predicate acc =
+    ToplAst.(function Binop (_op, l, r) -> do_value (do_value acc l) r | _ -> acc)
+  in
+  let do_condition acc = List.fold ~init:acc ~f:do_predicate in
+  let do_label acc {ToplAst.action; condition} = do_action (do_condition acc condition) action in
+  let do_label_opt acc = Option.fold ~init:acc ~f:do_label in
+  let do_transition acc {label} = do_label_opt acc label in
+  String.Set.to_list (Array.fold ~init:String.Set.empty ~f:do_transition a.transitions)
+
+
+let tfilter_map a ~f = Array.to_list (Array.filter_map ~f a.transitions)
+
+let pp_transition f {source; target; label} =
+  Format.fprintf f "@[%d -> %d:@,%a@]" source target ToplAstOps.pp_label label
diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli
index 6a5e25b13..0aa48c56d 100644
--- a/infer/src/topl/ToplAutomaton.mli
+++ b/infer/src/topl/ToplAutomaton.mli
@@ -39,6 +39,8 @@ val vcount : t -> int
 
 val transition : t -> tindex -> transition
 
+val tfilter_map : t -> f:(transition -> 'a option) -> 'a list
+
 val is_skip : t -> tindex -> bool
 (** A transition is *skip* when it has no action, its guard is implied by all other guards, and its
     target equals its source. [is_skip automaton t] returns true when it can prove that [t] is skip.*)
@@ -54,3 +56,9 @@ val get_start_error_pairs : t -> (vindex * vindex) list
 
 val pp_message_of_state : Format.formatter -> t * tindex -> unit
 (** Print "property P reaches state E". *)
+
+val starts : t -> vindex list
+
+val registers : t -> ToplAst.register_name list
+
+val pp_transition : Format.formatter -> transition -> unit
diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml
index 1ea0e60e3..c1afc06b3 100644
--- a/infer/src/topl/ToplMonitor.ml
+++ b/infer/src/topl/ToplMonitor.ml
@@ -289,30 +289,16 @@ let generate_execute_state automaton proc_name =
       let exp_of_value =
         let open ToplAst in
         function
-        | Constant c ->
-            c
+        | Constant (LiteralInt x) ->
+            Exp.Const (Const.Cint (IntLit.of_int x))
         | Register i ->
             ToplUtils.static_var (ToplName.reg i)
         | Binding v ->
             ToplUtils.static_var (binding_of v)
       in
-      let expbinop = function
-        | ToplAst.OpEq ->
-            Binop.Eq
-        | ToplAst.OpNe ->
-            Binop.Ne
-        | ToplAst.OpGe ->
-            Binop.Ge
-        | ToplAst.OpGt ->
-            Binop.Gt
-        | ToplAst.OpLe ->
-            Binop.Le
-        | ToplAst.OpLt ->
-            Binop.Lt
-      in
       let predicate = function
         | ToplAst.Binop (op, v1, v2) ->
-            Exp.BinOp (expbinop op, exp_of_value v1, exp_of_value v2)
+            Exp.BinOp (ToplUtils.binop_to op, exp_of_value v1, exp_of_value v2)
         | ToplAst.Value v ->
             exp_of_value v
       in
diff --git a/infer/src/topl/ToplParser.mly b/infer/src/topl/ToplParser.mly
index 5c8c1ab69..ef7b03264 100644
--- a/infer/src/topl/ToplParser.mly
+++ b/infer/src/topl/ToplParser.mly
@@ -81,8 +81,8 @@ predicate:
 value:
     id=LID { ToplAst.Register id }
   | id=UID { ToplAst.Binding id }
-  | x=INTEGER { ToplAst.Constant (Exp.Const (Const.Cint (IntLit.of_int x))) }
-  | x=STRING  { ToplAst.Constant (Exp.Const (Const.Cstr x)) }
+  | x=INTEGER { ToplAst.Constant (LiteralInt x) (* (Exp.Const (Const.Cint (IntLit.of_int x)))*) }
+  (* TODO(rgrigore): Add string literals. *)
 
 predop_value: o=predop v=value { (o, v) }
 
diff --git a/infer/src/topl/ToplUtils.ml b/infer/src/topl/ToplUtils.ml
index 14f292179..2d0f18f95 100644
--- a/infer/src/topl/ToplUtils.ml
+++ b/infer/src/topl/ToplUtils.ml
@@ -52,6 +52,12 @@ let is_synthesized = function
       false
 
 
+let binop_to =
+  let open ToplAst in
+  let open Binop in
+  function OpEq -> Eq | OpNe -> Ne | OpGe -> Ge | OpGt -> Gt | OpLe -> Le | OpLt -> Lt
+
+
 let debug fmt =
   let mode = if Config.trace_topl then Logging.Quiet else Logging.Verbose in
   Logging.debug Analysis mode "ToplTrace: " ;
diff --git a/infer/src/topl/ToplUtils.mli b/infer/src/topl/ToplUtils.mli
index a9d45161d..d96cd7bf5 100644
--- a/infer/src/topl/ToplUtils.mli
+++ b/infer/src/topl/ToplUtils.mli
@@ -34,3 +34,5 @@ val is_synthesized : Procname.t -> bool
 val debug : ('a, Format.formatter, unit) IStd.format -> 'a
 
 val make_field : string -> Fieldname.t
+
+val binop_to : ToplAst.binop -> Binop.t