Goose  Timeline

Advanced

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

87 check-ins using file bs/builtins/types/runtime/typecheck.cpp version ef34d352aa

2022-11-21
18:59
  • some fixes in #for base implementation
  • g0api: exposed functions to deconstructs decls
 check-in: ac0c5a2c6a user: zlodo tags: trunk
2022-11-20
10:49
g0api: expose some tuple and some parsing stuff check-in: ec453bb5a1 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
00:46
expose more compiler functionality to g0api:
  • local variable declarations
  • lifetime scopes
 check-in: 605ff0a654 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-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
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
Fossil 2.26 [1205ec86cb] 2025-04-30 16:57:32
This page was generated in about 0.027s