Goose  Timeline

Advanced

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

68 check-ins using file bs/parse/resolver.h version 13e3db5fdb

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-09-02
21:42
  • Implemented a test for variadic functions
  • Fixed a million issues and missing things preventing the above from working
  • Implemented equality operators for types
 check-in: 373a6ebd57 user: zlodo tags: trunk
2022-08-29
20:42
Partial implementation of compile-time for loop (rest to be done in prelude but needs a handful additional apis) check-in: 24b6c5ae2e user: zlodo tags: trunk
2022-08-28
17:12
vararg templates: completed the pack TExpr and pack TVars implementations (need tests) check-in: 0146622968 user: zlodo tags: trunk
2022-07-30
11:41
varargs: simplify (not going to attempt handling nesting repetitions after all) check-in: 4c0f447d59 user: zlodo tags: trunk
2022-07-25
17:23
vararg templates: set the signature of pack texprs as the repeating part of the vector, and diagnose packs not appearing last check-in: 27cf09cdf5 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-21
01:09
Small cleanup check-in: 6e0a90698d user: zlodo tags: trunk
2022-07-20
19:22
vararg template: added pack TExpr and ellipsis operator check-in: ba07901758 user: zlodo tags: trunk
2022-07-18
23:45
vararg templates: added a "prepare template" step prior to generating the template signature, which does nothing yet check-in: fe34bd71de user: zlodo tags: trunk
00:14
Keep track of the repetition depth of pack TVars, and assign a new value index for each repetition of a pack hole check-in: a2a6841c8b user: zlodo tags: trunk
2022-07-17
10:51
Fixed a bug in the verification instruction filter that somehow resulted in failed tests only on mac check-in: 64463a60a6 user: zlodo tags: trunk
2022-07-16
14:42
Varargs: added a "nested repetition depth" property to holes check-in: 97ff23912a user: zlodo tags: trunk
2022-07-05
22:10
TypeChecking: keep track of nested repetition indices for each sub context check-in: 95bdac72ca user: zlodo tags: trunk
2022-07-04
21:48
Minor cleanup check-in: 29b4ebb32f user: zlodo tags: trunk
21:20
typechecking: refactor type checking context to be able to hold more sub-context information than hole namespace indices check-in: 9fd8a2a87e user: zlodo tags: trunk
17:45
Refactored some template rules and type checking rules to avoid calling BuildTemplateSignature from inside type checking rules check-in: 64224a915f user: zlodo tags: trunk
2022-07-02
14:22
Vararg templates: function param decls with open tuple types are expanded into multiple params check-in: ecd5b0e89a 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
22:23
codegen: improved the translation of address computations into llvm GEP instructions check-in: 2a03dd67e5 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:56
Ported most of the g0 api to the new CIR language check-in: 9eb48e68a1 user: zlodo tags: cir-stack-language
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:26
Removed a bit of dead code check-in: b78a3ea203 user: zlodo tags: cir-stack-language
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-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
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
Fossil 2.26 [1205ec86cb] 2025-04-30 16:57:32
This page was generated in about 0.021s