Goose  Timeline

Advanced

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

113 check-ins using file tests/noprelude/diagnostics/template-instantiation-context.txt version b6ae13923f

2020-06-15
19:16
Moved some common code into a helper function to facilitate some future refactoring. check-in: df0ad9a7f1 user: achavasse tags: trunk
2020-06-13
22:59
  • Implemented Initialize overloads for tuples.
  • Lots of cleanup.
 check-in: 947b9d7cfc user: achavasse tags: trunk
13:34
Implemented new rules for implicit dereferencing and implicit referencing. check-in: 4d5cc07d86 user: achavasse tags: trunk
13:15
Rewrote the reference unification rules. check-in: ba97c17dee user: achavasse tags: trunk
13:05
Fixed eager evaluation not failing gracefully in some cases. check-in: c70d722331 user: achavasse tags: trunk
12:51
Modify the reference IR representation so that we can have holes for the behavior. check-in: 385846b609 user: achavasse tags: trunk
2020-06-05
18:57
Verifier: loops: instead of tracking and havocing modified variables during loops, track modified addresses, so that modifying only some fields of a tuple will not result in forgetting everything about the other fields. check-in: 54ef60956e user: achavasse tags: trunk
00:42
Cleanup. check-in: ea28d09f80 user: achavasse tags: trunk
00:35
Verifier: handle "StoreToAddress" for addresses that point to tuple members. check-in: 077c944c02 user: achavasse tags: trunk
2020-06-03
23:08
  • Verifier: a bunch of refactoring to better keep track of the types of the z3 expressions stored in variables.
  • Verifier: handle "LoadFromAddress" for addresses that point to tuple members.
 check-in: b00c682e34 user: achavasse tags: trunk
2020-06-01
18:39
Verifier: go through the LowerConstantForVerification extension point when building a constant expression. check-in: 98739f02b6 user: achavasse tags: trunk
01:21
Cleanup. check-in: c793734a0a user: achavasse tags: trunk
01:06
Verifier: refactored type handling and extended it to handle tuple types. check-in: 6f98718d3b user: achavasse tags: trunk
2020-05-30
14:25
Enable's z3 new arith solver as the old one takes a very long time in one of the tests with the latest version of z3. check-in: 4b56796791 user: achavasse tags: trunk
2020-05-25
22:08
  • Added a "LowerConstantForRuntime" extension point, similar to LowerTypeForRunTime.
  • Added a way to represent Record constants.
  • Implemented LowerConstantForRunTime for tuples, which lowers them into a constant record.
  • Implemented codegen for constant records.
  • Implemented codegen for storing an aggregate constant.
  • Implemented a way (not exposed in the syntax for now) to create vararg function types, to be able to call vararg external functions such as printf.
  • Enabled the tuple runtime/compilation combined test which is now working.
  • Various bug fixes.
 check-in: bb17e9f3dd user: achavasse tags: trunk
2020-05-23
12:58
  • Fixed the hole matching score which prevented some unification rules to be selected.
  • Implemented LowerTypeForRuntime for tuples.
  • Implemented an unification rule for constant tuples.
  • Added some debugging helpers.
 check-in: c39a302502 user: achavasse tags: trunk
2020-05-21
17:26
Created a new term type to represent holes in IR expressions. The old system of representing holes using a vector of two values led to ambiguousness when creating some rule patterns: a tuple whose both type vector and payload vector were holes would be indistinguishable from a tuple containing two elements. check-in: 51c6751b6d user: achavasse tags: trunk
2020-05-19
17:07
Added an unification rule for computed tuples which creates constant references for each members and unifies them. check-in: 2ecfa85c23 user: achavasse tags: trunk
15:03
The TemporaryAddress address calculation mode now carries around the initializer value, in case the temporary doesn't already exist. This allows a reference to a temporary to be completely self contained in its value, rather than requiring a separate setup instruction to be emited in the cfg. check-in: 934090c5a8 user: achavasse tags: trunk
2020-05-18
12:39
  • Renamed the LowerType extension point to LowerTypeForRuntime as we'll need a similar "LowerTypeForVerification" later on.
  • The function type case of LowerTypeForRuntime is no longer hardcoded in the c++ utility function of the same name but implemented as an overload of the extension point.
 check-in: 8818ea1872 user: achavasse tags: trunk
2020-05-17
17:30
  • Clean up the "default return value from top level file functions" stuff.
  • Standardize to a default return value of 0 for the top level file both in execution mode and in compilation mode.
  • Implemented a combined execution/compilation test for tuples in preparation for implementing tuple compilation. (not enabled yet)
 check-in: 397f594186 user: achavasse tags: trunk
2020-05-16
19:32
Repo: fix syntax highlighting with the latest trunk verison of fossil. check-in: 807a4f208b user: achavasse tags: trunk
19:21
Minor cleanups. check-in: 6099081bdd user: achavasse tags: trunk
18:39
Now that we can assign mutable references, it is possible to assign to a tuple member. Added a test for that. check-in: 27a74436f3 user: achavasse tags: trunk
18:32
The builtin assignment operator overloads now return the reference to support chained assignments. check-in: ba2a02025d user: achavasse tags: trunk
2020-05-14
22:24
The compound assignment operators now take a mutable reference as the lhs. check-in: e4cd7e104e user: achavasse tags: trunk
2020-05-13
18:15
References:
  • When doing variable declaration local type inference, look for an initialization function that takes a mutable reference on the lhs, instead of a local variable.
  • As a result of the above, got rid of Initialize() overloads for local variables.
  • The assignment operator now takes a mutable reference on the lhs, instead of directly working on a local variable.
 check-in: ebdba2e941 user: achavasse tags: trunk
2020-05-04
18:43
Refactored the Initialize() extension point to take a mutable reference instead of directly taking a locvar. check-in: 10df99e08a user: achavasse tags: trunk
2020-05-03
15:32
Simplified the llr address representation. check-in: 0b4eb97a44 user: achavasse tags: trunk
2020-04-22
23:27
Removed llr::SetVar, now using the more generic llr::Store instead. check-in: 036092faf1 user: achavasse tags: trunk
2020-04-15
06:36
Removed llr::GetVar, now using the more generic llr::Load instead. check-in: 20c242dc4f user: achavasse tags: trunk
2020-04-11
23:33
Updated to the latest git version of llvm. check-in: d38aab5fc2 user: achavasse tags: trunk
21:01
  • Implemented load, store and pointers in execute and codegen.
  • Implemented load and pointers in verify.
  • When unifying a local variable against a parameter, generate a reference.
 check-in: e814ad7e23 user: achavasse tags: trunk
2020-03-11
22:11
Reference: implemented a pattern provider for mutable references. check-in: 58491e544e user: achavasse tags: trunk
2020-03-07
16:36
More work and fixes on references. Reading a tuple member using the . operator (which returns a constant reference) is now working. check-in: 1c33db7499 user: achavasse tags: trunk
2020-02-29
15:07
Implemented unification for references. check-in: 4940c5c904 user: achavasse tags: trunk
2020-02-27
22:15
Implemented the dot operator for tuples. check-in: 2f953408d9 user: achavasse tags: trunk
2020-02-26
22:48
builtins: added the reference type. check-in: b4dfb8c928 user: achavasse tags: trunk
2020-02-23
23:57
llr: added the load and store instructions. check-in: f34a90f312 user: achavasse tags: trunk
2020-02-22
21:22
llr: added the GEP instruction. check-in: 1f1bc22ffc user: achavasse tags: trunk
2020-02-20
22:44
Minor code formatting cleanup. check-in: 0af3d1c728 user: achavasse tags: trunk
22:42
  • Wrap function parameters into local variables, which will make it easier later on to distinguish temporaries from stack values when implementing references.
  • Register parameters for destruction, which was missing.
  • Added an invocation rule for local variables, so that they can be invoked if they contain an invokable object.
 check-in: 652107629a user: achavasse tags: trunk
2020-02-17
23:15
Register temporary values returned from function calls for destruction, so that DestroyValue() is invoked on them. check-in: a0ee0dfc2e user: achavasse tags: trunk
2020-02-15
15:13
Started to implement a virtual memory sub system for compilation time execution. check-in: f18062b8da user: achavasse tags: trunk
2020-02-09
19:23
Small cosmetic error messages fixes. check-in: edf6a9d2ed user: achavasse tags: trunk
19:02
Builtin operators:
  • Verification time assertion failure errors for builtin division, module and shift operators are anchored to a valid source code location.
  • Added custom error messages for the above.
  • Added tests for the above.
 check-in: c4a6d4d66b user: achavasse tags: trunk
16:55
  • The builtin integer division and modulo operators now require a compile-time proof that the divider is not zero.
  • The builtin integer left shit and right shift operators now require a compile-time proof that the rhs value is less than the bitsize of lhs.
 check-in: 8c4fcc68b0 user: achavasse tags: trunk
2020-02-04
21:42
Builtins: implemented helpers to construct complex computed values using expression templates. check-in: 6ed2bd7a75 user: achavasse tags: trunk
20:20
Unfuck some documentation. check-in: 87f7150020 user: achavasse tags: trunk
2020-02-02
23:13
Docs: small layout improvement. check-in: 0521bfdcdf user: achavasse tags: trunk
23:10
Some documentation cleanup and update. check-in: c9186b7b9f user: achavasse tags: trunk
21:47
Refinement types: implemented tests and fixed some issues. check-in: 972099a359 user: achavasse tags: trunk
2020-02-01
23:28
Refinement types:
  • Assert type predicates after a variable assignment
  • Check type predicates when checking a compile-time function call
 check-in: 216ff2d9c8 user: achavasse tags: trunk
22:54
Refinement types: when calling a function, assert the param's predicates and assume the return type's predicates. check-in: d828564e66 user: achavasse tags: trunk
22:32
Refinement types: assert the return type predicates when returning from a function. check-in: 7259273cf9 user: achavasse tags: trunk
2020-01-28
21:52
Refinement types: assume parameter types predicates at the beginning of functions. check-in: 7f16edb82a user: achavasse tags: trunk
2020-01-27
00:24
Refinement types: parse predicates lazily to play well with templates. check-in: e57c63fea5 user: achavasse tags: trunk
2020-01-23
22:24
Refinement types: implemented the where operator to add predicates to a type. check-in: 9586391cdb user: achavasse tags: trunk
2020-01-22
22:14
Standardized the way type values are encoded to make room for an optional pointer to a list of predicates for refinement types. check-in: cc380f4f8f user: achavasse tags: trunk
2020-01-16
21:41
ir: also make void* always compare to true to make it easier to work with llvm type pointers embedded inside type IR expressions. check-in: 6680e30102 user: achavasse tags: trunk
20:46
ir: comparing ptr< void > is considered always true, to allow to more easily attach opaque data onto ir expressions without changing their semantics. check-in: 1a704c5a51 user: achavasse tags: trunk
2020-01-13
23:13
Renamed the runtime struct type to "record" to avoid future confusion since it's a much lower level type (essentially just a tuple restricted to runtime types) than the future "struct" type. check-in: b573d100cf user: achavasse tags: trunk
2020-01-12
21:10
builtins: added wrapper types to allow terms and values to be manipulated at low level within the language itself. check-in: ceb0b190d6 user: achavasse tags: trunk
20:03
builtins: added a wrapper for a CodeBuilder pointer. check-in: d4e5c46e57 user: achavasse tags: trunk
2020-01-11
18:28
  • Moved the cfg and lifetime management stuff into a CodeBuilder object owned by sema::Context. This is in preparation to allow alternative implementations of the builder, for instance to build classes.
  • Pass the context to intrinsic functions, which removes their dependency to the parser the need for the ugly "GetCurrentParser" static function.
 check-in: b3aeaae2df user: achavasse tags: trunk
2020-01-05
21:46
Fix (inconsequential) missing else. check-in: 9ad87f2dcf user: achavasse tags: trunk
20:22
  • Split extpoints.cpp into several files.
  • Fixed a tuple related bug that caused compilation failures when adding parentheses around expressions in some cases.
 check-in: 5967fcaf06 user: achavasse tags: trunk
17:41
Simplified the implementation of the comma operator. check-in: a25bb3bc5f user: achavasse tags: trunk
2020-01-04
23:44
  • Fixed crash when an undefined symbol is encountered in a verification condition.
  • Fixed crash when a non-boolean expression is encountered in a verification condition.
 check-in: f6e12ac41e user: achavasse tags: trunk
18:27
Verification: changed the syntax for the current function's return value to the more explicit "@result". check-in: cbbd282cfa user: achavasse tags: trunk
17:28
Loop verifier: when still finding counter-examples at max K unrolls, emit error messages for the failed conditions instead of a generic "couldn't verify loop" message. check-in: 23d2aa4c8a user: achavasse tags: trunk
15:48
Verifier: tweak the wording of the unsatisfiability error for consistency, also sort those by location ids to have a deterministic output. check-in: 264e55dac8 user: achavasse tags: trunk
15:17
  • verifier: check compilation-time function calls.
  • verifier: improved error messages wording.
 check-in: 353fcc252a user: achavasse tags: trunk
2019-12-14
21:24
Verifier: fixed multiple issues with nested loop verification. check-in: 693415ce16 user: achavasse tags: trunk
2019-12-11
15:38
  • Compile-time execution: don't attempt to perform a compile time evaluation of every invocation. Instead, wait until a type is being used by a decl to try and evaluate it.
  • Diagnostics: simplify accordingly (no need for the mode that silences all errors during attempted comptime evaluation)
  • Added some verification conditions to the mandelbrot sample, and created a broken variant as a verification diagnostics test.
 check-in: b702561850 user: achavasse tags: trunk
2019-12-05
17:40
Implemented a helper to check whether a type is compile-time only. check-in: 12f37d77cb user: achavasse tags: trunk
2019-12-03
20:34
  • Shift operators: the right hand side must be an unsigned int.
  • Verifier: added tests to check that bitwise operations are properly translated to z3.
 check-in: 74b73239c8 user: achavasse tags: trunk
2019-12-01
20:17
Verifier:
  • Fixed incorrect cfg walking order, which sometimes didn't properly process all the predecessors of a basic block first.
  • Preserve the unique id counter of the remapper when saving/restoring its state. Fixes breakage with nested loops.
  • Added tests for the logic or/and operators (which are really tests of the phi operator and of basic block processing order).
 check-in: f1e4ac80ba user: achavasse tags: trunk
2019-11-29
12:15
Verifier: handle phi instructions. check-in: b7dd8a4d25 user: achavasse tags: trunk
2019-11-28
17:53
Verifier: implemented most of the missing instructions (unsigned arithmetic and bitwise operations). check-in: 60e143d189 user: achavasse tags: trunk
2019-11-27
20:24
Verifier:
  • Unsigned ints are represented using z3 bitvecs.
  • The original type is carried around along with z3 exprs to be able to convert ints to bitvecs of the right size.
  • Insert int2bv conversions as necessary when encountering integer/bitvec mixed operations.
  • The logic and and logic or instructions are implemented on integers, which are converted to bitvecs.
 check-in: 18af6c1847 user: achavasse tags: trunk
2019-11-19
20:49
Store a location in loop headers, and use it to provide more context when diagnosing loop verification failures. check-in: 5f20eec65e user: achavasse tags: trunk
20:20
cfg: fix the way the variable ids modified by each loop are stored to avoid duplicate entries. check-in: 1c3ff200aa user: achavasse tags: trunk
00:04
cfg: now that we got rid of this crazy system where CFGs could "call" other CFGs that weren't really functions, removed that clumsy cfg index that was needed to identify temporaries everywhere. check-in: 238df77134 user: achavasse tags: trunk
2019-11-18
22:42
Removed the "inline CFG" llr instruction and related support code. check-in: 5329f83e33 user: achavasse tags: trunk
22:09
Refactor the logic and/or operator to directly append new basic blocks into the current CFG, rather than using a special llr instruction that embeds a nested CFG, whose implementation creates a lot of complexity everywhere. check-in: 70717f6b76 user: achavasse tags: trunk
01:40
Verifier: first seemingly working version of the k-induction loop checker. check-in: 477ef5b3d4 user: achavasse tags: trunk
2019-11-17
18:20
  • cfg: compute a list of every variable modified by each loop.
  • verifier: added a function to "havoc" a variable at the start of a given basic block.
 check-in: 02836c95bc user: achavasse tags: trunk
2019-11-16
16:27
  • while: remove code attempting to detect infinite loops, this will be best left to the verifier.
  • verifier: loop unrolling now works.
 check-in: f7c8245cb2 user: achavasse tags: trunk
2019-11-08
11:48
Verifier: check assertions with z3 immediately instead of postponing it until we have built the entire formula for the function. check-in: e33c4ea6c1 user: achavasse tags: trunk
2019-11-04
19:53
Verifier: more work on loop verification. check-in: b4385d9930 user: achavasse tags: trunk
2019-10-30
22:09
Removed an obsolete comment. check-in: 626057ff22 user: achavasse tags: trunk
22:08
Verifier: more work on loop verification. check-in: c91249ffc7 user: achavasse tags: trunk
2019-10-27
21:31
Verifier: split func.cpp into multiple files to make navigation easier. check-in: f606dd6e5d user: achavasse tags: trunk
2019-10-22
22:11
Verifier: traverse basic blocks in breadth first order and make sure that the current block's predecessors are processed first, so that we don't rely anymore on the order in which they are created by the statements. check-in: d7e2fcc24f user: achavasse tags: trunk
2019-10-20
14:13
Verifier: more work on loop unrolling. check-in: 8082ea7f42 user: achavasse tags: trunk
2019-10-18
11:33
Verifier:
  • Removed some hackish code to work around loops (not needed anymore now that loops edges are properly identified)
  • Added a placeholder class to track the state of loop unrolling and started plugging it into the existing code.
 check-in: b6662af2e1 user: achavasse tags: trunk
2019-10-16
23:08
llr: detect and store relevant informations about loops in the CFG to be able to unroll them in the verifier. check-in: b1f107d1e7 user: achavasse tags: trunk
2019-10-15
00:04
llr: implemented a helper function to compute dominators. check-in: cfc94e192c user: achavasse tags: trunk
2019-10-12
17:25
Verifier: use z3 push/pop to check assertions one at a time, so that we can find and report multiple errors in the same function. check-in: b414bc18df user: achavasse tags: trunk
2019-10-11
22:24
Docs: add anchors on sub section titles. check-in: 4f4a1dc4aa user: achavasse tags: trunk
2019-10-10
01:00
Docs: typo fix. check-in: d167a0b946 user: achavasse tags: trunk
00:38
Some docs fixes. check-in: e36fbebe18 user: achavasse tags: trunk
00:26
Wrote some docs. check-in: 8f046020b6 user: achavasse tags: trunk
2019-10-09
19:42
Added .editorconfig file. check-in: ed08ba02f2 user: achavasse tags: trunk
19:34
Some more renaming. check-in: f65c08a1c5 user: achavasse tags: trunk
19:21
Some renaming for consistency and to match commonly used names for those things. check-in: 5e72e8e08c user: achavasse tags: trunk
2019-10-08
21:55
  • Verifier: handle calls (assert the callee's preconditions and assume its postconditions)
  • Verifier: handle return value placeholder in the post conditions.
  • Verifier: fixes.
  • Verifier: context descriptions and locations can be attached to assertions.
  • Lexer: fix incorrect location length on integer literals.
  • Added some tests for successful and failed verification of functions pre-conditions and post-conditions.
 check-in: 09e8221436 user: achavasse tags: trunk
18:17
Expose "@" as a placeholder for the function's return value inside of ensures statements. check-in: 8541259c1c user: achavasse tags: trunk
18:02
Added the "placeholder" llr pseudo instruction. check-in: cc9ce06e64 user: achavasse tags: trunk
2019-10-07
22:04
Made the "assertion failure" error message lowercase to be consistent with other error messages. check-in: acbb4b30b8 user: achavasse tags: trunk
21:58
  • Fixed incorrect logic when generating z3 expressions to track the value of variables accross basic blocks.
  • Implemented basic error reporting for verification failure that highlights all the failed assertions.
  • Added a test program that demonstrates a simple case of failed static verification.
 check-in: 717a1ea6d4 user: achavasse tags: trunk
2019-10-05
16:37
  • Renamed the "assert" test helper function to "check".
  • Implemented a builtin "assert" intrinsic that emits an Assert instruction for the verifier.
  • Implemented a couple of tests to verify the generated z3 expressions for a couple of simple functions.
  • Fixed a few issues when building the z3 expressions.
 check-in: 3740e7a491 user: achavasse tags: trunk
Fossil 2.26 [1205ec86cb] 2025-04-30 16:57:32
This page was generated in about 0.02s