{"action":"created","issue":{"url":"https://api.github.com/repos/tracer-x/klee/issues/158","repository_url":"https://api.github.com/repos/tracer-x/klee","labels_url":"https://api.github.com/repos/tracer-x/klee/issues/158/labels{/name}","comments_url":"https://api.github.com/repos/tracer-x/klee/issues/158/comments","events_url":"https://api.github.com/repos/tracer-x/klee/issues/158/events","html_url":"https://github.com/tracer-x/klee/pull/158","id":190257478,"number":158,"title":"WIP: Interpolation for Memory Bound Checks","user":{"login":"domainexpert","id":696558,"avatar_url":"https://avatars.githubusercontent.com/u/696558?v=3","gravatar_id":"","url":"https://api.github.com/users/domainexpert","html_url":"https://github.com/domainexpert","followers_url":"https://api.github.com/users/domainexpert/followers","following_url":"https://api.github.com/users/domainexpert/following{/other_user}","gists_url":"https://api.github.com/users/domainexpert/gists{/gist_id}","starred_url":"https://api.github.com/users/domainexpert/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/domainexpert/subscriptions","organizations_url":"https://api.github.com/users/domainexpert/orgs","repos_url":"https://api.github.com/users/domainexpert/repos","events_url":"https://api.github.com/users/domainexpert/events{/privacy}","received_events_url":"https://api.github.com/users/domainexpert/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-11-18T07:56:59Z","updated_at":"2016-11-30T06:31:03Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/tracer-x/klee/pulls/158","html_url":"https://github.com/tracer-x/klee/pull/158","diff_url":"https://github.com/tracer-x/klee/pull/158.diff","patch_url":"https://github.com/tracer-x/klee/pull/158.patch"},"body":"KLEE checks that pointer values are within bounds, which is a proof. This is an implementation of the Craig interpolation of these proofs via a *slackening* of the bounds of pointer values (replacing concrete pointer values with bounds on their values) to gain more subsumptions."},"comment":{"url":"https://api.github.com/repos/tracer-x/klee/issues/comments/263794631","html_url":"https://github.com/tracer-x/klee/pull/158#issuecomment-263794631","issue_url":"https://api.github.com/repos/tracer-x/klee/issues/158","id":263794631,"user":{"login":"domainexpert","id":696558,"avatar_url":"https://avatars.githubusercontent.com/u/696558?v=3","gravatar_id":"","url":"https://api.github.com/users/domainexpert","html_url":"https://github.com/domainexpert","followers_url":"https://api.github.com/users/domainexpert/followers","following_url":"https://api.github.com/users/domainexpert/following{/other_user}","gists_url":"https://api.github.com/users/domainexpert/gists{/gist_id}","starred_url":"https://api.github.com/users/domainexpert/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/domainexpert/subscriptions","organizations_url":"https://api.github.com/users/domainexpert/orgs","repos_url":"https://api.github.com/users/domainexpert/repos","events_url":"https://api.github.com/users/domainexpert/events{/privacy}","received_events_url":"https://api.github.com/users/domainexpert/received_events","type":"User","site_admin":false},"created_at":"2016-11-30T06:31:03Z","updated_at":"2016-11-30T06:31:03Z","body":"Current statistics on `Regexp.c` as at @8d3c619.\r\n```\r\nKLEE: done: Subsumption statistics\r\nKLEE: done:     Time for actual solver calls in subsumption check (ms) = 0\r\nKLEE: done:     Number of solver calls for subsumption check (failed) = 0 (0)\r\nKLEE: done:     Average table entries per subsumption checkpoint = 77.59\r\nKLEE: done:     Number of subsumption checks = 2418\r\nKLEE: done:     Average solver calls per subsumption check = 0.00\r\nKLEE: done: ITree method execution times (ms):\r\nKLEE: done:     setCurrentINode = 12.061\r\nKLEE: done:     remove = 47.881\r\nKLEE: done:     subsumptionCheck = 2390.58\r\nKLEE: done:     markPathCondition = 69.774\r\nKLEE: done:     split = 2.184\r\nKLEE: done:     executeOnNode = 91.146\r\nKLEE: done: ITreeNode method execution times (ms):\r\nKLEE: done:     getInterpolant = 0.554\r\nKLEE: done:     addConstraintTime = 0.332\r\nKLEE: done:     splitTime = 2.073\r\nKLEE: done:     execute = 84.66\r\nKLEE: done:     bindCallArguments = 13.105\r\nKLEE: done:     bindReturnValue = 5.815\r\nKLEE: done:     getStoredExpressions = 61.144\r\nKLEE: done:     getStoredCoreExpressions = 20.225\r\n\r\nKLEE: done: total instructions = 167803\r\nKLEE: done: completed paths = 651, among which\r\nKLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0\r\nKLEE: done:     average branching depth of completed paths = 20.1615\r\nKLEE: done:     average branching depth of subsumed paths = 14.3723\r\nKLEE: done:     average instructions of completed paths = 611.741\r\nKLEE: done:     average instructions of subsumed paths = 351.153\r\nKLEE: done:     subsumed paths = 137\r\nKLEE: done:     error paths = 62\r\nKLEE: done:     program exit paths = 452\r\nKLEE: done: generated tests = 591, among which\r\nKLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0\r\nKLEE: done:     subsumed tests = 137\r\nKLEE: done:     error tests = 2\r\nKLEE: done:     program exit tests = 452\r\n4.02user 0.05system 0:04.07elapsed 99%CPU (0avgtext+0avgdata 39364maxresident)k\r\n0inputs+14560outputs (0major+8378minor)pagefaults 0swaps\r\n```\r\nFor comparison, this is the statistics for the `master` branch.\r\n```\r\nKLEE: done: Subsumption statistics\r\nKLEE: done:     Time for actual solver calls in subsumption check (ms) = 0\r\nKLEE: done:     Number of solver calls for subsumption check (failed) = 0 (0)\r\nKLEE: done:     Average table entries per subsumption checkpoint = 30.46\r\nKLEE: done:     Number of subsumption checks = 1494\r\nKLEE: done:     Average solver calls per subsumption check = 0.00\r\nKLEE: done: ITree method execution times (ms):\r\nKLEE: done:     setCurrentINode = 5.538\r\nKLEE: done:     remove = 16.537\r\nKLEE: done:     subsumptionCheck = 712.784\r\nKLEE: done:     markPathCondition = 63.322\r\nKLEE: done:     split = 1.199\r\nKLEE: done:     executeOnNode = 45.617\r\nKLEE: done: ITreeNode method execution times (ms):\r\nKLEE: done:     getInterpolant = 0.243\r\nKLEE: done:     addConstraintTime = 0.178\r\nKLEE: done:     splitTime = 1.151\r\nKLEE: done:     execute = 42.748\r\nKLEE: done:     bindCallArguments = 7.865\r\nKLEE: done:     bindReturnValue = 2.528\r\nKLEE: done:     getStoredExpressions = 26.029\r\nKLEE: done:     getStoredCoreExpressions = 4.382\r\n\r\nKLEE: done: total instructions = 70849\r\nKLEE: done: completed paths = 310, among which\r\nKLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0\r\nKLEE: done:     average branching depth of completed paths = 15.6149\r\nKLEE: done:     average branching depth of subsumed paths = 14.8889\r\nKLEE: done:     average instructions of completed paths = 693.838\r\nKLEE: done:     average instructions of subsumed paths = 340.352\r\nKLEE: done:     subsumed paths = 162\r\nKLEE: done:     error paths = 20\r\nKLEE: done:     program exit paths = 128\r\nKLEE: done: generated tests = 292, among which\r\nKLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0\r\nKLEE: done:     subsumed tests = 162\r\nKLEE: done:     error tests = 2\r\nKLEE: done:     program exit tests = 128\r\n```\r\nWe should investigate why subsumption is less effective."}}
{"actor":{"display_login":"domainexpert"}}