{"action":"created","issue":{"url":"https://api.github.com/repos/klee/klee/issues/198","labels_url":"https://api.github.com/repos/klee/klee/issues/198/labels{/name}","comments_url":"https://api.github.com/repos/klee/klee/issues/198/comments","events_url":"https://api.github.com/repos/klee/klee/issues/198/events","html_url":"https://github.com/klee/klee/pull/198","id":57838136,"number":198,"title":"Independent solver get initial values","user":{"login":"holycrap872","id":682536,"avatar_url":"https://avatars.githubusercontent.com/u/682536?v=3","gravatar_id":"","url":"https://api.github.com/users/holycrap872","html_url":"https://github.com/holycrap872","followers_url":"https://api.github.com/users/holycrap872/followers","following_url":"https://api.github.com/users/holycrap872/following{/other_user}","gists_url":"https://api.github.com/users/holycrap872/gists{/gist_id}","starred_url":"https://api.github.com/users/holycrap872/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/holycrap872/subscriptions","organizations_url":"https://api.github.com/users/holycrap872/orgs","repos_url":"https://api.github.com/users/holycrap872/repos","events_url":"https://api.github.com/users/holycrap872/events{/privacy}","received_events_url":"https://api.github.com/users/holycrap872/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":17,"created_at":"2015-02-16T18:38:57Z","updated_at":"2015-04-04T02:45:08Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/klee/klee/pulls/198","html_url":"https://github.com/klee/klee/pull/198","diff_url":"https://github.com/klee/klee/pull/198.diff","patch_url":"https://github.com/klee/klee/pull/198.patch"},"body":"The previous implementation simply passes the entire constraint forward\r\nwithout any factoring of the constraint at all. This is a problem\r\nsince it is highly likely that there are cached solutions to pieces\r\nof the constraint. The new implementation breaks the entire\r\nconstraint down into its requisite factors and passes each piece\r\nforward, one by one, down the solver chain. After an answer is\r\nreturned, it is integrated into a larger solution. Since, by\r\ndefinition, no factor can affect another, we can safely create a\r\nsolution to the larger constraint from the answers of its smaller\r\npieces.\r\n\r\nAfter completion, the changes:\r\n1) Pass all provided tests (other than ones that were expected to fail)\r\n2) Have been verified via -debug-validate-solver by a complete run through of 9 members of the bin-utils for\r\n--search=dfs with a halt being placed, and states dumped, after 500 forks\r\n--search=default with a halt being placed, and the states dumped, after 1000 forks\r\n3) Achieved significant speedup on test programs\r\n--search=dfs\r\na. On average 10% improvement (for example strings saw a decrease from 252 seconds to 162 seconds)\r\nb. Worst case (objcopy) saw decrease in performance of 27% (950 seconds to 1287 seconds)\r\n--search=default\r\na. On average 48% improvement (for example regElf saw a decrease from 1078 seconds to 884 seconds)\r\nb. Worse case (objcopy) saw decrease in performance of 15% (862 seconds to 1022 seconds)"},"comment":{"url":"https://api.github.com/repos/klee/klee/issues/comments/89488863","html_url":"https://github.com/klee/klee/pull/198#issuecomment-89488863","issue_url":"https://api.github.com/repos/klee/klee/issues/198","id":89488863,"user":{"login":"holycrap872","id":682536,"avatar_url":"https://avatars.githubusercontent.com/u/682536?v=3","gravatar_id":"","url":"https://api.github.com/users/holycrap872","html_url":"https://github.com/holycrap872","followers_url":"https://api.github.com/users/holycrap872/followers","following_url":"https://api.github.com/users/holycrap872/following{/other_user}","gists_url":"https://api.github.com/users/holycrap872/gists{/gist_id}","starred_url":"https://api.github.com/users/holycrap872/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/holycrap872/subscriptions","organizations_url":"https://api.github.com/users/holycrap872/orgs","repos_url":"https://api.github.com/users/holycrap872/repos","events_url":"https://api.github.com/users/holycrap872/events{/privacy}","received_events_url":"https://api.github.com/users/holycrap872/received_events","type":"User","site_admin":false},"created_at":"2015-04-04T02:45:08Z","updated_at":"2015-04-04T02:45:08Z","body":"I got a simple test case that shows the behavior in 3 quick steps.\r\n\r\nTest Case:\r\n<pre>\r\n/*\r\n * 1)\r\n * (Eq false\r\n *   (Ult 9 (Read w8 2 x)))\r\n *\r\n * 2)\r\n * (Eq false\r\n *   (Sle (Add w32 14\r\n *     (SExt w32 (Read w8 (Extract w32 0 (SExt w64 (Add w32 3\r\n *       (ZExt w32 (Read w8 2 x))))) const_arr1)))\r\n *         24))\r\n *\r\n * 3) \r\n * (Eq 8 (Read w8 2 x))\r\n *\r\n * YIELDS\r\n *\r\n * (Sle (Add w32 14\r\n *   (SExt w32 (Read w8 11 const_arr1)))\r\n *     24)\r\n */\r\nint run(unsigned char * x, unsigned char * y) {\r\n  y[6] = 15;\r\n\r\n  if(y[x[2] + 3] + 14 < 25){\r\n    if(x[2] == 8){\r\n      return 1;\r\n    }else{\r\n      return 2;\r\n    }\r\n  }else{\r\n    return 4;\r\n  }\r\n}\r\n\r\nint main() {\r\n    unsigned char x[4];\r\n    unsigned char y[255];\r\n    klee_make_symbolic(&x, sizeof x, \"x\");\r\n\r\n    return run(x, y);\r\n}\r\n</pre>\r\n\r\nKlee Setup:\r\n<pre>\r\nklee --use-query-log=solver:pc --search=dfs test0.o\r\n</pre>\r\n\r\nGDB Setup:\r\nSet your break point to lib/Expr/Constraints.cpp::ConstraintManager::rewriteConstraints.\r\nOn the third break point hit, you can watch as old[1] is simplified, but not completely.\r\n\r\nAs you can see, the simplifier tries to simplify the expression, but fails to do so completely.  I'm pretty sure the bug is that the ExprReplaceVisitor doesn't recognize that the const_arr is completely unconstrained.  My gut would say that there should be some meta check to see if there are any symbolic arrays that are invovled with the constant array.  If there aren't any interactions in the constraint (all constraints in the constraint manager?) then the constraint should be cleared.\r\n\r\nI'll try to work on a fix along with the accompanying test case.  If you have any hints on where to look/start, I'd appreciate because I don't have a ton of experience with this part of Klee.\r\n"}}