Silent concreterization

[sohah]

This is the issue reported by Georges regarding silent object concretization.

Here follows a reproducer for the bug about silent concretization when casting to Object. Here follows the code:

import gov.nasa.jpf.symbc.Debug;

import java.util.HashMap;
import java.util.Map;

public class Compare {
    protected Compare() {
        // prevents calls from subclass
        throw new UnsupportedOperationException();
    }
    private static Map<String, Object> map;
    public static void main(String[] args) {
        map = new HashMap<>();
        boolean mybool = Debug.makeSymbolicBoolean("randomvalue");
        map.put("abc", mybool);
        if ((boolean) map.get("abc")) {
            System.out.println("loose");
            assert (false);
        } else {
            System.out.println("win");
        }
        return;
    }
}
 

And I put the output of JR attached (as you see, it does not report any error, while it should as we can reach the assert (false) ) .

the log file is below

symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
* running veritesting with SPFCases and Early Returns.
JavaPathfinder core system v8.0 (rev 0df77f0a2a8fa55d58a4ed89b70b61e39626866c) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Compare.main()

====================================================== search started: 10/2/20 11:24 PM
win

====================================================== VeritestingListener report:
Encountered Veritesting Regions in veriRegions (i.e., VeriTestingMain.veriRegions size) = 0

/************************ Printing Exception Statistics *****************
Static Analysis exceptions count = 0
Instantiation Time exceptions count = 0
Unknown phases exception count = 0


/************************ Printing Time Decomposition Statistics *****************
static analysis time = 0 msec
Veritesting Dyn Time = 261 msec
Veritesting fix-point Time = 0 msec
GoTo rewrite instances = 0

/************************ Printing Solver Statistics *****************
Total Solver Queries Count = 0
Total Solver Time = 0 msec
Total Solver Parse Time = 0 msec
Region Summary Parse Time = 0 msec
Total Solver Clean up Time = 0 msec
PCSatSolverCount = 0
PCSatSolverTime = 0 msec
Constant Propagation Time for PC sat. checks = 0
Array SPF Case count = 0
If-removed count = 0

/************************ Printing Region Statistics *****************
Number of Distinct Veritested Regions = 0
Number of Distinct Un-Veritested Symbolic Regions = 0
Number of Distinct Failed Regions for Field Reference = 0
Number of Distinct Failed Regions for SPFCases = 0
Number of Distinct Failed Regions for missing method summaries = 0
Number of Distinct Failed Regions for Other Reasons = 0
Number of High Order Regions Used = 0

/************************ Printing Instantiation Statistics *****************
Number of successful instantiations = 0
Total Number of unsuccessful instantiations = 0
Number of failed instantiations due to Field Reference = 0
Number of failed instantiations due to SPFCases = 0
Number of failed instantiations due to missing method summaries = 0
Number of failed instantiations due to Other Reasons = 0


Number of Veritested Regions Instances = 0
Printing keys of regions that were instantiated at least once
Finished printing keys of regions that were instantiated at least once

Metrics Vector:
261,0,261,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,-1,0.0,0,0,0

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=374,released=11,maxLive=0,gcCycles=1
instructions:       3368
max memory:         123MB
loaded code:        classes=63,methods=1336

====================================================== search finished: 10/2/20 11:24 PM