* overall
** rename accumulators from [z] to [s] for "state"
* cli
** find a better naming convention than .llair and .llair.txt
** add a command to generate text llair directly from bitcode
- maybe `sledge llvm disassemble`?
* config
* llvm
* import
** consider adding set ops that operate on a set and the domain of a map
(e.g. intersect a set with the domain of a subst), which could be reimplemented efficiently internally
** fix the order of args to ~f args to fold functions
** implement the rest of the Array operations in Vector
** automatically keep interface of Vector in sync with Array
* trace and ppx_trace
** if a traced fun has a type annotation
copy it to the left arg of |> and to the arg of Trace.retn
** use name of enclosing function that is a structure item
rather than nearest enclosing
* modeling
** translate memset to store, and remove memset inst
** change translation of `invoke _Znwm` (operator new) to possibly throw
depends on [[*generalize specs to express throwing exceptions][generalize specs to express throwing exceptions]]
** revise spec of strlen to account for non-max length strings
- consider an intrinsic to return the end of the block containing a pointer
* llair
** simplify combinations of mul and div, e.g. x * (y / z) ==> (x * y) / z
** ? add Not exp and represent e.g. Dq as Not Eq
to strengthen equality propagation power
** normalize polynomial equations by dividing coefficients by their gcd
** add config to pp e.g. Exp.t as sexps
** add check for variable non-occurrence to Exp.rename
** define Label module for Exp.Label and Llair.label
- to unify how functions and blocks are named
- the Exp.label construction in Control.exec_term Iswitch is unwieldy
** check/ensure that generated names do not clash
- name ^ ".ti" xlate_instr LandingPad
** check that Loc.pp follows GNU conventions
** ? change Var.freshen to choose the first available
analogous to the following version that is over just ints
#+BEGIN_SRC ocaml
let freshen x ~wrt =
  [%Trace.call fun _ -> ()]
  ;
  ( match Set.max_elt wrt with
  | None -> (x, Set.add wrt x)
  | Some max_elt ->
      let max = max_elt in
      let len = Set.length wrt in
      if len = max + 1 then
        let x' = max + 1 in
        (x', Set.add wrt x')
      else
        let rec freshen_ lb wrt ub =
          if Set.is_empty wrt then (lb, Set.add wrt lb)
          else
            let mid = (lb + ub) / 2 in
            match Set.split wrt mid with
            | lower, _, _ when Set.length lower < (ub - lb) / 2 ->
                freshen_ lb lower mid
            | _, None, _ -> (mid, Set.add wrt mid)
            | _, _, upper -> freshen_ (mid + 1) upper ub
        in
        freshen_ 0 wrt (max + 1) )
  |>
  [%Trace.retn fun _ (x', wrt') ->
    assert (Set.mem wrt' x') ;
    assert (not (Set.mem wrt x')) ;
    for id = 0 to id x' - 1 do
      assert (Set.mem wrt (Var {name= name x'; id}))
    done]
#+END_SRC
** ? rename loc to pos for source locations, to avoid clash with logic loc
** ? expose the roots computed by Llair.mk
** use type info to print e.g. p+o as p.f
will likely need to consult what p is equal to, to find some meaningful type, and it could easily take much more work than this to produce reliably readable results
** do not hardcode target-specific types and layout
- add a target module
- construct an instance in frontend as first step
- use it during translation
- return it as part of program
- pass it from Control to Domain, etc.
** function types could include the types of throw continuation args
but they are currently the same for all functions: i8*
** ? format #line directives in programs
** find a way to avoid the manually generated sexp functions in Llair
** change Abort from an inst to a term
** change string in Llair.functions to some informative type
main constraint is that these uses of string need to be compatible with the "name" of a global
** clarify typ arg of Exp constructors
change constructor functions to not take the Typ.t as a separate arg, but to take a pair of an Exp.t and a Typ.t to indicate what the Typ.t refers to
** change function Call arguments to always be variables
* frontend
** make filenames in debug locations relative, and do something with model and system header paths
** check if freturn and fthrow reg names in frontend can clash
** ? translate PtrToInt and IntToPtr as cast when sizes match
** use llvm.lifetime.{start,end} to determine where to (alloc and?) free locals
** hoist alloca's to the beginning of the entry block whenever they dominate the return instr
** clean up translation of intrinsics
separation between xlate_intrinsic (which translates an intrinsic function name to an expression constructor) and the Call case of xlate_instr (which translates calls to intrinsic functions to instructions) is not clear
** extract struct field names from llvm debug info
** normalize cfg
- remove unreachable blocks
- combine blocks with cmnd= []; term= Unreachable into one
** support variadic functions
- nothing prevents the compiler from generating code that directly manipulates the target-specific va_list struct, and it appears to do so at least for amd64, so the only safe approach is to use the same representation:
  #+BEGIN_SRC C
  typedef struct {
     unsigned int gp_offset;
     unsigned int fp_offset;
     void *overflow_arg_area;
     void *reg_save_area;
  } va_list[1];
  #+END_SRC
** support dynamic sized stack allocation (alloca in non-entry blocks) 
- lower by implementing in terms of the core
- add a linked list of stack slots data structure
- each element contains
  + a pointer to some memory allocated for that slot's contents
  + a pointer to the next older slot
- add a local variable 'top' to each function with a non-entry alloca; that points to a pointer that always points to the head of the stack; initially NULL
- alloca in non-entry blocks adds an element and stores the result of alloc in it, sets next to contents of 'top', and stores result into 'top'
- function return (and other popping terminators) traverses the stack, popping elements, calling free on the slot pointers, until finding NULL in next
- stacksave intrinsic returns a pointer to a stack element
- stackrestore intrinsic pops the stack like return but only back to the argument pointer
** handle inline asm enough to over-approximate control-flow
- inline asm can take addresses of blocks as args, that can be jumped to
- treating inline asm conservatively requires considering these control flows
** support missing intrinsics
** try to extract scope for `ConstantExpr` and `ConstantPointerNull` value types
** support vector operations
- by lowering into multiple scalar operations
- most cases handled by Frontend.transform
- tests have a few exceptions, possibly for only unrealistic code
** support multiple address spaces
- need to, at least, treat addrspacecast as converting between pointer types of different sizes
** exceptions
- operator new should possibly throw
- is it correct to translate landingpad clauses not matching to unreachable, or should the exception be re-thrown
- check suspicious translation of landingpads
  The translation of landingpads with cleanup and other clauses ignores the other clauses. This seems suspicious, is this semantics correct?
- handle subtyping
  + xlate_instr on LandingPad uses Eq and Ne of type_info values. This ignores subtyping. Subtyping info is encoded into the type_info values.
- ? implement c++ abi functions instead of using libcxxabi
  + implement eh abi in C
  + see cxxabi https://libcxxabi.llvm.org/spec.html and itanium abi http://itanium-cxx-abi.github.io/cxx-abi/abi-eh.html
  + __cxa_call_unexpected
    - translate to Unreachable, possibly warn
  + __cxa_get_exception_ptr
    - translate as identity function
  + __cxa_allocate_exception
    - translate to Alloc of exception struct type
  + __cxa_begin_catch
    - increment handler count of arg
    - add arg to caught stack unless it is already there (next not null iff in stack)
    - return arg
  + __cxa_rethrow
    - set rethrown field of top of caught stack, std::terminate if stack empty
    - call __cxa_throw on top of caught stack
  + __cxa_end_catch
    - find top of caught stack
    - decrement its handler count
      + if handler count reaches 0
        - remove from stack
        - if rethrown flag not set
          + call destructor
          + deallocate memory allocated by __cxa_allocate_exception
** ? run translate in a forked subprocess
- so that when llvm crashes it does not take down sledge and an error can be returned
- will require serializing an deserializing the translated program
- alternatively: install a signal handler to catch and recover from crashes from llvm
** scalarizer does not work on functions with [optnone] attribute
- repro: llvm/Transforms/FunctionAttrs/optnone-simple.ll
- one solution: pre-process llvm to remove [optnone] attributes before running scalarizer pass
** ? remove Exp.Nondet, replace with free variables
it is not obvious whether it will be simpler to use free variables instead of Nondet in the frontend, or to treat Nondet as a single-occurrence existential variable in the analyzer
** llvm bugs?
- `opt -S -ipsccp llvm/Transforms/SimplifyCFG/indirectbr.ll` crashes, which makes sledge crash in the same way because it calls `Llvm_ipo.add_ipsccp`
- Calling `size_in_bits` on `%struct.__sFILE = type { %struct.__sFILE }` from llvm/Verifier/recursive-struct-param.ll crashes even though `type_is_sized` holds
- Why aren't shufflevector instructions with zeroinitializer masks eliminated by the scalarizer pass?
* term
** rename 'simplification' to 'normalization' and 'simp' to 'norm' for consistency with Equality
** should Add and Mul have an Ap form like ApN
with a corresponding norm function to use in the exposed interface and e.g. map?
** refactor Term so that the representation type is private
for all of the module except for the normalization functions, to ensure with the type system that everything passed out of the external interface has been checked to satisfy the invariant
** try only after getting rid of redundant type definitions due to Base containers
* equality
** treat disequalities in Equality
** should handle equality and disequality simplification
- equalities of equalities to integers currently handled by Sh.pure
- doing it in Exp leads to violations of the subexp assertion on app1
** optimize: change Cls.t and Use.t from a list to an unbalanced tree data structure
- only need empty, add, union, map, fold, fold_map to be fast, so no need for balancing
- detecting duplicates probably not worth the time since if any occur, the only cost is adding a redundant equation to pnd which will be quickly processed
** optimize: when called from extend, norm_extend calls norm unnecessarily
** revise mli to two sections, one for a "relation" api (with merge, mem/check, etc) and one for a "formula" api (with and_, or_, etc.)
** ? assert terms in formulas are in the carrier
us and xs, or just fv?
** strengthen invariant
** optimize: combine use and cls into one map
since they (could) have the same domain
** optimize: can identity mappings in lkp be removed?
** ? maybe need Mul terms in carrier due to non-linear to linear abstraction
* symbolic heap
** the way that Sh normalization is done needs to be overhauled, need more pure consequences
** expose and use Sh.stars
** ? rename 'cong' to 'eqr'
** ? rename 'canon' to 'norm'
** normalize exps in terms of reps
- add operation to normalize by rewriting in terms of reps
- check for unsat
- call it in Exec.assume
** eliminate existentials
by changing Congruence reps to avoid existentials if possible and then normalizing Sh ito reps
** add exps in pure and pto (including memory siz and arr) to carrier
** Sh.with_pure is an underspeced, tightly coupled, API: replace
Sh.with_pure assumes that the replaced pure part is defined in the same vocabulary, induces the same congruence, etc. This API is fragile, and ought to be replaced with something that has simpler assumptions without imposing an excessive pessimization.
** optimize Sh.and_ with direct implementation
** perhaps it would be better to allow us and xs to intersect
but to rename xs when binding them or otherwise operating under the quantifier. But it might be an unnecessary complication to always have to deal with the potential for shadowing.
** consider how to detect unsat formulas
in relation to also wanting to express formulas in terms of congruence
class representatives in order to perform quantifier elimination. Is
there a way to detect unsat at the same time / as part of the same
normalization?
** consider hoisting existentials over disjunction:
#+BEGIN_SRC ocaml
  | _ ->
      let us = Set.union q1.us q2.us in
      let xs1, xs, xs2 = Set.diff_inter_diff q1.xs q2.xs in
      let us1 = Set.union q1.us xs in
      let us2 = Set.union q2.us xs in
      { us
      ; xs
      ; cong= Congruence.true_
      ; pure= []
      ; heap= []
      ; djns= [[{q1 with us= us1; xs= xs1}; {q2 with us= us2; xs= xs2}]] }
  | _ ->
      let xs1, vs1 = Set.inter_diff q1.xs q2.us in
      let xs2, vs2 = Set.inter_diff q2.xs q1.us in
      let us1 = Set.union q1.us vs1 in
      let us2 = Set.union q2.us vs2 in
      let us = Set.union q1.us q2.us in
      let xs = Set.union vs1 vs2 in
      { us
      ; xs
      ; cong= Congruence.true_
      ; pure= []
      ; heap= []
      ; djns= [[{q1 with us= us1; xs= xs1}; {q2 with us= us2; xs= xs2}]] }
#+END_SRC
** consider how to arrange to have a complete set of variables
at the top of formulas so that freshening wrt them is guaranteed not to clash with subformulas. This would allow removing the call to freshen_xs in rename, which is called on every subformula for every freshen/rename operation. Is it complicated to make us always include xs, as well as the us of the subformulas? That would allow the top-level us to serve as such a complete set of vars. How often would we need to compute us - xs?
** think about how to avoid having to manipulate disjunct formulas
unnecessarily, e.g. freshening, etc.
** ? should star strengthen djns with stem's cong
** optimize: refactor Sh.pure to avoid `Congruence.(and_eq true_ ...)`
** consider strengthening cong of or_ at price of freshening existentials
** consider using the append case when freshening existentials is needed
** strengthen Sh.pure_approx
* solver
** solve more existential equations in excise_exp
If sub.pure contains an equation involving an existential, add equation to min, remove the var from xs, continue. If all pure atoms normalize to true, added equations induce good existential witnesses, and excise will return them as part of min.
* symbolic execution
** change function call to use substitution instead of conjoining equalities to pass args
depends on [[*change function Call arguments to always be variables][change function Call arguments to always be variables]]
** narrow scope of existentials in specs
in calls to exec_spec, only vars in post need appear in xs, others can be existential in foot
** generalize specs to express throwing exceptions
* domain
** implement resolve_virtual to not skip virtual calls
** consider lazy renaming
- instead of eagerly constructing renaming substitutions, traverse the formula and lazily construct the renaming substitution map
- may be better in case there are many variables that do not occur in the formula
* relation
** refactor lifting in Domain to use something like
type 'a with_entry = {entry: State_domain.t; current: 'a}
type t = State_domain.t with_entry
type from_call = State_domain.from_call with_entry
* used globals
** consider moving used globals info from exec_opts to a field of func
* intervals
** do something smarter with intrinsics
** implement summarization
* control
** change Depths.t from environment- to state-like treatment
- currently each waiting state has an associated depths map
- the depths of all edges into a destination are joined
- could the depths be just threaded through Work.run instead?
- this would involve changing type x to Depths.t -> t -> Depths.t * t, and removing Depths.t from waiting_states
- separate joining depths from joining states
- i.e. Change to repeatedly pop edges as long as the dst is the same, and only join the states for those. This would involve keeping the waiting states in the priority queue, and removing the waiting states map entirely.
** change Work.run to move Domain.join into ~f
** canonicalize renamings in stacks
It seems possible that two edges will be distinct only due to differences between choice of fresh variable names for shadowed variables. It is not obvious that this could not lead to an infinite number of Edge.t values even without recursion. Using predictable names for local variables, such as a pair of the declared name and the depth of the stack, would avoid these difficulties.
* build
** adapt infer's dead code detection
- this does not work easily, due at least to issues with wrapped libraries
* test
** ban #include from test code
tests can be sensitive to different system headers
* optimization
** Control uses Var.Set for locals, but could benefit from a set with constant-time union