Conversation
N1ark
added
soteria-rust
N1ark
force-pushed
the
rust-store-optim
branch
from
ecaaaae to
3de6f19
Compare
|
This somehow also needs promoting files |
|
I need to write a GitHub action that can be triggered by a comment (e.g. |
|
Heh fun idea |
|
What a waste of precious earth resources that was |
giltho
left a comment
giltho
left a comment
There was a problem hiding this comment.
Only nitpicks, feel free to ignore all of them
The one question I really have (for a future PR) is: how much work would it be do so that the following program doesn't allocate on the heap? I.e. you put the structure value on the stack and it already has all the necessary structure for reasoning here:
struct A { b : B }
struct B { x : u32 }
fn main() {
let a = A { b : B { x : 12 } };
let x = a.b.x;
}| - Uninit: the symbol is bound to an immediate, uninitialized value. | ||
| - Dead: the symbol is dead; it doesn't exist (e.g. after a [StorageDead]). | ||
| *) | ||
| type 'a binding_kind = |
There was a problem hiding this comment.
This is sufficiently identical to soteria-C that we should probably factor it out?
| let p = precision_of_f v.node.ty in | ||
| match (p, v.node.kind, size) with | ||
| | F32, Float f, 32 -> | ||
| mk 32 @@ Z.of_int32 (Int32.bits_of_float (Stdlib.Float.of_string f)) | ||
| | F64, Float f, 64 -> | ||
| mk 64 @@ Z.of_int64 (Int64.bits_of_float (Stdlib.Float.of_string f)) | ||
| | _, _, _ -> Unop (BvOfFloat (rounding, signed, size), v) <| t_bv size | ||
| Unop (BvOfFloat (rounding, signed, size), v) <| t_bv size |
There was a problem hiding this comment.
Curious why this is more efficient?
There was a problem hiding this comment.
it's not more efficient it's just wrong hahahha
BV.of_float converts a float into its integer representation, e.g. 5.0 becomes 0x5, while IntN.bits_of_float is the bit content of the float (wrong)
| type 'err fun_exec = rust_val list -> (rust_val, unit) Rust_state_m.t | ||
|
|
||
| let get_variable var_id = | ||
| type lazy_ptr = Store of Expressions.local_id | Heap of full_ptr |
There was a problem hiding this comment.
How is lazy_ptr not just "place"?
Or possibly "resolved_place" or something
There was a problem hiding this comment.
well because you don't know if lazy_ptr is a lazy pointer; really it's an (lazy_ptr, full_ptr) Either.t where lazy_ptr = local ⊂ place
I'm not sure; in theory it's "easy" because to each projection you just attach an index. I'm still worried we might miss some unsoundnesses, because load-store does all of the value-validation we want, but supposedly you cant do anything unsafe without going through a pointer (which would lower to the heap), so.... maybe? worth a shot for sure, uncertain what the gains are edit: Created #162 |
* Fix `BV.of_float` + add 2 reductions * Add store optimisation to Rust! * Optim `bv_to_z` * PR comments * Promote tests
Based on #205
Fixes #162
Add the store optimisation to Rust!
Running our Kani + Miri benchmark, we get an average time that goes from 0.232s to 0.211s, so a ~10% improvement!
Also added a couple reductions, and optimised
bv_to_zwhich interprets a bitvector into a signed value; this function went from taking 320 cycles to 31 cycles/op (on one test I tried that was quite slow, where it was used ~4M times)