Goose  Timeline

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

49 check-ins that include changes to files matching 'tests/noprelude/diagnostics/*'

2021-03-01
12:32
Reorganized tests, they are now grouped by language feature. check-in: 5e757567a6 user: achavasse tags: trunk
2020-07-05
20:15
Implemented reference parsing. check-in: 086a58a7a3 user: achavasse tags: trunk
2020-07-04
13:08
  • Verifier: fixed havocing of individual members of aggregate types not working.
  • Added verification loop tests (both passing and failing) that modify a tuple inside of the loop.
check-in: e3b9bd4c1b user: achavasse tags: trunk
2020-07-03
23:03
  • Fixed reference typechecking issues.
  • Fixed tuple initialization.
  • Added verification tests involving values stored in tuples.
check-in: 4be05b9f94 user: achavasse tags: trunk
2020-06-26
23:34
Cleanup:
  • Removed the poorly thought out "domain" system that was intended to allow for different implementations of functions for runtime and for compilation time, which was adding an absurd amount of crap everywhere and should be unnecessary with the current planned approach for implementing data structures.
  • The using statement doesn't do lazy parsing anymore. Lazy parsing is better left to specific constructs that require them (such as function bodies and later on class/structs). This removes the only case of significant newline character in the language.
check-in: 568c366a36 user: achavasse tags: trunk
2020-06-20
19:59
Verifier: some fixes to correctly handle tuples. Still not quite working yet. check-in: 060e84f233 user: achavasse tags: trunk
2020-06-15
19:45
Call "Postprocess" on unification solutions during the best solution lookup, so that custom postprocessing callbacks can trigger the rejection of a solution. check-in: daee557086 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-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-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
2020-02-02
21:47
Refinement types: implemented tests and fixed some issues. check-in: 972099a359 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-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-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
2019-11-18
01:40
Verifier: first seemingly working version of the k-induction loop checker. check-in: 477ef5b3d4 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-04
19:53
Verifier: more work on loop verification. check-in: b4385d9930 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-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
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
13:58
Implemented the conversion of GetVar/SetVar/GetTemporary/SetTemporary to z3 expressions. check-in: 3ae3c0b3ad user: achavasse tags: trunk
2019-09-26
23:37
Refactored the parsing of verification statements so that it works properly in all cases (regular functions, template functions, function type expressions, lambdas). check-in: 4fe418f4d0 user: achavasse tags: trunk
00:27
Static analysis: check that function verification statements are satisfiable and emit relevant error messages if they aren't. check-in: 7f14d60722 user: achavasse tags: trunk
2019-09-22
14:37
Project renaming. check-in: af650a9e95 user: achavasse tags: trunk
2019-08-25
01:54
  • Got rid of the LoadConstInt instruction and directly handle integer constants in codegen. The old system didn't work for compile-time evaluated runtime integers.
  • Added missing implementations for unsigned comparison, that were somehow forgotten.
  • Implemented the nullptr constant.
  • Made a test version of the mandelbrot sample that gets both compiled and interpreted and whose results are compared with the same reference file, as a sanity test that interpreted and compiled code behave identically.
check-in: 9a68159d52 user: achavasse tags: trunk
2019-08-24
19:33
More cleanup around which builtin functions should be intrinsics/eager/non eager. check-in: fece958df9 user: achavasse tags: trunk
16:54
  • ExecuteFile is now a regular builtin function.
  • Added #Include, which works the same as the old ExecuteFile.
  • Added a CreateConstant() builtin func.
  • Used the above to cleanup the command line parsing code in empathy.em.
check-in: f1cab5f761 user: achavasse tags: trunk
2019-08-23
20:18
  • Added a default InitializeVar() overload allowing any builtin type to be stored in a local variable during compile time.
  • Remplaced a lot of hackish uses of using with local variables, now that they work.
  • Changed several eager-evaluated bultin function to normal builtin functions, thanks to the above cleanup.
  • Eager-evaluated builtin functions are all now prefixed with a # symbol to indicate their "compiler directive" nature and make it clearer that they are evaluated during the translation phase of the program, rather than its execution (even compile time execution).
  • A few build and testing scripts fixes.
check-in: 133303cbbf user: achavasse tags: trunk
2019-08-22
13:23
You have failed me for the last time, CMake. check-in: e38aee1ca0 user: achavasse tags: trunk
2019-08-21
13:38
  • Automatically compile the samples during the build.
  • Added a --forcecolors to the front-end, since it can't detect whether colors are allowed when launched by Ninja.
  • while: if the condition evaluates to constant true and there is no break statement in the body, use a different code generation strategy to avoid generating a continuation block which makes a return statement mandatory after the loop even though it's unreachable.
check-in: 20d317a921 user: achavasse tags: trunk
2019-08-20
23:48
Removed an irrelevant comment. check-in: d2c3ec7961 user: achavasse tags: trunk
23:42
  • Fixed broken canBeExecuted() and canBeEagerlyEvaluated() computation of CFGs.
  • Added some error messages when a function with compile-time only types contains calls to runtime functions. (to be improved and detected during parsing rather than codegen but serviceable for now)
check-in: d5bc4daeca user: achavasse tags: trunk
20:00
Improved error messages. check-in: 25f4d2946d user: achavasse tags: trunk
16:15
  • Fixed error messages when compiling a file through the real frontend (this was broken again because this is a day ending in y)
  • Implemented initialization, assigment, and equality comparison for ct_char.
  • Implemented the cast builtin function. Its only overload currently allows to cast a ct_char into a ct_int.
  • Implemented the PrintAsciiChar builtin function to write a single ascii character.
check-in: c20ed5f1d3 user: achavasse tags: trunk
2019-08-19
19:25
  • Factored escape sequence parsing out and made hex and octal literal also output correct UTF-8 sequences when used in strings.
  • Fixed lexer errors never being displayed if they happen during the compile-time execution attempt, during which diagnostics are silenced.
check-in: 6c118e666d user: achavasse tags: trunk
2019-08-18
00:54
  • Implemented the while statement.
  • Fixed a lexer issue that generated invalid locations at the very end of files.
check-in: 459ee84d6b user: achavasse tags: trunk
2019-08-17
14:49
  • Intrinsics automatically set their domain depending on the domain restrictions of the builtin types that they use.
  • Declaring a local variable of a compile-time only type is now properly rejected during codegen.
  • Improved error messages for operators and extension point invocations.
check-in: 48a020a1fa user: achavasse tags: trunk
2019-08-15
22:37
  • Fixed some bugs related to dropping values.
  • Implemented local variable declarations with default initialization.
  • codegen: Fixed allocas not properly grouped up at the start of the first basic block of functions.
check-in: 3d8b581261 user: achavasse tags: trunk
2019-08-14
02:35
Fixed a misnamed test. check-in: 5a4946c300 user: achavasse tags: trunk
02:30
  • Added an unification rule to deal with LocationIds. It honors poisoning and preserve the most recent location from the input values.
  • Added a diagnostic context indicating the point at which a template function passed as a value has been instantiated.
  • Added a trace mode that logs the diagnostics contexts, which can be activated by calling a compile time function.
  • Added a few diagnostic messages tests.
check-in: 980effe072 user: achavasse tags: trunk