P icon indicating copy to clipboard operation
P copied to clipboard

[Bug report] Compiling generated Symbolic Java code FAILED!

Open PoorlyDefinedBehaviour opened this issue 1 year ago • 3 comments

Getting this compilation error in the example below using PSym as the target.

The error

[THIS SHOULD NOT HAVE HAPPENED, please report it to the P team or create a GitHub issue]
Compiling generated Symbolic Java code FAILED!
[ERROR] COMPILATION ERROR : 
[ERROR] /home/bruno/dev/formal-methods/p_lang_crash_repro_1/PGenerated/Symbolic/SingleDecreePaxosProgram.java:[92,73] incompatible types: psym.valuesummary.PrimitiveVS<java.lang.Integer> cannot be converted to psym.valuesummary.UnionVS
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.1:compile (default-compile) on project SingleDecreePaxos: Compilation failure
[ERROR] /home/bruno/dev/formal-methods/p_lang_crash_repro_1/PGenerated/Symbolic/SingleDecreePaxosProgram.java:[92,73] incompatible types: psym.valuesummary.PrimitiveVS<java.lang.Integer> cannot be converted to psym.valuesummary.UnionVS
[ERROR] 
[ERROR] -> [Help 1]
[ERROR] 
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e switch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR] 
[ERROR] For more information about the errors and possible solutions, please read the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/MojoFailureException

Environment

p --version
P version 2.2.2.0
~~ [PTool]: Thanks for using P! ~~

mvn --version
Apache Maven 3.6.3
Maven home: /usr/share/maven
Java version: 11.0.24, vendor: Ubuntu, runtime: /usr/lib/jvm/java-11-openjdk-amd64
Default locale: en_US, platform encoding: UTF-8
OS name: "linux", version: "6.8.0-45-generic", arch: "amd64", family: "unix"

Code to reproduce

// PTst/TestDriver.p
machine Foo {
  start state Init {
    entry {
      var count: map[any, int];
      var value: int;

      value = 1;

      count[value] = count[value] + 1;
    }
  }
}
// project.pproj
<Project>
<ProjectName>SingleDecreePaxos</ProjectName>
<InputFiles>
	<PFile>./PSrc/</PFile>
	<PFile>./PSpec/</PFile>
	<PFile>./PTst/</PFile>
</InputFiles>
<OutputDir>./PGenerated/</OutputDir>
<Target>PSym</Target>
</Project>

PoorlyDefinedBehaviour avatar Oct 04 '24 00:10 PoorlyDefinedBehaviour

@aman-goel can you please help here?

ankushdesai avatar Oct 07 '24 16:10 ankushdesai

Hi @PoorlyDefinedBehaviour . Thanks for trying out PSym! PSym currently does not support type-casting with the any data type. Try changing var count: map[any, int]; to var count: map[int, int];.

aman-goel avatar Oct 07 '24 18:10 aman-goel

Hi @PoorlyDefinedBehaviour . Thanks for trying out PSym! PSym currently does not support type-casting with the any data type. Try changing var count: map[any, int]; to var count: map[int, int];.

I see, would it make sense to improve the error message a little bit?

PoorlyDefinedBehaviour avatar Oct 12 '24 15:10 PoorlyDefinedBehaviour

We are planning to drop the support for PSym.

ankushdesai avatar Nov 21 '24 17:11 ankushdesai