Unecessary hc lookups in the symbolic memory

[filipeom]

When loading multiple bytes from memory, I consistently create sub-expressions while concatenating bytes. This practice results in unnecessary hc lookups in the problematic code found at:

https://github.com/OCamlPro/owi/blob/d70d88c34d84e91e0f8e795929b23dba60154b88/src/symbolic_memory.ml#L106-L119

For example, when loading a concrete i64 value from memory, it requires performing 7 hc lookups for no valid reason, as the final value is the only one that necessitates hash-consing.

The same issue arises when storing values in memory, leading to the creation of hash-consed expressions for extracted bytes. However, I believe the problem is more pronounced when loading from memory.

This is why I suspect that the performance issue in https://github.com/OCamlPro/owi/pull/118 remains unresolved. For me locally it still runs for a longer duration than expected. @krtab, could you confirm if this is the case?

A potential workaround for this could be to implement a dummy hash-consing function in hc that allows the construction of a ht_expr without performing lookups. Are there any other viable solutions to address this issue? I am keen on retaining hash-consing for path-condition related exprs, as these conditions tend to become very large in big programs.

Edit:

Perhaps making Extract and Concat defined over expr is enough?

  | Extract of expr * int * int
  | Concat of expr * expr

[zapashcanon]

Do you want me to try benchmarking on test-comp with the suggested changes in encoding ?

[filipeom]

I think it probably breaks hash-consing. I'm exploring a solution where we don't perform hashconsing on integers which should fix this issue :smile:

[zapashcanon]

Oh yes, we should no be hash-consing anything that gets compiled to a scalar (unit, bool, and ints)... :sweat_smile: