Goose  Timeline

Advanced

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

50 check-ins occurring around 2019-11-19 00:04:49.

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
Fossil 2.26 [1205ec86cb] 2025-04-30 16:57:32
This page was generated in about 0.015s