LHS of #Exists binds variables

[radumereuta]

Fixes: #2709
Just for reference, this is how the passing rule looks like at different stages:

orig:     rule { C #Equals { C }:>Int } => #Exists I1. { C #Equals I1:Int } [simplification]
parsed:   rule #Equals(#SemanticCastToK(C),`project:Int`(#SemanticCastToK(C)))=>#Exists(#SemanticCastToInt(I1),#Equals(#SemanticCastToK(C),#SemanticCastToInt(I1))) requires #token("true","Bool") ensures #token("true","Bool") [org.kframework.attributes.Location(Location(9,8,9,68)), org.kframework.attributes.Source(Source(/home/radu/work/k/k-distribution/tests/regression-new/checks/existsLHSBoundPass.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification]
compiled: rule #Equals(C,`project:Int`(C))=>#Exists(I1,#Equals(C,I1)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(bf3584916f98d9712a09c2f26f0a1bdd55ff9c3f406b4d0c5c83ee09104a5dc0), org.kframework.attributes.Location(Location(9,8,9,68)), org.kframework.attributes.Source(Source(/home/radu/work/k/k-distribution/tests/regression-new/checks/existsLHSBoundPass.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification]
kore:
// rule #Equals{K,#SortParam}(C,inj{Int,KItem}(`project:Int`(C)))=>#Exists{Int,#SortParam}(I1,#Equals{K,#SortParam}(C,inj{Int,KItem}(I1))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(bf3584916f98d9712a09c2f26f0a1bdd55ff9c3f406b4d0c5c83ee09104a5dc0), org.kframework.attributes.Location(Location(9,8,9,68)), org.kframework.attributes.Source(Source(/home/radu/work/k/k-distribution/tests/regression-new/checks/existsLHSBoundPass.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
  axiom{R,Q0} \implies{R} (
    \top{R}(),
    \equals{Q0,R} (
      \equals{SortK{}, Q0}(VarC:SortK{},kseq{}(inj{SortInt{}, SortKItem{}}(Lblproject'Coln'Int{}(VarC:SortK{})),dotk{}())),
     \and{Q0} (
       \exists{Q0}(VarI1:SortInt{},\equals{SortK{}, Q0}(VarC:SortK{},kseq{}(inj{SortInt{}, SortKItem{}}(VarI1:SortInt{}),dotk{}()))),
        \top{Q0}())))
  [sortParams{}("{Q0}"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/radu/work/k/k-distribution/tests/regression-new/checks/existsLHSBoundPass.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(9,8,9,68)"), simplification{}(), UNIQUE'Unds'ID{}("bf3584916f98d9712a09c2f26f0a1bdd55ff9c3f406b4d0c5c83ee09104a5dc0")]

@ehildenb please review
@PetarMax does this properly fix the issue you were having?

[PetarMax]

Yes, this fixes the issue.

[ehildenb]

This solutino looks like it won't work to me. We are just tracking if we are inside an exists, not the actual variable the exists binds. Does it work correctly on the following code?

rule foo(X) => #Exists Y . { I #Equals Y }

In particular, this one should:

• Warn about unused variable X
• No error about variable Y.
• Error about variable I, it's a universal variable only on the RHS of a rule, so should be ?I instead.

[ehildenb]

In particular, you need to track the boundVars set, instead of just tracking "am I inside an Exists/Forall".

so your code should check:

• Am I under an Exists X . ..., if so, then add X to the bound vars set for when recursing into the .... (Same for Forall).
• When checking variables (the KVariable case), if a variable is unbound, the same checks as before happen. But if a variable is bound, then it does not have the same restrictinos as before.

[radumereuta]

rule foo(X) => #Exists Y . { I #Equals Y }
[Warning] Compiler: Variable 'X' defined but not used. Prefix variable name with underscore if this is intentional.
	Source(/home/radu/work/test/test.k)
	Location(18,12,18,13)
	18 |	  rule foo(X) => #Exists Y . { I #Equals Y }
	   .	           ^
[Error] Compiler: Found variable I on right hand side of rule, not bound on left hand side. Did you mean "?I"?
	Source(/home/radu/work/test/test.k)
	Location(18,32,18,33)
	18 |	  rule foo(X) => #Exists Y . { I #Equals Y }
	   .	                               ^
[Warning] Compiler: Variable 'I' defined but not used. Prefix variable name with underscore if this is intentional.
	Source(/home/radu/work/test/test.k)
	Location(18,32,18,33)
	18 |	  rule foo(X) => #Exists Y . { I #Equals Y }
	   .	                               ^

Added ?

rule foo(X) => #Exists Y . { ?I #Equals Y }
[Warning] Compiler: Variable 'X' defined but not used. Prefix variable name with underscore if this is intentional.
	Source(/home/radu/work/test/test.k)
	Location(18,12,18,13)
	18 |	  rule foo(X) => #Exists Y . { ?I #Equals Y }
	   .	           ^
[Warning] Compiler: Variable '?I' defined but not used. Prefix variable name with underscore if this is intentional.
	Source(/home/radu/work/test/test.k)
	Location(18,32,18,34)
	18 |	  rule foo(X) => #Exists Y . { ?I #Equals Y }
	   .	                               ^~

If you look at the code, I modified GatherVarsVisitor. This tracks if we are in the LHS of a #Forall or #Exists, and if we find a variable, we add it to the bound set.
The original error message was thrown from CheckRHSVariables which relies on the visitor I just changed.

[ehildenb]

Add these as tests please. No reason not to.

[radumereuta]

Done.
First two were testing the llvm backend, the second two tests the haskell backend. One fail, one passing.