Goose: Timeline

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

32 check-ins using file tests/g0/verification/z3gen/e-z3gen-test-4.txt version 0148dc4e7e

2022-06-11
12:29		Verification now mostly works again, tests not re-enabled yet check-in: 17301ed8fc user: zlodo tags: cir-stack-language
2022-06-08
22:38		Refactored the verifier to use the stack-based CIR. It compiles but isn't re-enabled yet check-in: 4f05876cc2 user: zlodo tags: cir-stack-language
2022-05-28
17:17		Small optimization. check-in: f886c2d77c user: zlodo tags: cir-stack-language
2022-05-26
22:48		Merge mac build fixes from trunk check-in: 536a94f712 user: zlodo tags: cir-stack-language
22:42		Mac build fixes check-in: b8a2990900 user: zlodo tags: trunk
11:31		Re-enabled codegen and related tests, and adapted it to the now stack-based CIR language check-in: dd5c48041c user: zlodo tags: cir-stack-language
2022-05-25
17:28		Split function invocation code into several specialized versions for each function kind Almost fully completed the migration of CIR to a stack language Compilation-time execution works again check-in: 7992dbe59f user: zlodo tags: cir-stack-language
2022-05-23
09:04		Added a CIR instruction to push a constant on the stack check-in: 0d0130b939 user: zlodo tags: cir-stack-language
08:44		CIR instructions are now stored in lists Execute: handle the stack Converted some instructions to use the stack check-in: 0d5427d49b user: zlodo tags: cir-stack-language
2022-05-16
23:40		Temporarily disabled codegen, verification, and all the tests that can't work without these check-in: 5fc7b0623f user: zlodo tags: cir-stack-language
2022-05-15
19:25		cir: implemented a helper object to decorate operations such as calls with a prologue and an epilogue, not used yet. check-in: 2503738366 user: zlodo tags: trunk
2022-05-09
18:52		Verifier: implemented a new encoding for memory locations that lets the verifier deal correctly with aliasing Implemented test for the above Fixed a reference typechecking bug to celebrate a day ending in Y check-in: ead7162820 user: zlodo tags: trunk
2022-05-02
10:42		Updated dependencies check-in: 17cf663ede user: zlodo tags: trunk
2022-04-04
23:20		Fixed incorrect argument types for z3 func decls Fixed template ghost funcs Encode address calculations into z3 Added a typechecking rule to unwrap references of references (which happen when we pass a variable containing a reference) check-in: ef60c39ded user: zlodo tags: trunk
2022-03-25
18:42		Verifier: encode reference values address calculation into z3 expressions (for situations where they are used as values, rather than dereferenced) check-in: 0e33b524a6 user: zlodo tags: trunk
2022-03-15
22:54		Fix verification of loops that modify ghost func closures check-in: 6564792477 user: zlodo tags: trunk
2022-03-14
19:23		bracket blocks inlined in the code are no longer proposition lists but a new type of block to contain "ghost code" (ie a verification specific cfg) added a GhostBranch instruction to insert the above in the middle of regular code removed a bunch of hacks to ignore load/stores involving ghost funcs during execution and codegen since they are now separated from normal code using the above miscellaneous other refactorings and improvements as a result ghost code is now more flexible and can use idiomatic tuple assignments to exchange the values of two ghost function closures check-in: 68260b65f2 user: zlodo tags: trunk
2022-03-11
19:08		Verifier: handle ct_int types and ct_int constants check-in: 9b10735b71 user: zlodo tags: trunk
2022-03-01
00:29		Ghost functions: added tests and fixed a lot of bugs, it even seems that all this garbage is actually beginning to work check-in: 09337f6de9 user: zlodo tags: trunk
2022-02-18
17:36		refactored function parsing so that ghost function declarations can actually work (ie they don't expect a function body) some fixes in codegen to properly ignore statements involving ghost functions check-in: 07963466bf user: zlodo tags: trunk
2022-02-14
17:42		verifier: handle setting and retrieving the value of ghost function closures check-in: bef38cb315 user: zlodo tags: trunk
2022-02-02
01:08		verifier: build and cache z3 declarations for ghost funcs check-in: e607197fe9 user: zlodo tags: trunk
2022-01-31
18:07		ghost func invocation generates the ghost call CIR instruction (only allowed inside of propositions) check-in: c55193554e user: zlodo tags: trunk
2022-01-29
13:41		ghost funcs: added GhostCall CIR instruction check-in: 802b9820d4 user: zlodo tags: trunk
13:12		ghost functions parsing: ignore following brace block if any, since they don't have bodies check-in: b60fb08f17 user: zlodo tags: trunk
2022-01-28
17:41		Ghost functions: implemented "ghost" operator to mark a function or template function as ghost template functions can now be ghosts detect and reject mixing ghost and non ghost functions in the same overload set check-in: 26c724e318 user: zlodo tags: trunk
2022-01-27
18:33		Verifier: factored some code out of value tracker check-in: 480aaf534c user: zlodo tags: trunk
2022-01-25
18:57		FuncType: replace flags with a "kind" enum, add ghost kind check-in: 55c2184e6f user: zlodo tags: trunk
2022-01-24
19:09		Verifier: factor out variable tracking out of the builder so it can be reused to track other kind of values check-in: 6aa3486a16 user: zlodo tags: trunk
2022-01-07
20:02		Use non-experimental std::coroutine Get rid of fmt lib, use std::format instead check-in: 3b954688f3 user: zlodo tags: trunk
01:25		Verifier: fix missing loop context in error messages in some cases check-in: 55688826d9 user: zlodo tags: trunk
00:59		Verifier: fixed some errors in the implementation of the k-induction loop verification, which was breaking in some cases with nested loops Verifier: fixed some data flow bugs that resulted in losing track of the state of some local variables in some situations check-in: 43f03d4856 user: zlodo tags: trunk

Goose Timeline

32 check-ins using file tests/g0/verification/z3gen/e-z3gen-test-4.txt version 0148dc4e7e