NPEs when checking and diagnosing realizability

[fraimondi]

Hi,
I have a couple of null-pointer exceptions on a very simple example when running realizability checking (Kind2) and diagnosing them (JKind).
I'm using
Mac OS 15.4.1
JKind 4.5.1-202311081135
Detected solvers: smtinterpol, z
kind2 v2.3.0
NuSMV 2.6.0

If I select Kind2, I have a NPE when checking realizability
If I select JKind, I can check realizability (and it correctly detects one problem), but I get a NPE when diagnosing it.

The diff below fixes diagnosability when using JKind. For Kind2, the diff avoids the NPE but it cannot run.

Let me know if you need anything else, and thanks :-)!

diff --git a/fret-electron/analysis/realizabilityCheck.js b/fret-electron/analysis/realizabilityCheck.js
index eb7d29b..027dda9 100644
--- a/fret-electron/analysis/realizabilityCheck.js
+++ b/fret-electron/analysis/realizabilityCheck.js
@@ -34,7 +34,9 @@ export function checkRealizability(filePath, engine, options, callback) {
       if (engine === 'kind2') {
         var kind2Output = JSON.parse(stdout);
         var logResults = kind2Output.filter(e => ((e.objectType === "log") && (e.level === "error")))[0];
-        err.message = err.message + '\n' + logResults.value.toString();
+        if (logResults && ('value' in logResults) ) {
+          err.message = err.message + '\n' + logResults.value.toString();
+        }
       }
       var errorMessage = 'Error: ' + (engine === 'jkind' ? 'JKind' : 'Kind 2') + ' call terminated unexpectedly.'
       callback(errorMessage);
@@ -43,11 +45,16 @@ export function checkRealizability(filePath, engine, options, callback) {
       if (engine === 'jkind') {
         result = stdout.match(new RegExp('(?:\\+\\n)' + '(.*?)' + '(?:\\s\\|\\|\\s(K|R|S|T))'))[1];
         time = stdout.match(new RegExp('(Time = )(.*?)\\n'))[2];        
-        
+
         if (options.includes('json')) {
           var fileContent = fs.readFileSync(filePath+'.json', 'utf8');
           jsonOutput = JSON.parse(fileContent);
-          if (result === "REALIZABLE") {
+          if (result === "REALIZABLE" 
+               && jsonOutput 
+               && ('Counterexample' in jsonOutput) 
+               && Array.isArray(jsonOutput.Counterexample)  
+               && Array.isArray(jsonOutput.Counterexample[0])
+               && jsonOutput.Counterexample[0].length >1 ) {
             realizableTraceInfo = {K: Object.keys(jsonOutput.Counterexample[0]).length - 2, Trace: jsonOutput.Counterexample};
           } else {
             realizableTraceInfo = null;

[andreaskatis]

Hi @fraimondi ,

Thank you for your message. I would like to look into this more, but the currently attached JSON file contains only the requirement information. Would you mind sharing with me an updated version that also includes variable information in it (i.e. variable and data types as you have filled them in the Variable Mapping tab).

To do this you need to export the project by selecting Requirements & Variables in the Select data type option before exporting (see screenshot below).

Best,

Andreas

[fraimondi]

Thank you Andreas,

This is the export with variables.
I also attach:

1. The file that creates problems with Kind2 I had to add a .txt extension to upload, please remove. If I execute kind2 --lus_main rover_cc0Spec -json --enable CONTRACTCK --timeout 900 rover_cc0Spec.lus, the json that is returned finishes with the following:

[...]
,
{
  "objectType" : "log",
  "level" : "fatal",
  "source" : "parse",
  "value" : "Runtime failure in contract checker: SMT solver failed: tactic failed: unknown"
}

(notice that level is "fatal", not "error")

2. The file that creates problems with jKind: here Counterexamples seems an empty array.

[andreaskatis]

Thank you, @fraimondi .

I was testing things in the meantime and I did encounter the Kind 2 message that you shared, but it was only occuring with specific combinations of versions of Kind 2 and Z3. Would you mind letting me know the version of Z3 that you are using? You can do so by running the following command in the command line.

z3 -h

Best,

Andreas

[fraimondi]

Hi Andreas,

z3 -h

The output is:

Z3 [version 4.12.5 - 64 bit]

[andreaskatis]

Thank you for the quick responses, @fraimondi !

I was able to replicate the issue with Kind 2 v2.3.0 + Z3 v4.12.5 . It appears that Kind 2 v2.3.0 may not fully support that version of Z3, as it is a few releases old. I will share this info with the Kind 2 developers, perhaps it is something that can be fixed on their end.

From my experience testing things today, the same issue does not come up with Z3 v4.14.1 , which is the latest version available through OPAM. So I would suggest that you update to at least that version of Z3 to overcome this.

As for the JKind NPE, the actual issue seems to be due to an odd case in the diagnosis engine, when it comes to handling diagnosis of singleton requirements. I will work on a fix and provide an update here when it has gone public.

Thanks again for reporting these. Feel free to let us know if you have any further questions regarding the realizability checking feature in FRET.

Best,

Andreas

[fraimondi]

Hi Andreas,
I upgraded Z3 (I use brew on mac): with version 4.15.0 everything seems to work fine with Kind2.
Thanks!
Franco