path-condition slicing

[zapashcanon]

No description provided.

[filipeom]

I guess if get_symbols returns [] it must be a concrete expression that is not being simplified properly 😢

[zapashcanon]

Hum... I believe this branch is sometimes reached. I can provide the list of expressions that are not simplified if you're interested? :)

[zapashcanon]

I added a commit that fails on such not properly simplified expressions, see 5d4b35b

They all seem to be related to ++, extract and extend.

[filipeom]

Ah thanks! I think there are a few of these that I can fix easily.

The ones with pointers are more tricky because I don't want to simplify pointers so much that we loose the Ptr type from a given expression. Then, we would loose the ability to track heap chunks.

Do you think having something like an unsafe_simplify, that is more aggressive and simplifies every concrete expression to a given value helpful here?

[zapashcanon]

I need to think more about it to get a clear idea of what we want. I believe you know better than me so, unsafe_simplify is probably OK for now! :)

[zapashcanon]

I'm getting a few (3):

$ owi c ...
owi: internal error, uncaught exception:
     Invalid_argument("index out of bounds")
     Raised at Stdlib__Domain.join in file "domain.ml", line 299, characters 16-24
     Called from Stdlib__Array.iter in file "array.ml", line 113, characters 31-48
     Called from Owi__Wq.read_as_seq.(fun) in file "src/data_structures/wq.ml", line 17, characters 4-16
     Called from Owi__Cmd_sym.cmd.print_and_count_failures in file "src/cmd/cmd_sym.ml", line 100, characters 10-20
     Called from Owi__Cmd_sym.cmd in file "src/cmd/cmd_sym.ml", line 131, characters 15-49
     Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
     Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

When running on Test-Comp (on programs 829, 843 and 1187).

[zapashcanon]

TODO:

change type t = Smtml.Expr.Set.t Union_find.t to type t = Smtml.Expr.Set.t Union_find.t * Smtml.Expr.Set.t so that we don't have to convert the UF to a set all the time. It should be almost free to maintain.

EDIT: Done in 0255585