Goose: Timeline

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

50 most recent check-ins that include changes to files matching 'bs/verify/*'

2024-09-15
20:24		Add clang format settings, reformat everything check-in: 0db147f117 user: achavasse tags: cir-ssa-refactor
2024-09-13
21:05		Drop in the most apocalyptic changes: new CIR instruction structure, new sequence builder, new compile time address representation, do almost just the bare minimum to compile again. A few simple things are still working somehow check-in: 57d4d0c79e user: achavasse tags: cir-ssa-refactor
2024-08-31
14:05		Refactor Instruction to be just a variant instead of a class containing a variant and a clownshoes bunch of constructors check-in: 8ffbc35112 user: achavasse tags: cir-ssa-refactor
2024-03-14
23:23		add type wrapper for unresolved compile time identifier, move undefined identifier handling to dropValue() of those implemented dot operator for structs fixed struct lazy parsing implemented some tests for structs default construction fixed struct default ctor generation check-in: 75a719c020 user: zlodo tags: trunk
2024-02-09
18:05		Lowering: completely reworked all lowering to happen in the same two unified extension points upstream of all three CIR consumers check-in: 1793989d05 user: zlodo tags: trunk
2024-01-02
22:41		Structs: build the default ctor and add it as an overload of _Initialize. check-in: ad919df201 user: zlodo tags: trunk
2023-11-30
18:29		Handful of fixes and improvements from an abandoned refactor of inline funcs, will go for a different solution check-in: 5b069c9677 user: zlodo tags: trunk
2023-11-05
13:04		Implemented inline functions check-in: 96c02f37d1 user: zlodo tags: trunk
2023-08-27
22:30		Added "CallCheck" CIR instruction to request the verifier to check a bunch of func params like it was a real call Used the above to verify the arguments passed to ghost funcs check-in: 83971c96a4 user: zlodo tags: trunk
2023-08-24
21:55		Verifier: optimize the way CreateTemporary/GetTemporary are handled check-in: 942f3c4fe0 user: zlodo tags: trunk
2023-08-13
18:04		It turns out cmake hadn't, in fact, failed me for the last time: migrating back from meson to cmake check-in: 9722f7aa3f user: zlodo tags: trunk
2023-08-02
21:46		Implemented forall statement check-in: 32f94cd2e1 user: zlodo tags: trunk
2023-07-13
21:45		CIR, verifier: added forall quantified variables check-in: 20223acc66 user: zlodo tags: trunk
2023-07-06
18:25		Verification: add IsPrefixOf instruction check-in: 33d8f4d593 user: zlodo tags: trunk
2023-06-30
22:41		Verifier: Remove hardcoded handling of ref type from verifier, lower ref type to address for verification instead Complete the handling of address type and handle selecting+loading an address' lifetime, origin and path check-in: 1adbcaa805 user: zlodo tags: trunk
2023-06-22
23:33		Implemented lowering of Addresses into a tuple representation for verification check-in: 25b51220ed user: zlodo tags: trunk
2023-06-17
10:15		Remove MemLoc, it's redundant with cir::Address Added compîlation time sequence type Partially handle sequence type in the verifier (to be completed later) Added "SelectPath" builtin type for adress paths check-in: 08898dae70 user: zlodo tags: trunk
2023-05-31
21:34		Lifetimes: implemented verifier's z3 representation check-in: b1d4853b7f user: zlodo tags: trunk
2023-03-27
18:34		reworked value wrapping in intrinsics, unwrapping can now only happen for the returned value (for verification reasons) removed the _ConvertFuncArg extension point, replaced it with _ConvertFuncArgs that operates on all of the args (so that we can do cross argument things in the prelude, will be needed for lifetimes) check-in: f271454617 user: zlodo tags: trunk
2023-03-05
22:24		removed fmtlib, now use std::format vastly improved the overload resolution debugging tools prelude: started adding some extra error detection for small things that don't need to be builtin prelude: started working on implementing #for for tuples, some stuff needs to be addressed still fixed some type checking issue with wrapped args fixed superfluous nested lifetime scope in brace blocks (which caused redundant calls to some extension points) check-in: 4d4d76607a user: zlodo tags: trunk
2023-01-30
19:33		Implemented the _IsTrivialInitialization extension point to optimize tuple initialization in the same way as assignments check-in: d70fa1ef12 user: zlodo tags: trunk
2023-01-05
19:44		Fixed passing tuple by value to functions, which involved properly handling type checking of constant tuples containing computed data and some codegen bugs check-in: 9b8306c3af user: zlodo tags: trunk
2022-11-17
22:57		Remove an old z3 workaround that doesn't seem necessary anymore check-in: 44da39ac61 user: zlodo tags: trunk
22:43		g0api: visiblity scopes combined visibility/lifetime scopes check-in: 8546f1ef75 user: zlodo tags: trunk
2022-11-11
20:01		Implemented template tuples and vararg tuples Fixed a few issues with the verifier check-in: 08ffdaf6db user: zlodo tags: trunk
2022-07-22
00:36		Switch back to using fmtlib so we can build with clang 14 for stability and since nowadays we apparently can't expect to be able to use c++ features that were accepted in the standard 2 years ago :/ check-in: 7e6d3483ec user: zlodo tags: trunk
2022-07-04
21:48		Minor cleanup check-in: 29b4ebb32f user: zlodo tags: trunk
2022-06-30
19:06		Remove obsolete TODO check-in: 3f5776378b user: zlodo tags: trunk
17:58		Verifier: fix unique id generation to be done on a per function basis rather than globally to make the z3 generation tests more stable check-in: f4e40b75d7 user: zlodo tags: trunk
2022-06-29
21:47		The CIR is no longer made out of instructions that are basically expression trees, but is now instead a stack language to make it possible to insert verification instructions before and after the evaluation of individual function arguments check-in: 1f87fbda15 user: zlodo tags: trunk
21:39		Verifier: consider verification failed if we encountered anything funny that prevented us from translating the entire function cfg to z3, rather than silently ignoring it Verifier: fixed a case where the verifier would improperly bail out and do the above Verifier: fixed a nasty use-after-free caused by forgetting an ampersand. fucking c++ Closed-Leaf check-in: 9814f18b04 user: zlodo tags: cir-stack-language
2022-06-28
22:51		Removed an unusued file and a left over debugging profanity check-in: 6c5b747f5c user: zlodo tags: cir-stack-language
2022-06-27
16:56		cir: allow verification specific code and instructions to be interspersed with regular code again and added a function to filter them out before consuming the code in the interpreter and during codegen verification: better handling of non-representable types that don't involve giving up entirely on verifying the function g0 api: updated it to match the CIR changes prelude: adapted reference verification to the new CIR api check-in: b81d4242e3 user: zlodo tags: cir-stack-language
2022-06-23
20:01		Correctly handle ghost func applications as "storage locations" alongside regular addresses, fixes the remaining ghost func test check-in: 68da32e88b user: zlodo tags: cir-stack-language
2022-06-22
20:06		Re-implemented "addr modified by loop" stuff (except ghost func related stuff) and re-enabled loop verification tests check-in: a0a57b5e22 user: zlodo tags: cir-stack-language
2022-06-21
17:09		Implemented conversion of Address into a z3 expression, fixes ghostfunc test 4 Fixed handling of Ret terminator that didn't always pop the result value check-in: d2090773d9 user: zlodo tags: cir-stack-language
2022-06-18
18:51		Added a location id to all CIR instructions (needed with the stack based approach to locate intermediate results) Fixed a bunch of verifier errors Re-enabled most verifier tests, other than some requiring to re-implement a few more bits check-in: b4d5bdf6ec user: zlodo tags: cir-stack-language
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-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-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

Goose Timeline

50 most recent check-ins that include changes to files matching 'bs/verify/*'