|
|
@2317
|
7 years |
boender |
- small changes to make things compile
|
|
|
@2316
|
7 years |
boender |
- committed temporary version: true version has to wait until I …
|
|
|
@2315
|
7 years |
campbell |
Add some more commentary.
|
|
|
@2314
|
7 years |
campbell |
Move generic definitions from recent commit to appropriate places.
|
|
|
@2313
|
7 years |
campbell |
RTLabs cost checker correct.
|
|
|
@2312
|
7 years |
garnier |
Memory injections, to be revised
|
|
|
@2311
|
7 years |
garnier |
Some more cleaning of switchRemoval …
|
|
|
@2310
|
7 years |
garnier |
Moved a lemma from switchRemoval to positive.
|
|
|
@2309
|
7 years |
garnier |
Removed the superfluous xorb definition and move some basic properties …
|
|
|
@2308
|
7 years |
campbell |
More proof (and corrections) on cost checking.
|
|
|
@2307
|
7 years |
campbell |
Half the proofs for sound cost labelling check.
|
|
|
@2306
|
7 years |
campbell |
An insertion sort for testing purposes.
|
|
|
@2305
|
7 years |
campbell |
RTLabs cost spec checking function implemented (lacks proof, or much …
|
|
|
@2304
|
7 years |
garnier |
Strengthened proof of associativity of bitvector addition. Some more …
|
|
|
@2303
|
7 years |
campbell |
Some preliminary checking of cost labelling properties in RTLabs.
|
|
|
@2302
|
7 years |
garnier |
Finally proved associativity of addition on bitvectors. Rejoice.
|
|
|
@2301
|
7 years |
mulligan |
Trying to get the big proof working again
|
|
|
@2300
|
7 years |
campbell |
Cut out some dead ends and add some comments to the last commit.
|
|
|
@2299
|
7 years |
campbell |
Soundly labelled RTLabs structured traces are "unrepeating".
|
|
|
@2298
|
7 years |
garnier |
WIP: converting switch removal from Z to bitvectors. Does not compile, …
|
|
|
@2297
|
7 years |
campbell |
Nicer form of steps until cost label bound in RTLabs.
|
|
|
@2296
|
7 years |
campbell |
Tidy up some ill-placed definitions.
|
|
|
@2295
|
7 years |
campbell |
Start on showing unrepeating property of RTLabs structured traces: …
|
|
|
@2294
|
7 years |
campbell |
Make RTLabs cost spec deterministic.
|
|
|
@2293
|
7 years |
campbell |
Add instruction pointer for call states in RTLabs.
|
|
|
@2292
|
7 years |
campbell |
More RTLabs invariants.
|
|
|
@2291
|
7 years |
campbell |
Disable switch removal in compiler.ma for now.
|
|
|
@2290
|
7 years |
campbell |
Remove jump tables from RTLabs -> RTL.
|
|
|
@2289
|
7 years |
campbell |
Update alias
|
|
|
@2288
|
7 years |
campbell |
Remove jumptables from RTLabs. :(
|
|
|
@2287
|
7 years |
campbell |
RTLabs typing for loads and stores.
|
|
|
@2286
|
7 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
@2285
|
7 years |
sacerdot |
1. duplicated code erased
2. POP case finished up to lemmas on …
|
|
|
@2284
|
7 years |
sacerdot |
PUSH finished
|
|
|
@2283
|
7 years |
mulligan |
Work from today.
|
|
|
@2282
|
7 years |
sacerdot |
PUSH case almost finished
|
|
|
@2281
|
7 years |
sacerdot |
…
|
|
|
@2280
|
7 years |
sacerdot |
Proof repaired.
|
|
|
@2279
|
7 years |
sacerdot |
1. Bug fixed in the semantics of PUSH (no indirection performed)
2. …
|
|
|
@2278
|
7 years |
mulligan |
Half of JC case complete
|
|
|
@2277
|
7 years |
tranquil |
* replaced incorrect use of subvector_with
|
|
|
@2276
|
7 years |
sacerdot |
…
|
|
|
@2275
|
7 years |
tranquil |
* moved around some code (I8051.ma does not depend on ByteValues?.ma …
|
|
|
@2274
|
7 years |
sacerdot |
Dead code commented out and code out of place moved to Test.ma.
|
|
|
@2273
|
7 years |
sacerdot |
1. lemmas moved from all files to Test.ma
2. most of the lemmas in …
|
|
|
@2272
|
7 years |
mulligan |
Changed proof strategy for main lemma after noticed that the current …
|
|
|
@2271
|
7 years |
garnier |
Proof of correction for the semantics of expressions under memory …
|
|
|
@2270
|
7 years |
mulligan |
Bug spotted and fixed in write_at_stack_pointer
|
|
|
@2269
|
7 years |
sacerdot |
Proof completely repaired up to …
|
|
|
@2268
|
7 years |
mulligan |
Bug spotted in instruction_size (lookup_datalabels cannot just be a …
|
|
|
@2267
|
7 years |
sacerdot |
Call is now proved using the new strategy.
|
|
|
@2266
|
7 years |
sacerdot |
All daemons closed in Jmp case.
|
|
|
@2265
|
7 years |
sacerdot |
Commented out code removed.
|
|
|
@2264
|
7 years |
sacerdot |
1) Major change: we now always use the efficient way of resolving …
|
|
|
@2263
|
7 years |
garnier |
Finished proving semantics preservation under memory injections for …
|
|
|
@2262
|
7 years |
mulligan |
Changes from today.
|
|
|
@2261
|
7 years |
mulligan |
Resolved conflict
|
|
|
@2260
|
7 years |
sacerdot |
Now we use the efficient lookup_address.
|
|
|
@2259
|
7 years |
mulligan |
For Claudio
|
|
|
@2258
|
7 years |
sacerdot |
1. lemma generalized
2. automation replaced with expansion to make …
|
|
|
@2257
|
7 years |
mulligan |
Daemon in SETB case closed.
|
|
|
@2256
|
7 years |
mulligan |
MOV and MOVX cases complete
|
|
|
@2255
|
7 years |
garnier |
Had to modify the definition of memory injections to prove that …
|
|
|
@2254
|
7 years |
campbell |
Fix up invariants in Cminor semantics.
|
|
|
@2253
|
7 years |
campbell |
Cminor to RTLabs is now a total function.
|
|
|
@2252
|
7 years |
campbell |
Use the return statement invariant. Restructure the invariants for …
|
|
|
@2251
|
7 years |
campbell |
Add new invariant to Cminor that return typs should be respected.
|
|
|
@2250
|
7 years |
campbell |
Tidy up Clight to Cminor pass a bit.
|
|
|
@2249
|
7 years |
campbell |
Tweak Cminor invariant to be slightly more readable/extendable.
|
|
|
@2248
|
7 years |
sacerdot |
Final changes. All daemons removed, but the real one (open goal).
|
|
|
@2247
|
7 years |
mulligan |
Work on the MOV instruction from today and bug fixes in set_arg_1.
|
|
|
@2246
|
7 years |
sacerdot |
Final technical lemma streamlined. Maybe it can be streamlined even more.
|
|
|
@2245
|
7 years |
sacerdot |
Temporary commit to have a backtracking point. Yes, I know this breaks …
|
|
|
@2244
|
7 years |
sacerdot |
Technical lemma used.
|
|
|
@2243
|
7 years |
sacerdot |
One more lemma streamlined, one to go + one to be completed.
|
|
|
@2242
|
7 years |
sacerdot |
jump_expansion_step3 streamlined
|
|
|
@2241
|
7 years |
boender |
- merged changes by Claudio
|
|
|
@2240
|
7 years |
sacerdot |
All "interesting" technical lemmas singled out, proofs to be uncommented.
|
|
|
@2239
|
7 years |
sacerdot |
One more lemma polished.
|
|
|
@2238
|
7 years |
sacerdot |
Taken out lemma integrated.
|
|
|
@2237
|
7 years |
sacerdot |
Even shorter version.
|
|
|
@2236
|
7 years |
sacerdot |
One subproof made shorter.
|
|
|
@2235
|
7 years |
sacerdot |
Towards smaller proofs.
|
|
|
@2234
|
7 years |
garnier |
Progress on proving semantics preservation under memory injections.
|
|
|
@2233
|
7 years |
tranquil |
* completed update of ERTL semantics
* some minor changes in joint …
|
|
|
@2232
|
7 years |
campbell |
Remove unused block structure in Cminor.
|
|
|
@2231
|
7 years |
garnier |
Various tiny lemmas used in at least two files in the fornt-end.
|
|
|
@2230
|
7 years |
sacerdot |
Glue proof maximally simplified or sort of.
|
|
|
@2229
|
7 years |
sacerdot |
More cleaning up, ready for more aggressive factorization.
|
|
|
@2228
|
7 years |
sacerdot |
Further proof reduction.
|
|
|
@2227
|
7 years |
garnier |
* New version of the switch removal algorithm, described at the top of …
|
|
|
@2226
|
7 years |
campbell |
Whole program proof.
|
|
|
@2225
|
7 years |
sacerdot |
Minor and major improvements everywhere, shortened proofs.
|
|
|
@2224
|
7 years |
campbell |
Proper whole program result in RTLabs/Traces
|
|
|
@2223
|
7 years |
campbell |
Simplify RTLabs structure traces proofs by getting rid of wrong …
|
|
|
@2222
|
7 years |
sacerdot |
More robust to possible future changes to the "in match" semantics …
|
|
|
@2221
|
7 years |
boender |
- removed cases daemon from PolicyFront?
|
|
|
@2220
|
7 years |
sacerdot |
Some minor speed up and daemon-uncommenting.
|
|
|
@2219
|
7 years |
campbell |
Speed up cast simplification proof checking a bit.
|
|
|
@2218
|
7 years |
campbell |
Separate out cost properties required of RTLabs programs from the …
|
|
|