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

List:       klee-commits
Subject:    [klee-commits] [klee/klee] f049ff: Added factory method for Arrays + hid constructors...
From:       Cristian Cadar <c.cadar () imperial ! ac ! uk>
Date:       2015-03-02 18:39:45
Message-ID: 54f4ae71a956b_5a9c3fcea653929c92331 () hookshot-fe6-cp1-prd ! iad ! github ! net ! mail
[Download RAW message or body]

Branch: refs/heads/master
  Home:   https://github.com/klee/klee
  Commit: f049ff3bc04daead8c3bb9f06e89e71e2054c82a
      https://github.com/klee/klee/commit/f049ff3bc04daead8c3bb9f06e89e71e2054c82a
  Author: Eric Rizzi <eric.rizzi@gmail.com>
  Date:   2015-02-22 (Sun, 22 Feb 2015)

  Changed paths:
    M include/klee/Expr.h
    M lib/Core/Executor.cpp
    M lib/Core/Memory.cpp
    M lib/Expr/Expr.cpp
    M lib/Expr/Parser.cpp
    M lib/SMT/SMTParser.cpp
    M unittests/Expr/ExprTest.cpp
    M unittests/Solver/SolverTest.cpp

  Log Message:
  -----------
  Added factory method for Arrays + hid constructors from outside calls

The way that Arrays were handled in the past led to the possibility of
aliasing issues.  This occured whenever a new branch discovered an array
for the first time.  Each branch would create a new instance of the same
array without seeing if it had been created before. Therefore, should a
new branch encounter the same state as some previous branch, the
previous branch's solution wouldn't satisfy the new state since they
didn't recognize they were referencing the same array.  By creating an
array factory that creates a single symbolic array, that problem is
handled.  Note: Concrete arrays should not be created by the factory
method since their values are never shared between branches.

The factory works by seeing if an array with a similar hash has been
created before (the hash is based on the name and size of array).  If
there has been it then searches through all of the arrays with the same
hash (stored in a vector) to see if there is one with an exact match.
If there is one, the address of this previously created equivalent
array is returned.  Otherwise, the newly created array is unique, it is
added to the map, and it's address is returned.

This aliasing issue can be seen by comparing the output of the
Dogfood/ImmutableSet.cpp test cases with and with out this commit.
Both act correctly, but the number of queries making it to the solver
in the previous version is much greater 244 vs 211.  This is because
the UBTree in the CexCachingSolver and the cache in the CachingSolver
do not recognize queries whose solutions were previously calculated
because it doesn't think the arrays in the two queries are the same.
While this does not cause an error, it does mean that extra calls are
made.


  Commit: 35117b9f9273d2465abe56ef11f89ca7477e3d91
      https://github.com/klee/klee/commit/35117b9f9273d2465abe56ef11f89ca7477e3d91
  Author: Cristian Cadar <c.cadar@imperial.ac.uk>
  Date:   2015-02-27 (Fri, 27 Feb 2015)

  Changed paths:
    M include/klee/Expr.h
    M lib/Core/Executor.cpp
    M lib/Core/Memory.cpp
    M lib/Expr/Expr.cpp
    M lib/Expr/Parser.cpp
    M lib/SMT/SMTParser.cpp
    M unittests/Expr/ExprTest.cpp
    M unittests/Solver/SolverTest.cpp

  Log Message:
  -----------
  Merge branch 'ArrayFactory' of https://github.com/holycrap872/klee into \
holycrap872-ArrayFactory


  Commit: 1c10b2b52a4f91f62bc9ef632032d7f0ade0307c
      https://github.com/klee/klee/commit/1c10b2b52a4f91f62bc9ef632032d7f0ade0307c
  Author: Cristian Cadar <c.cadar@imperial.ac.uk>
  Date:   2015-02-27 (Fri, 27 Feb 2015)

  Changed paths:
    M include/klee/Expr.h
    M lib/Core/Executor.cpp
    M lib/Core/Memory.cpp
    M lib/Expr/Expr.cpp
    M lib/Expr/Parser.cpp

  Log Message:
  -----------
  Improved some comments and fixed some formatting issues in the Array factory patch.


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

  Changed paths:
    M include/klee/Expr.h
    M lib/Core/Executor.cpp
    M lib/Core/Memory.cpp
    M lib/Expr/Expr.cpp
    M lib/Expr/Parser.cpp
    M lib/SMT/SMTParser.cpp
    M unittests/Expr/ExprTest.cpp
    M unittests/Solver/SolverTest.cpp

  Log Message:
  -----------
  Merge branch 'holycrap872-ArrayFactory'


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

  Changed paths:
    A test/Feature/MultiMkSym.c

  Log Message:
  -----------
  New regression test checking that the Array factory correctly distinguishes between \
arrays created at the same location but with different sizes


Compare: https://github.com/klee/klee/compare/3bd3789c2009...a2617b6bba5b



_______________________________________________
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]