Factored identifier encoding #394

ehildenb · 2019-04-04T18:18:24Z

Makes some common machinery for escaping identifiers to various encoding formats.

…specific one as modifications on default

…cations

…ringToAlphanumeric method

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

…tually copy asciiReadableEncodingDefault

…terize in escape char

… filtering (#394)

* llvm-backend/src/main/native/llvm-backend: 3d72166 - Rename #True and #False to #Top and #Bottom in kprint (#393) * llvm-backend/src/main/native/llvm-backend: 3d008ee - Fix substitution filtering (#394)

This PR changes `KCFGExplore.cterm_implies`: * to always bind variables in the consequent This change is motivated by #394 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>

This PR is factored-out from #394. Changes: * `EqualityProver.advance_proof` now calls `cterm_implies` to check the implication of form `(dummy_config #And constraints) #Implies ((dummy_config #And LHS) #Equals (dummy_config #And RHS)))` where `dummy_config` is the configuration of the semantics (in our case, IMP) with all cells holding symbolic variables. * tests for various edge-cases, specifically when the constraints are `#Bottom`. Is this case, the proof should pass trivially, issuing a warning to the user. --------- Co-authored-by: devops <devops@runtimeverification.com>

This PR takes some methods for the `Proof` abstract class from #394 into a separate pull request. Adds: - `Proof.digest()` - `Proof.up_to_date(check_method)` - `Proof.read_proof(id, proof_dir)`, Generic way to read a proof from a file, regardless of type - `hash_file(file)` to compute the hash of a file A test for `read_proof` with test cases for each of the 3 existing proof types This test should currently be failing due to #484. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

This PR pulls the Subproof-related components out of #394. It also adds a default implementation of `dict` for the `Proof` class, which includes the proof ID and any subproofs. This can be built on by any implementing classes. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

runtimeverification/pyk#396 Work towards [evm-semantics#1753](runtimeverification/evm-semantics#1753) Blocked on: #419 Changes: **Subproofs** * `Proof` now holds a list of proof ids that are required to pass for the parent proof to pass. If a proof has subproofs, it must have a `proof_dir` set, and the subproofs are looked up there. * factor-out `read_proof` to be a standalone function, rather than a `Proof` static method. This allows looking up the proof type in the JSON and returning the proof of the appropriate type * Modifies the `*Proof.status` property to consider subproofs * adds unit tests for the above logic Subproofs are intended to serve as "proof obligations", i.e. auxiliary proofs that are factored-out of a larger ongoing proof. All subproofs are "direct dependencies" of their parent proof, i.e. the parent proof cannot have *explicit* chains of subproofs. These chains could be implicit, i.e. the subproofs can have their own subproofs. Related work is the `ProofSchedule` (PR #396) --- it is intended to make transitive dependencies explicit by organizing them into a DAG. **Node refutation** Having subproofs allows us to add a possibility to refute nodes in the `APRProver`. Refuting a node means (see `APRProver.refute_node`): * marking it as expanded in the KCFG of the proof * generating a `RefutationProof` that states the following: the conjunction of the node's conditions along the path AND the the condition of the first node down the split is unsatisfiable * Add the generated proof as a subproof of the parent `APRProof`. * If all stuck nodes of a proof haver a passing refutation, the parent proof passes. *Note*: The node refutations proofs are proofs of the unsatisfiability of the node's path constraint. They have different meaning than `EqualityProof`'s, and are constructed in a slightly different way. I've decided to separate `RefutationProof` into its own class that does not inherit `EqualityProof` to make this distinction clear. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com> Co-authored-by: Noah Watson <noah@nwatson.xyz> Co-authored-by: Noah Watson <107630091+nwatson22@users.noreply.github.com>

This PR changes `KCFGExplore.cterm_implies`: * to always bind variables in the consequent This change is motivated by #394 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>

This PR is factored-out from #394. Changes: * `EqualityProver.advance_proof` now calls `cterm_implies` to check the implication of form `(dummy_config #And constraints) #Implies ((dummy_config #And LHS) #Equals (dummy_config #And RHS)))` where `dummy_config` is the configuration of the semantics (in our case, IMP) with all cells holding symbolic variables. * tests for various edge-cases, specifically when the constraints are `#Bottom`. Is this case, the proof should pass trivially, issuing a warning to the user. --------- Co-authored-by: devops <devops@runtimeverification.com>

This PR takes some methods for the `Proof` abstract class from #394 into a separate pull request. Adds: - `Proof.digest()` - `Proof.up_to_date(check_method)` - `Proof.read_proof(id, proof_dir)`, Generic way to read a proof from a file, regardless of type - `hash_file(file)` to compute the hash of a file A test for `read_proof` with test cases for each of the 3 existing proof types This test should currently be failing due to #484. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

This PR pulls the Subproof-related components out of #394. It also adds a default implementation of `dict` for the `Proof` class, which includes the proof ID and any subproofs. This can be built on by any implementing classes. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

runtimeverification/pyk#396 Work towards [evm-semantics#1753](runtimeverification/evm-semantics#1753) Blocked on: #419 Changes: **Subproofs** * `Proof` now holds a list of proof ids that are required to pass for the parent proof to pass. If a proof has subproofs, it must have a `proof_dir` set, and the subproofs are looked up there. * factor-out `read_proof` to be a standalone function, rather than a `Proof` static method. This allows looking up the proof type in the JSON and returning the proof of the appropriate type * Modifies the `*Proof.status` property to consider subproofs * adds unit tests for the above logic Subproofs are intended to serve as "proof obligations", i.e. auxiliary proofs that are factored-out of a larger ongoing proof. All subproofs are "direct dependencies" of their parent proof, i.e. the parent proof cannot have *explicit* chains of subproofs. These chains could be implicit, i.e. the subproofs can have their own subproofs. Related work is the `ProofSchedule` (PR #396) --- it is intended to make transitive dependencies explicit by organizing them into a DAG. **Node refutation** Having subproofs allows us to add a possibility to refute nodes in the `APRProver`. Refuting a node means (see `APRProver.refute_node`): * marking it as expanded in the KCFG of the proof * generating a `RefutationProof` that states the following: the conjunction of the node's conditions along the path AND the the condition of the first node down the split is unsatisfiable * Add the generated proof as a subproof of the parent `APRProof`. * If all stuck nodes of a proof haver a passing refutation, the parent proof passes. *Note*: The node refutations proofs are proofs of the unsatisfiability of the node's path constraint. They have different meaning than `EqualityProof`'s, and are constructed in a slightly different way. I've decided to separate `RefutationProof` into its own class that does not inherit `EqualityProof` to make this distinction clear. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com> Co-authored-by: Noah Watson <noah@nwatson.xyz> Co-authored-by: Noah Watson <107630091+nwatson22@users.noreply.github.com>

…ification/pyk#416) This PR changes `KCFGExplore.cterm_implies`: * to always bind variables in the consequent This change is motivated by #394 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>

This PR is factored-out from #394. Changes: * `EqualityProver.advance_proof` now calls `cterm_implies` to check the implication of form `(dummy_config #And constraints) #Implies ((dummy_config #And LHS) #Equals (dummy_config #And RHS)))` where `dummy_config` is the configuration of the semantics (in our case, IMP) with all cells holding symbolic variables. * tests for various edge-cases, specifically when the constraints are `#Bottom`. Is this case, the proof should pass trivially, issuing a warning to the user. --------- Co-authored-by: devops <devops@runtimeverification.com>

…n/pyk#485) This PR takes some methods for the `Proof` abstract class from #394 into a separate pull request. Adds: - `Proof.digest()` - `Proof.up_to_date(check_method)` - `Proof.read_proof(id, proof_dir)`, Generic way to read a proof from a file, regardless of type - `hash_file(file)` to compute the hash of a file A test for `read_proof` with test cases for each of the 3 existing proof types This test should currently be failing due to #484. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>