GitHub PullRequestReviewCommentEvent at 2014-08-20 09:28:27
Repository: souper
Actor: pcc
Payload: {"action":"created","comment":{"url":"https://api.github.com/repos/google/souper/pulls/comments/16466371","id":16466371,"diff_hunk":"@@ -441,6 +438,92 @@ ref<Expr> ExprBuilder::getInstMapping(const InstMapping &IM) {\n   return EqExpr::create(get(IM.Source), get(IM.Replacement));\n }\n \n+std::vector<ref<Expr> > ExprBuilder::getPhiPredicates(Inst *I) {\n+  assert(!PhiPredMap.count(I) && \"phi predicates exist\");\n+  const std::vector<Inst *> &Ops = I->orderedOps();\n+  std::vector<ref<Expr> > PredExpr;\n+  for (unsigned J = 0; J < Ops.size()-1; ++J)\n+    PredExpr.push_back(makeSizedArrayRead(1, \"blockpred\", I));\n+  PhiPredMap[I] = PredExpr;\n+  return PredExpr;\n+}\n+\n+ref<Expr> ExprBuilder::getUBInstCondition() {\n+  ref<Expr> Result = klee::ConstantExpr::create(1, Expr::Bool);\n+  std::set<Inst *> UsedUBInst;\n+  // For each Phi node\n+  for (const auto &V : PhiPredMap) {\n+    // For each Phi operand\n+    for (unsigned A = 0; A < V.first->Ops.size(); ++A) {\n+      std::vector<Inst *> UBInst;\n+      // Scan for UB instructions\n+      getUBInstructions(V.first->Ops[A], UBInst);\n+      if (UBInst.size() > 0) {\n+        ref<Expr> Ante = klee::ConstantExpr::alloc(1, 1);\n+        // Collect UB constraints\n+        for (Inst *I : UBInst) {\n+          assert(UBExprMap.count(I) && \"UB instruction expression not found\");\n+          UsedUBInst.insert(I);\n+          Ante = AndExpr::create(Ante, UBExprMap[I]);\n+        }\n+        // Get operand predicate\n+        ref<Expr> Pred;\n+        if (A == 0)\n+          Pred = V.second[0];\n+        else\n+          Pred = Expr::createIsZero(V.second[A-1]);\n+        // Add predicate->UB constraint\n+        Result = AndExpr::create(Result, Expr::createImplies(Pred, Ante));\n+      }\n+    }\n+  }\n+  // Add the the remaining UB constraints\n+  for (const auto &Entry: UBExprMap) {\n+    if (!UsedUBInst.count(Entry.first)) {\n+      Result = AndExpr::create(Result, Entry.second);\n+    }\n+  }\n+  return Result;\n+}\n+\n+void ExprBuilder::getUBInstructions(Inst *I, std::vector<Inst *> &Insts) {\n+  switch (I->K) {\n+    default:\n+      break;\n+\n+    case Inst::AddNSW:\n+    case Inst::AddNUW:\n+    case Inst::AddNW:\n+    case Inst::SubNSW:\n+    case Inst::SubNUW:\n+    case Inst::SubNW:\n+    case Inst::MulNSW:\n+    case Inst::MulNUW:\n+    case Inst::MulNW:\n+    case Inst::UDiv:\n+    case Inst::SDiv:\n+    case Inst::UDivExact:\n+    case Inst::SDivExact:\n+    case Inst::URem:\n+    case Inst::SRem:\n+    case Inst::Shl:\n+    case Inst::ShlNSW:\n+    case Inst::ShlNUW:\n+    case Inst::ShlNW:\n+    case Inst::LShr:\n+    case Inst::LShrExact:\n+    case Inst::AShr:\n+    case Inst::AShrExact:\n+      Insts.push_back(I);\n+      break;\n+  }\n+\n+  const std::vector<Inst *> &Ops = I->orderedOps();\n+  for (unsigned J = 0; J != Ops.size(); ++J) {","path":"lib/Extractor/KLEEBuilder.cpp","position":282,"original_position":282,"commit_id":"619ab100a7dd19f17f07931427d435d19b71e0f0","original_commit_id":"619ab100a7dd19f17f07931427d435d19b71e0f0","user":{"login":"pcc","id":425024,"avatar_url":"https://avatars.githubusercontent.com/u/425024?v=2","gravatar_id":"77dd5d8abf56481edd062b2c2aadc6df","url":"https://api.github.com/users/pcc","html_url":"https://github.com/pcc","followers_url":"https://api.github.com/users/pcc/followers","following_url":"https://api.github.com/users/pcc/following{/other_user}","gists_url":"https://api.github.com/users/pcc/gists{/gist_id}","starred_url":"https://api.github.com/users/pcc/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/pcc/subscriptions","organizations_url":"https://api.github.com/users/pcc/orgs","repos_url":"https://api.github.com/users/pcc/repos","events_url":"https://api.github.com/users/pcc/events{/privacy}","received_events_url":"https://api.github.com/users/pcc/received_events","type":"User","site_admin":false},"body":"What if this is a phi node?","created_at":"2014-08-20T09:28:27Z","updated_at":"2014-08-20T09:28:27Z","html_url":"https://github.com/google/souper/pull/37#discussion_r16466371","pull_request_url":"https://api.github.com/repos/google/souper/pulls/37","_links":{"self":{"href":"https://api.github.com/repos/google/souper/pulls/comments/16466371"},"html":{"href":"https://github.com/google/souper/pull/37#discussion_r16466371"},"pull_request":{"href":"https://api.github.com/repos/google/souper/pulls/37"}}},"pull_request":{"url":"https://api.github.com/repos/google/souper/pulls/37","id":20019069,"html_url":"https://github.com/google/souper/pull/37","diff_url":"https://github.com/google/souper/pull/37.diff","patch_url":"https://github.com/google/souper/pull/37.patch","issue_url":"https://api.github.com/repos/google/souper/issues/37","number":37,"state":"open","locked":false,"title":"Fix proposal for unsoundness issue #13 + test case","user":{"login":"rsas","id":8187588,"avatar_url":"https://avatars.githubusercontent.com/u/8187588?v=2","gravatar_id":"683b6d26717839e2e8116ddfd23edfb4","url":"https://api.github.com/users/rsas","html_url":"https://github.com/rsas","followers_url":"https://api.github.com/users/rsas/followers","following_url":"https://api.github.com/users/rsas/following{/other_user}","gists_url":"https://api.github.com/users/rsas/gists{/gist_id}","starred_url":"https://api.github.com/users/rsas/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/rsas/subscriptions","organizations_url":"https://api.github.com/users/rsas/orgs","repos_url":"https://api.github.com/users/rsas/repos","events_url":"https://api.github.com/users/rsas/events{/privacy}","received_events_url":"https://api.github.com/users/rsas/received_events","type":"User","site_admin":false},"body":"This patch addresses the unsoundness issue #13. The idea is to first collect the UB constraints and then add them together with the Phi node predicates. If no Phi nodes exist, add the UB constraints directly as instruction conditions. The recursive parsing at each Phi node can be improved, but we should discuss the proposed solution first.","created_at":"2014-08-20T00:41:38Z","updated_at":"2014-08-20T09:28:27Z","closed_at":null,"merged_at":null,"merge_commit_sha":"e3d6580c86e0e5cf04020a2d88626f0c745240ca","assignee":null,"milestone":null,"commits_url":"https://api.github.com/repos/google/souper/pulls/37/commits","review_comments_url":"https://api.github.com/repos/google/souper/pulls/37/comments","review_comment_url":"https://api.github.com/repos/google/souper/pulls/comments/{number}","comments_url":"https://api.github.com/repos/google/souper/issues/37/comments","statuses_url":"https://api.github.com/repos/google/souper/statuses/619ab100a7dd19f17f07931427d435d19b71e0f0","head":{"label":"rsas:issue13-fix","ref":"issue13-fix","sha":"619ab100a7dd19f17f07931427d435d19b71e0f0","user":{"login":"rsas","id":8187588,"avatar_url":"https://avatars.githubusercontent.com/u/8187588?v=2","gravatar_id":"683b6d26717839e2e8116ddfd23edfb4","url":"https://api.github.com/users/rsas","html_url":"https://github.com/rsas","followers_url":"https://api.github.com/users/rsas/followers","following_url":"https://api.github.com/users/rsas/following{/other_user}","gists_url":"https://api.github.com/users/rsas/gists{/gist_id}","starred_url":"https://api.github.com/users/rsas/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/rsas/subscriptions","organizations_url":"https://api.github.com/users/rsas/orgs","repos_url":"https://api.github.com/users/rsas/repos","events_url":"https://api.github.com/users/rsas/events{/privacy}","received_events_url":"https://api.github.com/users/rsas/received_events","type":"User","site_admin":false},"repo":{"id":21929888,"name":"souper","full_name":"rsas/souper","owner":{"login":"rsas","id":8187588,"avatar_url":"https://avatars.githubusercontent.com/u/8187588?v=2","gravatar_id":"683b6d26717839e2e8116ddfd23edfb4","url":"https://api.github.com/users/rsas","html_url":"https://github.com/rsas","followers_url":"https://api.github.com/users/rsas/followers","following_url":"https://api.github.com/users/rsas/following{/other_user}","gists_url":"https://api.github.com/users/rsas/gists{/gist_id}","starred_url":"https://api.github.com/users/rsas/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/rsas/subscriptions","organizations_url":"https://api.github.com/users/rsas/orgs","repos_url":"https://api.github.com/users/rsas/repos","events_url":"https://api.github.com/users/rsas/events{/privacy}","received_events_url":"https://api.github.com/users/rsas/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/rsas/souper","description":null,"fork":true,"url":"https://api.github.com/repos/rsas/souper","forks_url":"https://api.github.com/repos/rsas/souper/forks","keys_url":"https://api.github.com/repos/rsas/souper/keys{/key_id}","collaborators_url":"https://api.github.com/repos/rsas/souper/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/rsas/souper/teams","hooks_url":"https://api.github.com/repos/rsas/souper/hooks","issue_events_url":"https://api.github.com/repos/rsas/souper/issues/events{/number}","events_url":"https://api.github.com/repos/rsas/souper/events","assignees_url":"https://api.github.com/repos/rsas/souper/assignees{/user}","branches_url":"https://api.github.com/repos/rsas/souper/branches{/branch}","tags_url":"https://api.github.com/repos/rsas/souper/tags","blobs_url":"https://api.github.com/repos/rsas/souper/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/rsas/souper/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/rsas/souper/git/refs{/sha}","trees_url":"https://api.github.com/repos/rsas/souper/git/trees{/sha}","statuses_url":"https://api.github.com/repos/rsas/souper/statuses/{sha}","languages_url":"https://api.github.com/repos/rsas/souper/languages","stargazers_url":"https://api.github.com/repos/rsas/souper/stargazers","contributors_url":"https://api.github.com/repos/rsas/souper/contributors","subscribers_url":"https://api.github.com/repos/rsas/souper/subscribers","subscription_url":"https://api.github.com/repos/rsas/souper/subscription","commits_url":"https://api.github.com/repos/rsas/souper/commits{/sha}","git_commits_url":"https://api.github.com/repos/rsas/souper/git/commits{/sha}","comments_url":"https://api.github.com/repos/rsas/souper/comments{/number}","issue_comment_url":"https://api.github.com/repos/rsas/souper/issues/comments/{number}","contents_url":"https://api.github.com/repos/rsas/souper/contents/{+path}","compare_url":"https://api.github.com/repos/rsas/souper/compare/{base}...{head}","merges_url":"https://api.github.com/repos/rsas/souper/merges","archive_url":"https://api.github.com/repos/rsas/souper/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/rsas/souper/downloads","issues_url":"https://api.github.com/repos/rsas/souper/issues{/number}","pulls_url":"https://api.github.com/repos/rsas/souper/pulls{/number}","milestones_url":"https://api.github.com/repos/rsas/souper/milestones{/number}","notifications_url":"https://api.github.com/repos/rsas/souper/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/rsas/souper/labels{/name}","releases_url":"https://api.github.com/repos/rsas/souper/releases{/id}","created_at":"2014-07-17T05:36:06Z","updated_at":"2014-07-01T01:26:49Z","pushed_at":"2014-08-20T01:20:42Z","git_url":"git://github.com/rsas/souper.git","ssh_url":"git@github.com:rsas/souper.git","clone_url":"https://github.com/rsas/souper.git","svn_url":"https://github.com/rsas/souper","homepage":null,"size":346,"stargazers_count":0,"watchers_count":0,"language":null,"has_issues":false,"has_downloads":true,"has_wiki":false,"forks_count":0,"mirror_url":null,"open_issues_count":0,"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"google:master","ref":"master","sha":"ad55aa36cab26db8a42625e342511fa75c67ff96","user":{"login":"google","id":1342004,"avatar_url":"https://avatars.githubusercontent.com/u/1342004?v=2","gravatar_id":"24ba30616d2a20673f54c2aee36d159e","url":"https://api.github.com/users/google","html_url":"https://github.com/google","followers_url":"https://api.github.com/users/google/followers","following_url":"https://api.github.com/users/google/following{/other_user}","gists_url":"https://api.github.com/users/google/gists{/gist_id}","starred_url":"https://api.github.com/users/google/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/google/subscriptions","organizations_url":"https://api.github.com/users/google/orgs","repos_url":"https://api.github.com/users/google/repos","events_url":"https://api.github.com/users/google/events{/privacy}","received_events_url":"https://api.github.com/users/google/received_events","type":"Organization","site_admin":false},"repo":{"id":18458047,"name":"souper","full_name":"google/souper","owner":{"login":"google","id":1342004,"avatar_url":"https://avatars.githubusercontent.com/u/1342004?v=2","gravatar_id":"24ba30616d2a20673f54c2aee36d159e","url":"https://api.github.com/users/google","html_url":"https://github.com/google","followers_url":"https://api.github.com/users/google/followers","following_url":"https://api.github.com/users/google/following{/other_user}","gists_url":"https://api.github.com/users/google/gists{/gist_id}","starred_url":"https://api.github.com/users/google/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/google/subscriptions","organizations_url":"https://api.github.com/users/google/orgs","repos_url":"https://api.github.com/users/google/repos","events_url":"https://api.github.com/users/google/events{/privacy}","received_events_url":"https://api.github.com/users/google/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/google/souper","description":null,"fork":false,"url":"https://api.github.com/repos/google/souper","forks_url":"https://api.github.com/repos/google/souper/forks","keys_url":"https://api.github.com/repos/google/souper/keys{/key_id}","collaborators_url":"https://api.github.com/repos/google/souper/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/google/souper/teams","hooks_url":"https://api.github.com/repos/google/souper/hooks","issue_events_url":"https://api.github.com/repos/google/souper/issues/events{/number}","events_url":"https://api.github.com/repos/google/souper/events","assignees_url":"https://api.github.com/repos/google/souper/assignees{/user}","branches_url":"https://api.github.com/repos/google/souper/branches{/branch}","tags_url":"https://api.github.com/repos/google/souper/tags","blobs_url":"https://api.github.com/repos/google/souper/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/google/souper/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/google/souper/git/refs{/sha}","trees_url":"https://api.github.com/repos/google/souper/git/trees{/sha}","statuses_url":"https://api.github.com/repos/google/souper/statuses/{sha}","languages_url":"https://api.github.com/repos/google/souper/languages","stargazers_url":"https://api.github.com/repos/google/souper/stargazers","contributors_url":"https://api.github.com/repos/google/souper/contributors","subscribers_url":"https://api.github.com/repos/google/souper/subscribers","subscription_url":"https://api.github.com/repos/google/souper/subscription","commits_url":"https://api.github.com/repos/google/souper/commits{/sha}","git_commits_url":"https://api.github.com/repos/google/souper/git/commits{/sha}","comments_url":"https://api.github.com/repos/google/souper/comments{/number}","issue_comment_url":"https://api.github.com/repos/google/souper/issues/comments/{number}","contents_url":"https://api.github.com/repos/google/souper/contents/{+path}","compare_url":"https://api.github.com/repos/google/souper/compare/{base}...{head}","merges_url":"https://api.github.com/repos/google/souper/merges","archive_url":"https://api.github.com/repos/google/souper/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/google/souper/downloads","issues_url":"https://api.github.com/repos/google/souper/issues{/number}","pulls_url":"https://api.github.com/repos/google/souper/pulls{/number}","milestones_url":"https://api.github.com/repos/google/souper/milestones{/number}","notifications_url":"https://api.github.com/repos/google/souper/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/google/souper/labels{/name}","releases_url":"https://api.github.com/repos/google/souper/releases{/id}","created_at":"2014-04-05T02:09:09Z","updated_at":"2014-08-13T05:00:15Z","pushed_at":"2014-08-19T21:40:47Z","git_url":"git://github.com/google/souper.git","ssh_url":"git@github.com:google/souper.git","clone_url":"https://github.com/google/souper.git","svn_url":"https://github.com/google/souper","homepage":null,"size":1032,"stargazers_count":74,"watchers_count":74,"language":"C++","has_issues":true,"has_downloads":true,"has_wiki":false,"forks_count":12,"mirror_url":null,"open_issues_count":7,"forks":12,"open_issues":7,"watchers":74,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/google/souper/pulls/37"},"html":{"href":"https://github.com/google/souper/pull/37"},"issue":{"href":"https://api.github.com/repos/google/souper/issues/37"},"comments":{"href":"https://api.github.com/repos/google/souper/issues/37/comments"},"review_comments":{"href":"https://api.github.com/repos/google/souper/pulls/37/comments"},"review_comment":{"href":"https://api.github.com/repos/google/souper/pulls/comments/{number}"},"commits":{"href":"https://api.github.com/repos/google/souper/pulls/37/commits"},"statuses":{"href":"https://api.github.com/repos/google/souper/statuses/619ab100a7dd19f17f07931427d435d19b71e0f0"}}}}