Goose: Timeline

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

24 check-ins using file bs/builtins/types/reference/typecheck.cpp version cb9fa9c0ab

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
2021-12-09
18:31		Verifier graphviz vizualizer fixes and improvements check-in: 5a84c0610a user: zlodo tags: trunk
2021-12-08
20:05		Implemented a graphviz visualizer to help debugging the loop verifier check-in: 12fc470a72 user: zlodo tags: trunk
2021-11-28
13:34		Verification: fixed incorrect handling of type predicates in function parameters check-in: c066339928 user: zlodo tags: trunk
2021-11-26
22:42		Fixed adding predicates to a type alias created with using that modified the original type Fixed ambiguous parsing of using expressions that were mistook for overload redefinitions in some cases check-in: 35ff2a536e user: zlodo tags: trunk
00:37		Parser: if an infix rules fails to parse, backtrack Parser: it is now possible to define a contextual "default lhs value" Parser: if an infix operator fails parsing, it is retried as an infix operator, using the default lhs value if there is one available Type predicates: setup @val as the default lhs value inside of the proposition list context, so it is now possible to write u32[<10] instead of u32[@val<10] check-in: 0184a27429 user: zlodo tags: trunk
2021-11-25
21:21		Got rid of the where operator. Predicates are now added to types simply by following the type with a proposition list. check-in: 23ecb4f9cb user: zlodo tags: trunk

Goose Timeline

24 check-ins using file bs/builtins/types/reference/typecheck.cpp version cb9fa9c0ab