[prev in list] [next in list] [prev in thread] [next in thread] 

List:       klee-commits
Subject:    [klee-commits] [klee/klee] b70e2d: Altered DenseSet and IndependentElementSet to reco...
From:       Cristian Cadar <c.cadar () imperial ! ac ! uk>
Date:       2015-08-03 15:02:28
Message-ID: 55bf82841cab_4833fe74841d2b8609bf () hookshot-fe6-cp1-prd ! iad ! github ! net ! mail
[Download RAW message or body]

Branch: refs/heads/master
  Home:   https://github.com/klee/klee
  Commit: b70e2d2e772748ac4e217881742ad55fcfb77096
      https://github.com/klee/klee/commit/b70e2d2e772748ac4e217881742ad55fcfb77096
  Author: Eric Rizzi <eric.rizzi@gmail.com>
  Date:   2015-03-10 (Tue, 10 Mar 2015)

  Changed paths:
    M lib/Solver/IndependentSolver.cpp

  Log Message:
  -----------
  Altered DenseSet and IndependentElementSet to record ref<Expr> involved

This is important for future changes to IndependentSolver::
getInitialValues() so that an incoming constraint can be broken
down into its smallest possible parts.  Each of these individual
parts may then be solved for and then the solutions to each piece
combined to create a final answer.

Finally, several fields which had previously been private are now
public to facilitate the smaller solutions being combined into a
larger solution.


  Commit: d9bcbba2c94086039c11c86200670639ee2ec19f
      https://github.com/klee/klee/commit/d9bcbba2c94086039c11c86200670639ee2ec19f
  Author: Eric Rizzi <eric.rizzi@gmail.com>
  Date:   2015-04-01 (Wed, 01 Apr 2015)

  Changed paths:
    M lib/Solver/IndependentSolver.cpp

  Log Message:
  -----------
  Added the ability to solve for all factors in a particular query.

This functionality is necessary in order to more effectively handle
calls to IndependentSolver::getInitialValues.  An incoming query will
be broken down into its smaller parts, and each piece will be solved
for. At the end, the pieces will be recombined into a larger solution.
The IndependentElementSet::getAllFactors() method takes a query and
breaks it down into all of it's non-interacting factors.  The
IndependentElementSet::calculateArrays() method calculates which
arrays are involved in a particular factor.


  Commit: 76b6ae9a16dcb643456a98a845dc8d44df3aa049
      https://github.com/klee/klee/commit/76b6ae9a16dcb643456a98a845dc8d44df3aa049
  Author: Eric Rizzi <eric.rizzi@gmail.com>
  Date:   2015-04-01 (Wed, 01 Apr 2015)

  Changed paths:
    M include/klee/util/Assignment.h
    M lib/Solver/IndependentSolver.cpp

  Log Message:
  -----------
  Commit of improved IndependentSolver::getIniitalValues().

Previous implementation simply passed the entire constraint forward
without any factoring of the constraint at all.  This is a problem
since it is highly likely that there are cached solutions to pieces
of the constraint.  The new implementation breaks the entire
constraint down into its requisite factors and passes each piece
forward, one by one, down the solver chain.  After an answer is
returned, it is integrated into a larger solution.  Since, by
definition, no factor can affect another, we can safely create a
solution to the larger constraint from the answers of its smaller
pieces.

The reconstruction of the solution is done by analyzing which parts of
an array a factor touches.  If the factor is the only one to reference
a particular array, then all of the values calculated in the solution
for that array are included in the final answer.  If the factor
references a particular element of the array (for example, arr[1]),
then only the value in index 1 of array arr will be included in the
solution.


  Commit: be37ac9605d380b7f36717338c2c520f375798c8
      https://github.com/klee/klee/commit/be37ac9605d380b7f36717338c2c520f375798c8
  Author: Eric Rizzi <eric.rizzi@gmail.com>
  Date:   2015-04-01 (Wed, 01 Apr 2015)

  Changed paths:
    M lib/Solver/IndependentSolver.cpp

  Log Message:
  -----------
  Added the function IndependentSolver::createdPointEvaluatesToTrue

This function should be used solely in assertion statements and is
intended as a sanity check to make sure that the solution constructed
by IndependentSolver::getInitialValues() produces and answer that in
fact satisfies the the query.


  Commit: c91a035e51d2023133d4767eeb99bb8931710876
      https://github.com/klee/klee/commit/c91a035e51d2023133d4767eeb99bb8931710876
  Author: Cristian Cadar <c.cadar@imperial.ac.uk>
  Date:   2015-08-03 (Mon, 03 Aug 2015)

  Changed paths:
    M include/klee/util/Assignment.h
    M lib/Solver/IndependentSolver.cpp

  Log Message:
  -----------
  Merge pull request #198 from holycrap872/IndependentSolverGetInitialValues

New version of the get initial values functionality which makes use of the independent solver.


Compare: https://github.com/klee/klee/compare/26f485384e24...c91a035e51d2

_______________________________________________
klee-commits mailing list
klee-commits@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-commits


[prev in list] [next in list] [prev in thread] [next in thread]