ClassCastException in ExpressionValueVisitor.MemoryLocationEvaluator
For 94 of the intel-tdx tasks in SV-Benchmarks we get the following exception:
Exception in thread "main" java.lang.ClassCastException: class org.sosy_lab.cpachecker.cfa.ast.c.CCastExpression cannot be cast to class org.sosy_lab.cpachecker.cfa.ast.c.CLeftHandSide (org.sosy_lab.cpachecker.cfa.ast.c.CCastExpression and org.sosy_lab.cpachecker.cfa.ast.c.CLeftHandSide are in unnamed module of loader 'app')
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor$MemoryLocationEvaluator.visit(ExpressionValueVisitor.java:332)
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor$MemoryLocationEvaluator.visit(ExpressionValueVisitor.java:1)
at org.sosy_lab.cpachecker.cfa.ast.c.CFieldReference.accept(CFieldReference.java:121)
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor$MemoryLocationEvaluator.visit(ExpressionValueVisitor.java:334)
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor$MemoryLocationEvaluator.visit(ExpressionValueVisitor.java:1)
at org.sosy_lab.cpachecker.cfa.ast.c.CFieldReference.accept(CFieldReference.java:121)
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor$MemoryLocationEvaluator.visit(ExpressionValueVisitor.java:334)
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor$MemoryLocationEvaluator.visit(ExpressionValueVisitor.java:1)
at org.sosy_lab.cpachecker.cfa.ast.c.CFieldReference.accept(CFieldReference.java:121)
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor.evaluateMemoryLocation(ExpressionValueVisitor.java:231)
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor.evaluateLValue(ExpressionValueVisitor.java:117)
at org.sosy_lab.cpachecker.cpa.value.ExpressionValueVisitor.evaluateCFieldReference(ExpressionValueVisitor.java:210)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.visit(AbstractExpressionValueVisitor.java:1680)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.visit(AbstractExpressionValueVisitor.java:1)
at org.sosy_lab.cpachecker.cfa.ast.c.CFieldReference.accept(CFieldReference.java:126)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.visit(AbstractExpressionValueVisitor.java:179)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.visit(AbstractExpressionValueVisitor.java:1)
at org.sosy_lab.cpachecker.cfa.ast.c.CBinaryExpression.accept(CBinaryExpression.java:48)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.visit(AbstractExpressionValueVisitor.java:179)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.visit(AbstractExpressionValueVisitor.java:1)
at org.sosy_lab.cpachecker.cfa.ast.c.CBinaryExpression.accept(CBinaryExpression.java:48)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.visit(AbstractExpressionValueVisitor.java:179)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.visit(AbstractExpressionValueVisitor.java:1)
at org.sosy_lab.cpachecker.cfa.ast.c.CBinaryExpression.accept(CBinaryExpression.java:48)
at org.sosy_lab.cpachecker.cpa.value.AbstractExpressionValueVisitor.evaluate(AbstractExpressionValueVisitor.java:2400)
at org.sosy_lab.cpachecker.cpa.value.ValueAnalysisTransferRelation.handleFunctionCallEdge(ValueAnalysisTransferRelation.java:354)
at org.sosy_lab.cpachecker.cpa.value.ValueAnalysisTransferRelation.handleFunctionCallEdge(ValueAnalysisTransferRelation.java:1)
at org.sosy_lab.cpachecker.core.defaults.ForwardingTransferRelation.getAbstractSuccessorsForEdge(ForwardingTransferRelation.java:164)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.callTransferRelation(CompositeTransferRelation.java:295)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForSimpleEdge(CompositeTransferRelation.java:263)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForEdge(CompositeTransferRelation.java:190)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessors(CompositeTransferRelation.java:88)
at org.sosy_lab.cpachecker.cpa.arg.ARGTransferRelation.getAbstractSuccessors(ARGTransferRelation.java:45)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:334)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:289)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:260)
[...]
Example command line:
bin/cpachecker --option cpa.arg.compressWitness=true --option counterexample.export.compressWitness=true --option termination.compressWitness=true --svcomp25 --heap 10000M --benchmark --timelimit '900 s' --stats --spec test/programs/benchmarks/properties/unreach-call.prp --64 test/programs/benchmarks/intel-tdx-module/tdh_mng_vpflushdone__requirement__invalid_state_tdr_metadata_havoc_memory.i
This is likely because the program contains field accesses on something that is the result of a cast: ((pa_t) local_data->vmm_regs.rcx).full_pa.