{"action":"created","issue":{"url":"https://api.github.com/repos/tracer-x/klee/issues/203","repository_url":"https://api.github.com/repos/tracer-x/klee","labels_url":"https://api.github.com/repos/tracer-x/klee/issues/203/labels{/name}","comments_url":"https://api.github.com/repos/tracer-x/klee/issues/203/comments","events_url":"https://api.github.com/repos/tracer-x/klee/issues/203/events","html_url":"https://github.com/tracer-x/klee/pull/203","id":213726888,"number":203,"title":"WIP: Stacked store","user":{"login":"domainexpert","id":696558,"avatar_url":"https://avatars2.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":3,"created_at":"2017-03-13T10:30:52Z","updated_at":"2017-04-19T09:30:54Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/tracer-x/klee/pulls/203","html_url":"https://github.com/tracer-x/klee/pull/203","diff_url":"https://github.com/tracer-x/klee/pull/203.diff","patch_url":"https://github.com/tracer-x/klee/pull/203.patch"},"body":"This is a re-implementation of Tracer-X value store as a stack, such that the local memory is cleared after a function is exited. This is to avoid the local memory of an already-exited function is stored in the interpolant. The following is a very simplified version of `Regexp.c` that may demonstrate the issue.\r\n```\r\n/*\r\n * An example that exhibits issue of not clearing local memory after\r\n * function exit in Tracer-X KLEE revision 08b728a, which results in\r\n * subsumption failure as defined memory in the interpolant is not\r\n * found in the memory of the state to be subsumed. This is because\r\n * some allocations in the state to be subsumed have not yet been\r\n * initialized, in particular, the allocation of the return value of\r\n * matchhere. The store to this allocation only happens shortly before\r\n * the return of the function, and therefore at most points during the\r\n * execution of the function, the value is undefined.\r\n *\r\n * In a stored interpolant, however, the do loop in matchhere may have\r\n * been executed for several iterations. This results in the return\r\n * value becomes defined (as it has been stored into before in some\r\n * iterations). It is included in the interpolant as the return value\r\n * is used in the if condition in the body of the do loop to prove\r\n * that control can only go one direction. This defined memory cannot\r\n * subsume the undefined memory in the state to be subsumed.\r\n *\r\n * The issue disappear when the \"do\" and \"while\" statements in\r\n * matchhere are removed.\r\n *\r\n * Simplified from simple regular expression matching in\r\n *   The Practice of Programming\r\n *   Brian W. Kernighan, Rob Pike\r\n *\r\n * The code with KLEE harness is obtained from the following\r\n * page of the KLEE tutorial on December 2015:\r\n *   http://klee.github.io/resources/Regexp.c.html\r\n */\r\n#ifdef LLBMC\r\n#include <llbmc.h>\r\n#else\r\n#include <klee/klee.h>\r\n#endif\r\n\r\nstatic int matchhere(char *re, char *text) {\r\n  if (re[0] == '\\0')\r\n     return 0;\r\n  if (re[1] == '*') {\r\n    char c = re[0];\r\n    re += 2;\r\n    do {\r\n      if (matchhere(re, text))\r\n        return 1;\r\n    } while (*text != '\\0' && *text++ == c);\r\n    return 0;\r\n  }\r\n  if (*text!='\\0' && re[0]==*text)\r\n    return matchhere(re+1, text+1);\r\n  return 0;\r\n}\r\n\r\n/*\r\n * Harness for testing with KLEE.\r\n */\r\n\r\n// The size of the buffer to test with.\r\n#define SIZE 7\r\n\r\nint main() {\r\n  // The input regular expression.\r\n  char re[SIZE];\r\n\r\n// Make the input symbolic.\r\n#ifdef LLBMC\r\n  for (int i = 0; i < SIZE; ++i) {\r\n    re[i] = __llbmc_nondef_char();\r\n  }\r\n#else\r\n  klee_make_symbolic(re, sizeof re, \"re\");\r\n#endif\r\n\r\n  // Try to match against a constant string \"hello\".\r\n  if (matchhere(re, \"hello\"))\r\n    return 1;\r\n  return 0;\r\n}\r\n```"},"comment":{"url":"https://api.github.com/repos/tracer-x/klee/issues/comments/295186387","html_url":"https://github.com/tracer-x/klee/pull/203#issuecomment-295186387","issue_url":"https://api.github.com/repos/tracer-x/klee/issues/203","id":295186387,"user":{"login":"domainexpert","id":696558,"avatar_url":"https://avatars2.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":"2017-04-19T09:30:54Z","updated_at":"2017-04-19T09:30:54Z","body":"Also to note that as @8506b40, loss of error report is noticeable with `basic/regexp_iteative.c`."}}
{"actor":{"display_login":"domainexpert"}}