Goose  History of bs/verify/call.cpp of 238df77134c7da91

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

History of file bs/verify/call.cpp at check-in 238df77134c7da91

2024-09-15
20:24
Add clang format settings, reformat everything file: [a001b6bb59] check-in: [0db147f117] user: achavasse branch: cir-ssa-refactor, size: 4437
2024-02-09
18:05
Lowering: completely reworked all lowering to happen in the same two unified extension points upstream of all three CIR consumers file: [d67460f5e6] check-in: [1793989d05] user: zlodo branch: trunk, size: 4322
2024-01-02
22:41
Structs: build the default ctor and add it as an overload of _Initialize. file: [d03cd73cd1] check-in: [ad919df201] user: zlodo branch: trunk, size: 4232
2023-08-27
22:30
  • Added "CallCheck" CIR instruction to request the verifier to check a bunch of func params like it was a real call
  • Used the above to verify the arguments passed to ghost funcs
 file: [b807ad38ff] check-in: [83971c96a4] user: zlodo branch: trunk, size: 4233
2023-01-05
19:44
Fixed passing tuple by value to functions, which involved properly handling type checking of constant tuples containing computed data and some codegen bugs file: [13d2ddea54] check-in: [9b8306c3af] user: zlodo branch: trunk, size: 3696
2022-11-11
20:01
  • Implemented template tuples and vararg tuples
  • Fixed a few issues with the verifier
 file: [e5d196205a] check-in: [08ffdaf6db] user: zlodo branch: trunk, size: 3702
2022-06-29
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++
 file: [d524da943d] check-in: [9814f18b04] user: zlodo branch: cir-stack-language, size: 4018
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
 file: [57a883805c] check-in: [b81d4242e3] user: zlodo branch: cir-stack-language, size: 3992
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
 file: [0262dc29de] check-in: [b4d5bdf6ec] user: zlodo branch: cir-stack-language, size: 3638
2022-06-11
12:29
Verification now mostly works again, tests not re-enabled yet file: [51739ba84d] check-in: [17301ed8fc] user: zlodo branch: cir-stack-language, size: 3624
2022-06-08
22:38
Refactored the verifier to use the stack-based CIR. It compiles but isn't re-enabled yet file: [7d37ffb787] check-in: [4f05876cc2] user: zlodo branch: cir-stack-language, size: 3477
2022-01-07
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
 file: [c7647710bb] check-in: [43f03d4856] user: zlodo branch: trunk, size: 3433
2021-11-28
13:34
Verification: fixed incorrect handling of type predicates in function parameters file: [4e6dec6a3e] check-in: [c066339928] user: zlodo branch: trunk, size: 3583
2021-11-22
20:22
Function pre-conditions and post-conditions now use the same proposition lists as type predicates file: [340aa76713] check-in: [1c335aeb04] user: zlodo branch: trunk, size: 3342
2021-10-31
18:52
  • Reverted most of the horribly complicated changes done since [b3ff9af3c2fe4925], other than the ability to hash all terms, values, instructions and predicates
  • Solved the problem for which tests were added in [b3ff9af3c2fe4925] in a much simpler way
 file: [a08836c3dc] check-in: [1fe5a1ac2b] user: zlodo branch: trunk, size: 3324
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 file: [3d70124287] check-in: [996d8d9686] user: zlodo branch: trunk, size: 3342
2021-10-09
20:12
Predicates: add the possibility to store named sets of predicates in types, to be retrieved from a dictionary at verification time file: [8fa0d4f058] check-in: [459f60ca3a] user: zlodo branch: trunk, size: 3490
15:52
  • Fixed a couple of verification bugs and added related tests
  • Added some tests for currently broken verification scenarios involving template functions
 file: [58245c62ec] check-in: [b3ff9af3c2] user: zlodo branch: trunk, size: 3472
2021-09-12
16:48
  • Started work on extensibility api
  • some code cleanup
 file: [67a349e5b8] check-in: [55beba911a] user: achavasse branch: trunk, size: 3518
2021-01-02
18:24
Yet one more reference/address refactor: each calculation step (getting temp addr, getting var addr, selecting a member) is now a separate cir instruction. We need this level of generalization to be able to obtain addresses from anywhere, including variables and function parameters. file: [9ec9bf90e3] check-in: [26c691ecb9] user: achavasse branch: trunk, size: 3524
18:00
Some more renaming. file: [094afc210f] check-in: [0345b9f807] user: achavasse branch: trunk, size: 3548
2020-12-27
14:40
Renamed "ir" to "eir" (expression intermediate representation) and "llr" to "cir" (code intermediate representation) for clarity. file: [7827f5e7ad] check-in: [7d2def7b75] user: achavasse branch: trunk, size: 3557
2020-12-18
01:29
References refactor: references are now values all the way to the llr, where a new "CalcAddress" instruction represents a conversion from a logical address (location + path) into an actual runtime or compilation time address. This is in preparation to allow references to be stored in variables or passed as parameters. (It just took 4.5 months to finish this... Refactoring just sucks) file: [7c621d120c] check-in: [8ddd71f9b2] user: achavasse branch: trunk, size: 3557
2020-06-20
14:32
  • Got rid of the gross system of performing unifications twice in all cases. It's only really needed when invoking template functions.
  • Since the above had the unexpected side effect of fixing the tuple Initialize() overloads not being called, fixed those (which were actually broken).
 file: [ace936b55b] check-in: [c3f897359f] user: achavasse branch: trunk, size: 3560
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.
 file: [b78ea33802] check-in: [b00c682e34] user: achavasse branch: trunk, size: 3570
2020-06-01
01:06
Verifier: refactored type handling and extended it to handle tuple types. file: [0d3b1e73d2] check-in: [6f98718d3b] user: achavasse branch: trunk, size: 3575
2020-04-15
06:36
Removed llr::GetVar, now using the more generic llr::Load instead. file: [89e670bdbd] check-in: [20c242dc4f] user: achavasse branch: trunk, size: 3549
2020-02-02
21:47
Refinement types: implemented tests and fixed some issues. file: [f0ede1ceae] check-in: [972099a359] user: achavasse branch: trunk, size: 3532
2020-02-01
22:54
Refinement types: when calling a function, assert the param's predicates and assume the return type's predicates. file: [216cef3fd0] check-in: [d828564e66] user: achavasse branch: trunk, size: 3552
2020-01-04
18:27
Verification: changed the syntax for the current function's return value to the more explicit "@result". file: [d876d0a006] check-in: [cbbd282cfa] user: achavasse branch: trunk, size: 2268
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.
 file: [9920a93832] check-in: [18af6c1847] user: achavasse branch: trunk, size: 2262
2019-11-19
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. file: [17c5fefbc2] check-in: [238df77134] user: achavasse branch: trunk, size: 2265
2019-11-18
01:40
Verifier: first seemingly working version of the k-induction loop checker. file: [a8013dbf65] check-in: [477ef5b3d4] user: achavasse branch: trunk, size: 2294
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. file: [3508fcc2e3] check-in: [e33c4ea6c1] user: achavasse branch: trunk, size: 2293
2019-10-30
22:08
Verifier: more work on loop verification. file: [399c2f58ce] check-in: [c91249ffc7] user: achavasse branch: trunk, size: 2303
2019-10-20
14:13
Verifier: more work on loop unrolling. file: [4bc2c3ee4d] check-in: [8082ea7f42] user: achavasse branch: trunk, size: 2303
2019-10-09
19:21
Renamed and modified bs/analyze/call.cpp → bs/verify/call.cpp. Some renaming for consistency and to match commonly used names for those things. file: [ba68c2e417] check-in: [5e72e8e08c] user: achavasse branch: trunk, size: 2289
2019-10-08
21:55
Added:
  • 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.
 file: [b077ac933a] check-in: [09e8221436] user: achavasse branch: trunk, size: 2289
Fossil 2.26 [1205ec86cb] 2025-04-30 16:57:32
This page was generated in about 0.049s