Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
149 check-ins using file bs/builtins/types/template/tvar.cpp version 540c1850ce
|
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 |
| |
|
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 |
| |
|
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 |
| |
|
2022-06-18
| ||
| 18:51 |
| |
|
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 |
| |
|
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 |
| |
|
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 |
| |
|
2022-05-02
| ||
| 10:42 | Updated dependencies check-in: 17cf663ede user: zlodo tags: trunk | |
|
2022-04-04
| ||
| 23:20 |
| |
|
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 |
| |
|
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 |
| |
|
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:
| |
|
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 |
| |
| 01:25 | Verifier: fix missing loop context in error messages in some cases check-in: 55688826d9 user: zlodo tags: trunk | |
| 00:59 |
| |
|
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 |
| |
| 00:37 |
| |
|
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 |
| |
|
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 |
| |
|
2021-11-23
| ||
| 19:45 |
| |
|
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 |
| |
|
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 |
| |
|
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 |
| |
|
2021-10-30
| ||
| 22:51 |
| |
|
2021-10-29
| ||
| 20:03 | Template rules: implemented a function to setup bindings for captured predicates check-in: eccb9be7b9 user: zlodo tags: trunk | |
|
2021-10-28
| ||
| 21:48 | Template rules: implemented a function to extract the type predicate hashes of captured types check-in: 8fe613b1ac user: zlodo tags: trunk | |
| 20:25 | Template: split template function verification from instantiation check-in: 84723188cd user: zlodo tags: trunk | |
|
2021-10-27
| ||
| 22:23 | Func: CompileFunc() doesn't perform function verification anymore, there's now a separate CompileAndVerifyFunc() for that check-in: 562bf11329 user: zlodo tags: trunk | |
| 20:55 | Parser: when building a function, if its parent identity depends on type predicates captured by template vars, build it as a template function instead. check-in: 45078c42df user: zlodo tags: trunk | |
|
2021-10-26
| ||
| 18:43 | Type predicates: implemented helper functions to append / filter out type predicate hashes in identities. check-in: d40e6470bf user: zlodo tags: trunk | |
|
2021-10-25
| ||
| 19:34 | Type predicates: store the expressions as an array of values, which avoids unecessary conversions and results in the inclusion of the CIR from the expressions in the hash check-in: 996d8d9686 user: zlodo tags: trunk | |
|
2021-10-24
| ||
| 20:22 | Implemented CIR instruction hashing check-in: f5cd8d2642 user: zlodo tags: trunk | |
|
2021-10-23
| ||
| 19:40 | Small code cleanup, moved some code to .cpp that didn't need to be in the header check-in: ef3548db6c user: zlodo tags: trunk | |
| 16:34 | Implemented hashing of EIR terms check-in: ec41139b5a user: zlodo tags: trunk | |
|
2021-10-09
| ||
| 22:07 | Prelude: use the Conjunction instruction to build the reference predicate equivalence check check-in: 233221b915 user: zlodo tags: trunk | |
| 21:50 | Added the Conjunction CIR instruction to build a conjunction from predicates at verification time check-in: e3485faf08 user: zlodo tags: trunk | |
| 20:12 | Predicates: add the possibility to store named sets of predicates in types, to be retrieved from a dictionary at verification time check-in: 459f60ca3a user: zlodo tags: trunk | |
| 15:52 |
| |
|
2021-10-08
| ||
| 17:06 | Linux build fix check-in: e386f21089 user: zlodo tags: trunk | |
|
2021-10-07
| ||
| 22:37 | Added tests for mutref predicates equivalence checking check-in: 50c3984309 user: zlodo tags: trunk | |
|
2021-10-06
| ||
| 21:50 | Mut ref predicates verification: display a useful error message check-in: 05ada78145 user: zlodo tags: trunk | |
| 14:13 | Diagnostics: when registering a custom diagnostic message, save the context stack along with it check-in: 18734ccbef user: zlodo tags: trunk | |
|
2021-10-04
| ||
| 16:13 | Fixed build issues with Tracy on mac and updated it to the last version check-in: f408a2e123 user: zlodo tags: trunk | |
| 12:06 | Cleanup check-in: b974d30199 user: zlodo tags: trunk | |
| 11:57 |
| |
|
2021-10-01
| ||
| 19:20 |
| |
|
2021-09-30
| ||
| 23:37 | Fixed a couple of bugs, but the linux version is broken for now (due to language bugs that can't be worked around and need to be fixed) check-in: 24415e41e4 user: zlodo tags: trunk | |
| 22:07 | Correctly generate and link executables on darwin check-in: 5f6197d1a0 user: zlodo tags: trunk | |
| 19:14 | Added a builtin g0 variable that exposes the name of the target OS, just to be able to quickly hack around some rudimentary mac support check-in: ec5428614c user: zlodo tags: trunk | |
|
2021-09-29
| ||
| 22:59 | Fixes for wsl build check-in: 886e9f72c4 user: zlodo tags: trunk | |
| 22:07 |
| |
|
2021-09-28
| ||
| 17:59 | Fix functions and template functions not getting compiled with visibility over their original enclosing scope, but over the current scope at the point of invocation instead check-in: 39c8a653da user: achavasse tags: trunk | |
|
2021-09-26
| ||
| 23:25 | Fixed template bugs with parametric types check-in: 097569fdd6 user: achavasse tags: trunk | |
| 21:11 | TDecl: instead of directly storing the type signature (and forgetting all about the nested TExprs), we store the TExpr and generate the signature during typechecking check-in: 00408e8723 user: achavasse tags: trunk | |
| 19:47 |
| |
| 17:00 | g0 api: added a function to retrieve the CFG from a code builder check-in: e1194caa9e user: achavasse tags: trunk | |
| 16:16 | g0 api: removed the old codegen module wrapper, use TypeWrapper instead check-in: ded246dccd user: achavasse tags: trunk | |
| 14:17 | Intrinsics: expose the current code builder as an implicit parameter check-in: 60a2f901d5 user: achavasse tags: trunk | |
| 13:03 | Integrated mimalloc check-in: 8398bd36c2 user: achavasse tags: trunk | |
| 12:00 |
| |
|
2021-09-25
| ||
| 15:53 | eir: implemented OrPattern term check-in: 6b3eee40c4 user: achavasse tags: trunk | |
|
2021-09-24
| ||
| 19:11 | Overload resolution: cache which overload was selected for a given argument tuple check-in: 7bb051b826 user: achavasse tags: trunk | |
|
2021-09-23
| ||
| 21:42 | Got rid of trie versus trie matching, again. The clown show goes on check-in: ad0b20f57d user: achavasse tags: trunk | |
|
2021-09-22
| ||
| 20:25 | Removed the gross use of std::any from the type checking trie, also fixed some horribly wrong type error that got hidden by the std::any and happened to miraculously work anyway check-in: fabfc6df97 user: achavasse tags: trunk | |
|
2021-09-21
| ||
| 22:43 | Resurrected and updated trie versus trie matching that was removed [e9ee5d4728e2b2807b761d67820df11dcfbcdbaea2742828ac9ec8f8d3372e3e|a long time ago] to attempt an overload resolution optimization check-in: 626dafb38e user: achavasse tags: trunk | |
| 18:48 | eir: remove the function to match a single eir against another eir, which was never actually used check-in: dbf5bbf612 user: achavasse tags: trunk | |
|
2021-09-20
| ||
| 23:23 | Integrated the Tracy profiling client and added some profiling instrumentation check-in: b846dfa2fb user: achavasse tags: trunk | |
|
2021-09-19
| ||
| 23:35 | Fixed various bugs encountered while trying to override an extension point in the prelude check-in: 89c0616e71 user: achavasse tags: trunk | |
| 20:18 | Implemented "Implies" and "PHOverride" verification-specific CIR instructions check-in: 56ae4179a9 user: achavasse tags: trunk | |
| 19:30 | g0 api: ReferenceType and retrieving type predicates check-in: 78e91a4545 user: achavasse tags: trunk | |
| 16:06 | Began implementing the prelude, which now sets up the g1 namespace, hiding all the internal builtins and APIs from user code. check-in: 15fd7eba11 user: achavasse tags: trunk | |
| 14:42 | g0 api: #CompileFileToFunction takes the identity to use as root as parameter check-in: dd5e98c20d user: achavasse tags: trunk | |
| 14:23 | g0 api: Env check-in: 0da72aac62 user: achavasse tags: trunk | |
| 13:59 | g0 api: diagnostics check-in: 5ccfe91819 user: achavasse tags: trunk | |
| 11:20 | g0 api: CIR: CFG check-in: bdfee6615a user: achavasse tags: trunk | |
| 10:30 | g0 api: CIR: BasicBlock check-in: b96622b654 user: achavasse tags: trunk | |
|
2021-09-18
| ||
| 18:43 | g0 api: more work on the CIR api check-in: 447824df93 user: achavasse tags: trunk | |
| 17:00 |
| |
|
2021-09-17
| ||
| 23:04 | g0api, builtins: got rid of TermWrapper and ValueWrapper, use specializations of TypeWrapper instead to allow for more generic code check-in: 4a571387ed user: achavasse tags: trunk | |
| 20:43 | g0 api: more work on the CIR api check-in: a7c05af907 user: achavasse tags: trunk | |
| 19:15 |
g0 api:
| |
|
2021-09-16
| ||
| 21:31 | g0 api: started implementing the CIR api check-in: 8dd49b0d89 user: achavasse tags: trunk | |
| 21:01 | g0 api: implemented Value api check-in: 5c68efeb07 user: achavasse tags: trunk | |
| 20:05 | g0 api: the EIR Terms are now completely covered check-in: 78da84d2af user: achavasse tags: trunk | |
| 19:00 | More work on the g0 EIR api check-in: 967d3ba3d7 user: achavasse tags: trunk | |
|
2021-09-15
| ||
| 22:15 | Fixed the generic CTType and RTType patterns, and removed the super generic assignment operator overload that would accept literally any type check-in: ea7c04df2f user: achavasse tags: trunk | |
| 21:24 |
| |
| 01:02 | More work on the extensibility api check-in: 29872be1f2 user: achavasse tags: trunk | |
| 00:11 | Added a test for, and fixed tctrie variable length vector type checking check-in: c1b565fdda user: achavasse tags: trunk | |
|
2021-09-13
| ||
| 21:52 |
| |
|
2021-09-12
| ||
| 23:52 | Repo: syntax color theme change check-in: b4fe430e44 user: achavasse tags: trunk | |
| 23:20 | Repo: more syntax highlighting workarounds check-in: 6c481d18a4 user: achavasse tags: trunk | |
| 23:18 | Repo: syntax highlighting issue workaround check-in: 4b28030b9a user: achavasse tags: trunk | |
| 23:09 | Updated repo's syntax highlighting check-in: 951c8fed08 user: achavasse tags: trunk | |
| 21:38 |
| |
| 16:48 |
| |