{"push_id":1275943593,"size":9,"distinct_size":9,"ref":"refs/heads/GUPDR","head":"83fe88e5920aadd4b951484a69b6f9b7f190c4f1","before":"5f2d99bd2e81329dc86ba56de65b35699d33b68c","commits":[{"sha":"e998fb25b94aa6b1896859f444a6ddbf01ddc152","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"Tiny cleanup","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/e998fb25b94aa6b1896859f444a6ddbf01ddc152"},{"sha":"c42f5652fea71cf14cd858c1ee8c7d3b92f5b16f","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"Starting to collect counterexamples from PDR","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/c42f5652fea71cf14cd858c1ee8c7d3b92f5b16f"},{"sha":"6199e9c5aa575eced5cbfd3ffb94394807ff9e34","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"API comments","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/6199e9c5aa575eced5cbfd3ffb94394807ff9e34"},{"sha":"4df827d98c226ac3cb97a770d7252c7d2a067628","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"Using bounded model checking that mimics the abstract cex call tree to try and find a concrete counterexample, not just an abstract trace (which indicates that there is no universal summary for proving the program correct, it may still be correct).","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/4df827d98c226ac3cb97a770d7252c7d2a067628"},{"sha":"1ac3a1540c134381c2e36412b4ffe61972de80c2","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"Beginning to overcome quite a nasty bug: Ivy hides irrelevant model facts when representing the model as clauses, which is nice but introduces an abstraction which is problematic when we decompose a cex to a concrete *trace*.\nConsider the program:\naction coolest_check_renaming = {\n   local i1: iterator, i2: iterator {\n       assume ~cme(I);\n       assume i1 ~= i2;\n       call check_renaming(i2, i1);\n       #cme(I) := false;\n       call check_renaming(i1, i2);\n       if (~cme(I)) {\n           assume true\n       } else {\n           assume true\n       }\n   }\n}\nexport coolest_check_renaming\n\naction check_renaming(i1: iterator, i3: iterator) = {\n  if (i1 = i3) {\n    cme(i1) := true\n  }\n}\n\nwhich is erroneously reported as unsafe, but when with the commented line uncommented (cme(I) := false) it is considered the safe.\nThe reason is that the decomposition returns two transition (one for each call) but doesn't report on which of these cme(I) became true, because cme seems irrelevant to Ivy because it doesn't appear anywhere in the clauses. None of these transitions can be blocked, because if cme(I) doesn't change then the transition is valid but can be blocked if cme(I) does become true.\n\nTo circumvent this we concretize the transition by assuming that relations that don't appear anywhere are false, and hope that this concretization will not hurt our generalization where it's not essential due to the use of unsat_core.\n\nIn this commit adding information just on the cme() relation, to be completed for all relation symbols.","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/1ac3a1540c134381c2e36412b4ffe61972de80c2"},{"sha":"4fa10995ded39723b21cba099e03349cddbafabd","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"Concretizing countertraces with all relation symbols, completing the previous commit.","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/4fa10995ded39723b21cba099e03349cddbafabd"},{"sha":"9e357cc1865a5449cebd2fa4ad6e044f09b92caa","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"Also concretizing constant symbols. Consider for example the following program:\n\naction coolest_concretize_consts = {\n      call get_some_stale();\n      call cme_if_not_stale()\n}\nexport coolest_concretize_consts\n\naction get_some_stale = {\n     local i1: iterator {\n          stale(itr) := true\n     }\n}\n\naction cme_if_not_stale = {\n     if (~stale(I)) {\n         cme(I) := true\n     }\n}\n\nwhich is safe but without the concretization of the constant symbol \"itr\" we are unable to show this.","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/9e357cc1865a5449cebd2fa4ad6e044f09b92caa"},{"sha":"440788593bab2a31a3ad05bc9938286f3fe8e2b1","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"Changing comment, probably will need to concretize function symbols as well...","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/440788593bab2a31a3ad05bc9938286f3fe8e2b1"},{"sha":"83fe88e5920aadd4b951484a69b6f9b7f190c4f1","author":{"name":"yotamfe","email":"4e9fdc5f41f9e580a2b6a3c4d7dd99978a9d4d07@gmail.com"},"message":"Changing print just to commit this example: safe but not provable using purely universal summaries:\n\naction get_some_stale = {\n     local i1: iterator {\n          i1 := *;\n\t  stale(i1) := true\n     }\n}\n\naction cme_if_not_stale = {\n     if (~stale(I)) {\n         cme(I) := true\n     }\n}","distinct":true,"url":"https://api.github.com/repos/yotamfe/ivy/commits/83fe88e5920aadd4b951484a69b6f9b7f190c4f1"}]}
{"actor":{"display_login":"yotamfe"}}