Goose: Timeline

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

36 check-ins using file bs/builtins/types/template/build.h version 00e9171ad7

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
20:30		simplified ref parsing implementation by using the parser's infix parsing rule helper refactored "requires" and "ensures": they are now simply infix operators that take a function type on the lhs and a proposition list on the rhs check-in: e1ede8dafa user: zlodo tags: trunk
2021-11-24
19:45		Propositions are now parsed like regular statement sequences, but using the proposition list under construction as the current builder check-in: 8be0ff932c user: zlodo tags: trunk
00:38		Removed a misleading comment check-in: ea3608d6e9 user: zlodo tags: trunk
00:03		Moved the hackish "cast" function from builtins to the prologue Fixed failed eager evaluation of builtin function calls raising erorrs, instead of being ignored Fixed the first local variable inside intrinsic functions getting a temporary index that aliases one of the params to hilarious effects check-in: b8498ed590 user: zlodo tags: trunk
2021-11-23
19:45		Parser: when encountering a prefix bracket block, parse it into a propositions list. Builtins: when a proposition list is dropped (ie used as a stand alone statement), convert it into assert instructions. Builtins: remove the builtin assert function, now replaced with the above so that propositions are always enclosed in brackets, regardless of where they are used. Also removes the confusion of making the assert function a compile-time check when its traditionally a runtime check check-in: 2ba2e560b1 user: zlodo tags: trunk
2021-11-22
20:33		Parser: split block parsing code check-in: a4eaf901ef user: zlodo tags: trunk
20:22		Function pre-conditions and post-conditions now use the same proposition lists as type predicates check-in: 1c335aeb04 user: zlodo tags: trunk
2021-11-19
22:28		Replaced "TypePredicates" by a more generic "Propositions" class, to be used for function predicates as well check-in: 098b3c34c9 user: zlodo tags: trunk
2021-11-16
21:18		The details of creating a new visibility scope are now handled by the builder instead of being hardcoded in the parser check-in: 16dd587889 user: zlodo tags: trunk
2021-11-13
14:09		The builder is now passed as the first param of the _DropValue extension point check-in: c33b227735 user: zlodo tags: trunk
2021-11-11
20:31		Removed two other obsolete files check-in: ade3099696 user: zlodo tags: trunk
20:19		Removed a file that was not properly deleted in the previous commit check-in: b808c4a5f5 user: zlodo tags: trunk
20:05		Refactored the code builder: it is now carried around as a Value, and accessed through a bunch of extension points, so we can have different builders (and even user defined ones) later to make classes etc. check-in: 1ad61a2717 user: zlodo tags: trunk
01:00		refactored the ref syntax again: "ref" is now an infix operator that takes an "AccessLevel" compile time value (mut/const/temp) on the lhs, or a TVar to capture/constrain it used the above feature to fix the constref verification _ConvertArg overload which was silently dereferencing the arg, causing it to get converted to a temp ref in all cases check-in: d679acf746 user: zlodo tags: trunk
2021-11-05
12:56		Fixed non mutable reference passing verification. It was a completely stupid error entirely in the prelude. I'm already fucking up using my own language, this bode well check-in: 0c58009de2 user: zlodo tags: trunk
2021-11-03
22:55		References: ref now creates a template type accepting any kind of reference, and mut/const/temp are prefix operators turning that into a ref (or template ref) type of the corresponding kind (this also changes the syntax from ref mut XXX to mut ref XXX which is more natural) Fixed the bizarely broken implicit referencing typechecking rule that performed a superfluous intermediate TypeCheck that crashed on non mutable template reference types Fixed builtin function wrapper that omitted a cast of the return value to the specified type, which allowed builtin functions to silently return values of a different type than advertised, resulting in fun type checking errors Fixed a bunch of fucked up return types that worked by chance (because of the above) in several g0 api functions Implemented non mutable reference passing verification + related tests (it doesn't work yet but too many fixes need to be committed first) check-in: 55994a469a user: zlodo tags: trunk
2021-11-01
11:16		Verifier: fixed verification taking a billion years in some cases check-in: ec2b1e3b74 user: zlodo tags: trunk
2021-10-31
18:52		Reverted most of the horribly complicated changes done since [b3ff9af3c2fe4925], other than the ability to hash all terms, values, instructions and predicates Solved the problem for which tests were added in [b3ff9af3c2fe4925] in a much simpler way check-in: 1fe5a1ac2b user: zlodo tags: trunk

Goose Timeline

36 check-ins using file bs/builtins/types/template/build.h version 00e9171ad7