Rename some exploration strategies - Simplify DFS and random selection

[fruffy]

This PR does two major things:

Renames some components and deletes strategies which are defunct:

• IncrementalStack -> DepthFirstSearch
• RandomAccessStack -> [deleted]
• IncrementalMaxCoverageStack -> [deleted]
• LinearEnumeration -> [deleted]
• UnboundedRandomAccessStack -> RandomBacktrack
• GreedyPotential -> GreedyStmtSelection
• RandomAccessMaxCoverage -> RandomMaxStmtCoverage
• ExplorationStrategy -> SymbolicExecutor

The second part of this PR is a simplification of DFS and random search. Most of the stack code is removed and the list of unexplored branches is flattened. We also do early pruning now. Branches are only added to the list of unexplored branches if their path conditions are actually satisfiable. We only select a branch from a list that can be satisfied.

[fruffy]

@VolodymyrPeschanenko
This PR simplifies DFS to be more efficient and less complex in implementation. However, the gtest for the reachability analysis is running into an infinite loop. In particular the command

p4c/build/p4testgen -I "p4c/build/p4include" --target bmv2  --std p4-16 --test-backend STF --arch v1model --seed 1000 --max-tests 10  --pattern "ingress.MyAction1;ingress.table2" --out-dir "p4c/build/tmp" "p4c/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_if.p4"

Do you know what the cause of this could be?

Edit: I think I found the root cause and fixed it. The analysis always returns its own state, which may cause it to execute on the same execution state forever.

[VolodymyrPeschanenkoLitSoft]

@VolodymyrPeschanenko This PR simplifies DFS to be more efficient and less complex in implementation. However, the gtest for the reachability analysis is running into an infinite loop. In particular the command

p4c/build/p4testgen -I "p4c/build/p4include" --target bmv2  --std p4-16 --test-backend STF --arch v1model --seed 1000 --max-tests 10  --pattern "ingress.MyAction1;ingress.table2" --out-dir "p4c/build/tmp" "p4c/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_if.p4"

Do you know what the cause of this could be?

Edit: I think I found the root cause and fixed it. The analysis always returns its own state, which may cause it to execute on the same execution state forever.

I can't repeat this problem on MacOS. I'll try to check it on the latest ubuntu, but it'll take some time.

[fruffy]

I can't repeat this problem on MacOS. I'll try to check it on the latest ubuntu, but it'll take some time.

Thanks for checking! I implemented a fix for it here:
a7eeca8

Do these changes make sense? Otherwise I run into an infinite loop.

[VolodymyrPeschanenkoLitSoft]

I can't repeat this problem on MacOS. I'll try to check it on the latest ubuntu, but it'll take some time.

Thanks for checking! I implemented a fix for it here: a7eeca8

Do these changes make sense? Otherwise I run into an infinite loop.

Yes, these changes are correct.

[jnfoster]

Love getting the names right!