Elazar Gershuni comments

Results 102 comments of


                                            Elazar Gershuni

Add FiniteDomain

This PR may be complementent by moving the type domain outside too, as demonstrated by #673.

State of hardware performance monitoring in WSL2

``` $ /usr/lib/linux-tools/6.8.0-45-generic/perf stat ls event syntax error: 'cpu_core/TOPDOWN.SLOTS,metric-id=cpu_core!3TOPDOWN.SLOTS!3/,cpu_core/topdown-retiring,metric-id=cpu_core!3topdo..' \___ Bad event or PMU Unable to find PMU or event on a PMU of 'cpu_core' Initial error: event syntax error:...

Type not narrowed correctly for `if X in collection`

Related #2357 #1203

Move definitions inside ebpf_vm_isa.hpp out of prevail namespace

Should they even be part of prevail? There needs to be a different source for this.

Move definitions inside ebpf_vm_isa.hpp out of prevail namespace

I think there needs to be an ebpf_spec repository with definitions related to specification, stuff that is relevant to interpreters, verifiers or both. This dependency should replace the dependency on...

Check for unreachable exit

I think exit unreachability is not the same as having an infinite loop. It might happen due to failed assertions or bugs, and an infinite loop on one path may...

Check for unreachable exit

> Would it make more sense to scan the post condition for each state to find any with loop count > threshold? In order to pinpoint the location? Yes, I...

Check for unreachable exit

Might be simplest to add a special assertion instruction for each increment. Then you have no special termination handling code in generate report. I'm not sure if thats better overall.

Check for unreachable exit

> > Might be simplest to add a special assertion instruction for each increment. Then you have no special termination handling code in generate report. I'm not sure if thats...