From: jjenista Date: Fri, 13 May 2011 20:17:30 +0000 (+0000) Subject: this system checks heap results against runtime pointers to look for analysis bugs... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=8d6ecb5faa7dc88cdead6e1385a4a10c2ec2eec4;p=IRC.git this system checks heap results against runtime pointers to look for analysis bugs. It is currently missing that FlatLiteral nodes can allocation a new string object, coming in a future update. --- diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java index a2bf09fc..583aa3d1 100644 --- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java +++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java @@ -353,6 +353,12 @@ public class DisjointAnalysis implements HeapAnalysis { public Alloc getCmdLineArgsAlloc() { return getAllocationSiteFromFlatNew( constructedCmdLineArgsNew ); } + public Alloc getCmdLineArgAlloc() { + return getAllocationSiteFromFlatNew( constructedCmdLineArgNew ); + } + public Alloc getCmdLineArgBytesAlloc() { + return getAllocationSiteFromFlatNew( constructedCmdLineArgBytesNew ); + } /////////////////////////////////////////// // // end public interface @@ -560,6 +566,8 @@ public class DisjointAnalysis implements HeapAnalysis { // know if something is pointing-to to the cmd line args // and we can verify by checking the allocation site field. protected FlatNew constructedCmdLineArgsNew; + protected FlatNew constructedCmdLineArgNew; + protected FlatNew constructedCmdLineArgBytesNew; @@ -1200,12 +1208,12 @@ public class DisjointAnalysis implements HeapAnalysis { rg.writeGraph("genReach"+fgrn.getGraphName(), true, // write labels (variables) - true, // selectively hide intermediate temp vars - true, // prune unreachable heap regions + false, //true, // selectively hide intermediate temp vars + false, //true, // prune unreachable heap regions true, // hide reachability altogether true, // hide subset reachability states true, // hide predicates - false); // hide edge taints + true); //false); // hide edge taints } break; @@ -1985,8 +1993,7 @@ public class DisjointAnalysis implements HeapAnalysis { mods.addModifier(Modifiers.PUBLIC); mods.addModifier(Modifiers.STATIC); - TypeDescriptor returnType = - new TypeDescriptor(TypeDescriptor.VOID); + TypeDescriptor returnType = new TypeDescriptor(TypeDescriptor.VOID); this.mdAnalysisEntry = new MethodDescriptor(mods, @@ -1994,56 +2001,96 @@ public class DisjointAnalysis implements HeapAnalysis { "analysisEntryMethod" ); + TypeDescriptor argsType = mdSourceEntry.getParamType(0); TempDescriptor cmdLineArgs = new TempDescriptor("analysisEntryTemp_args", - mdSourceEntry.getParamType(0) + argsType ); - FlatNew fnArgs = - new FlatNew(mdSourceEntry.getParamType(0), + new FlatNew(argsType, cmdLineArgs, false // is global ); this.constructedCmdLineArgsNew = fnArgs; + TypeDescriptor argType = argsType.dereference(); + TempDescriptor anArg = + new TempDescriptor("analysisEntryTemp_arg", + argType + ); + FlatNew fnArg = + new FlatNew(argType, + anArg, + false // is global + ); + this.constructedCmdLineArgNew = fnArg; + + TypeDescriptor typeIndex = new TypeDescriptor(TypeDescriptor.INT); + TempDescriptor index = + new TempDescriptor("analysisEntryTemp_index", + typeIndex + ); + FlatLiteralNode fli = + new FlatLiteralNode(typeIndex, + new Integer( 0 ), + index + ); - // jjenista - we might want to model more of the initial context - // someday, so keep this trickery in that case. For now, this analysis - // ignores immutable types which includes String, so the following flat - // nodes will not add anything to the reach graph. - // - //TempDescriptor anArg = - // new TempDescriptor("analysisEntryTemp_arg", - // mdSourceEntry.getParamType(0).dereference() - // ); - // - //FlatNew fnArg = - // new FlatNew(mdSourceEntry.getParamType(0).dereference(), - // anArg, - // false // is global - // ); - // - //TempDescriptor index = - // new TempDescriptor("analysisEntryTemp_index", - // new TypeDescriptor(TypeDescriptor.INT) - // ); - // - //FlatLiteralNode fl = - // new FlatLiteralNode(new TypeDescriptor(TypeDescriptor.INT), - // new Integer( 0 ), - // index - // ); - // - //FlatSetElementNode fse = - // new FlatSetElementNode(cmdLineArgs, - // index, - // anArg - // ); + FlatSetElementNode fse = + new FlatSetElementNode(cmdLineArgs, + index, + anArg + ); + + TypeDescriptor typeSize = new TypeDescriptor(TypeDescriptor.INT); + TempDescriptor sizeBytes = + new TempDescriptor("analysisEntryTemp_size", + typeSize + ); + FlatLiteralNode fls = + new FlatLiteralNode(typeSize, + new Integer( 1 ), + sizeBytes + ); + + TypeDescriptor typeBytes = + new TypeDescriptor(TypeDescriptor.CHAR).makeArray( state ); + TempDescriptor strBytes = + new TempDescriptor("analysisEntryTemp_strBytes", + typeBytes + ); + FlatNew fnBytes = + new FlatNew(typeBytes, + strBytes, + //sizeBytes, + false // is global + ); + this.constructedCmdLineArgBytesNew = fnBytes; + + ClassDescriptor cdString = argType.getClassDesc(); + assert cdString != null; + FieldDescriptor argBytes = null; + Iterator sFieldsItr = cdString.getFields(); + while( sFieldsItr.hasNext() ) { + FieldDescriptor fd = (FieldDescriptor) sFieldsItr.next(); + if( fd.getSymbol().equals( typeUtil.StringClassValueField ) ) { + argBytes = fd; + break; + } + } + assert argBytes != null; + FlatSetFieldNode fsf = + new FlatSetFieldNode(anArg, + argBytes, + strBytes + ); + // throw this in so you can always see what the initial heap context + // looks like if you want to, its cheap + FlatGenReachNode fgen = new FlatGenReachNode( "argContext" ); TempDescriptor[] sourceEntryArgs = new TempDescriptor[1]; sourceEntryArgs[0] = cmdLineArgs; - FlatCall fc = new FlatCall(mdSourceEntry, null, // dst temp @@ -2060,10 +2107,35 @@ public class DisjointAnalysis implements HeapAnalysis { fe ); - this.fmAnalysisEntry.addNext(fnArgs); - fnArgs.addNext(fc); - fc.addNext(frn); - frn.addNext(fe); + List nodes = new LinkedList(); + nodes.add( fnArgs ); + nodes.add( fnArg ); + nodes.add( fli ); + nodes.add( fse ); + nodes.add( fls ); + nodes.add( fnBytes ); + nodes.add( fsf ); + nodes.add( fgen ); + nodes.add( fc ); + nodes.add( frn ); + nodes.add( fe ); + + FlatNode current = this.fmAnalysisEntry; + for( FlatNode next: nodes ) { + current.addNext( next ); + current = next; + } + + + // jjenista - this is useful for looking at the FlatIRGraph of the + // analysis entry method constructed above if you have to modify it. + // The usual method of writing FlatIRGraphs out doesn't work because + // this flat method is private to the model of this analysis only. + //try { + // FlatIRGraph flatMethodWriter = + // new FlatIRGraph( state, false, false, false ); + // flatMethodWriter.writeFlatIRGraph( fmAnalysisEntry, "analysisEntry" ); + //} catch( IOException e ) {} } diff --git a/Robust/src/Analysis/Disjoint/HeapAnalysis.java b/Robust/src/Analysis/Disjoint/HeapAnalysis.java index 1228c9c6..ce041e8f 100644 --- a/Robust/src/Analysis/Disjoint/HeapAnalysis.java +++ b/Robust/src/Analysis/Disjoint/HeapAnalysis.java @@ -11,7 +11,18 @@ import IR.Flat.FlatNew; public interface HeapAnalysis { public EffectsAnalysis getEffectsAnalysis(); public Alloc getAllocationSiteFromFlatNew(FlatNew node); - public Alloc getCmdLineArgsAlloc(); + + // what are these for? Well, if your heap analysis wants to model + // the command line argument heap as the initial context, AND you are + // assigning IDs to allocation sites, the problem is there is no explicit + // allocation site for the command line arguments in the source code. So + // what you do is build your model and when these methods are invoked, return + // the alloc ID from your model. So the structure is an array of Strings has + // elements that reference a single String, and that String has a field that + // references an array of char primitives. + public Alloc getCmdLineArgsAlloc(); // an array of String + public Alloc getCmdLineArgAlloc(); // a String + public Alloc getCmdLineArgBytesAlloc();// an array of char // Use these methods to find out what allocation sites // the given pointer might point to at or after the diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index ca2616e0..2e16ad1f 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -5234,11 +5234,10 @@ public class ReachGraph { VariableNode vn = getVariableNodeNoMutation( x ); if( vn == null ) { - // the empty set means "can't point to anything" + // the empty table means "x can't point to anything" return out; } - Iterator edgeItr = vn.iteratorToReferencees(); while( edgeItr.hasNext() ) { HeapRegionNode hrn = edgeItr.next().getDst(); diff --git a/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java b/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java index 7211dd99..bd39fa6f 100644 --- a/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java +++ b/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java @@ -45,8 +45,8 @@ public class FlatIRGraph { } } } - - private void writeFlatIRGraph(FlatMethod fm, String graphname) throws java.io.IOException { + + public void writeFlatIRGraph(FlatMethod fm, String graphname) throws java.io.IOException { // give every node in the flat IR graph a unique label // so a human being can inspect the graph and verify // correctness diff --git a/Robust/src/Analysis/Pointer/Pointer.java b/Robust/src/Analysis/Pointer/Pointer.java index 447d321e..efaf3fe8 100644 --- a/Robust/src/Analysis/Pointer/Pointer.java +++ b/Robust/src/Analysis/Pointer/Pointer.java @@ -2099,7 +2099,12 @@ nextdelta: public Alloc getCmdLineArgsAlloc() { return null; } - + public Alloc getCmdLineArgAlloc() { + return null; + } + public Alloc getCmdLineArgBytesAlloc() { + return null; + } public Set canPointToAt( TempDescriptor x, diff --git a/Robust/src/IR/Flat/BCXPointsToCheckVRuntime.java b/Robust/src/IR/Flat/BCXPointsToCheckVRuntime.java index 9cfca997..1aa948b1 100644 --- a/Robust/src/IR/Flat/BCXPointsToCheckVRuntime.java +++ b/Robust/src/IR/Flat/BCXPointsToCheckVRuntime.java @@ -27,8 +27,8 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { } - public void additionalIncludesMethodsHeader(PrintWriter outmethodheader) { - outmethodheader.println("#include \"assert.h\""); + public void additionalIncludesMethodsHeader(PrintWriter outmethodheader) { + outmethodheader.println( "#include" ); } @@ -118,6 +118,12 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { lhs, heapAnalysis.canPointToAt( lhs, fn ) ); + + genAssertRuntimePtrVsHeapResults( output, + fm, + rhs, + heapAnalysis.canPointToAt( rhs, fn ) + ); genAssertRuntimePtrVsHeapResults( output, fm, @@ -143,6 +149,12 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { lhs, heapAnalysis.canPointToAt( lhs, fn ) ); + + genAssertRuntimePtrVsHeapResults( output, + fm, + rhs, + heapAnalysis.canPointToAt( rhs, fn ) + ); genAssertRuntimePtrVsHeapResults( output, fm, @@ -183,6 +195,16 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { + protected void + printConditionFailed( PrintWriter output, + String condition ) { + output.println( "printf(\"[[[ CHECK VS HEAP RESULTS FAILED ]]] Condition for failure( "+ + condition+" ) at %s:%d\\n\", __FILE__, __LINE__ );" ); + } + + + + protected void genAssertRuntimePtrVsHeapResults( PrintWriter output, FlatMethod context, @@ -193,7 +215,7 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { output.println( "" ); - output.println( "// asserts vs. heap results (DEBUG)" ); + output.println( "// checks vs. heap results (DEBUG) for "+x ); if( targetsByAnalysis == HeapAnalysis.DONTCARE_PTR ) { @@ -201,31 +223,36 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { return; } + + String condition; if( targetsByAnalysis.isEmpty() ) { - output.println( "assert( "+ - buildCode.generateTemp( context, x )+ - " == NULL );\n" ); + condition = + buildCode.generateTemp( context, x )+ + " != NULL"; } else { - output.print( "assert( "+ - buildCode.generateTemp( context, x )+ - " == NULL || " ); - + condition = + buildCode.generateTemp( context, x )+ + " != NULL &&"; + Iterator aItr = targetsByAnalysis.iterator(); while( aItr.hasNext() ) { Alloc a = aItr.next(); - output.print( buildCode.generateTemp( context, x )+ - "->allocsite == "+ - a.getUniqueAllocSiteID() - ); + condition += + buildCode.generateTemp( context, x )+ + "->allocsite != "+ + a.getUniqueAllocSiteID(); + if( aItr.hasNext() ) { - output.print( " || " ); + condition += " &&"; } - } - - output.println( " );\n" ); + } } + + output.println( "if( "+condition+" ) {" ); + printConditionFailed( output, condition ); + output.println( "}\n" ); } @@ -237,11 +264,19 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { FieldDescriptor f, // this null OR TempDescriptor i, // this null Hashtable< Alloc, Set > targetsByAnalysis ) { + // I assume when you invoke this method you already + // invoked a check on just what x points to, don't duplicate + // AND assume the check to x passed + assert targetsByAnalysis != null; assert f == null || i == null; - - output.println( "// asserts vs. heap results (DEBUG)" ); + + if( f != null ) { + output.println( "// checks vs. heap results (DEBUG) for "+x+"."+f ); + } else { + output.println( "// checks vs. heap results (DEBUG) for "+x+"["+i+"]" ); + } if( targetsByAnalysis == HeapAnalysis.DONTCARE_DREF ) { @@ -251,12 +286,11 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { if( targetsByAnalysis.isEmpty() ) { - output.println( "assert( "+ - buildCode.generateTemp( context, x )+ - " == NULL );\n" ); + output.println( "// Should have already checked "+x+" is NULL" ); + } else { output.println( "{" ); - + // if the ptr is null, that's ok, if not check allocsite output.println( "if( "+ buildCode.generateTemp( context, x )+ @@ -277,9 +311,9 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { "(((void*) &("+buildCode.generateTemp( context, x )+"->___length___))+sizeof(int)))"+ "["+buildCode.generateTemp( context, i )+"];" ); } - + output.println( "if( objOneHop != NULL ) { allocsiteOneHop = objOneHop->allocsite; }" ); - + output.println( "switch( "+ buildCode.generateTemp( context, x )+ "->allocsite ) {" ); @@ -295,33 +329,39 @@ public class BCXPointsToCheckVRuntime implements BuildCodeExtension { Set hopTargets = targetsByAnalysis.get( k ); if( hopTargets == HeapAnalysis.DONTCARE_PTR ) { output.print( "/* ANALYSIS DOESN'T CARE */" ); - + } else { - output.print( "assert( allocsiteOneHop == -1" ); - + String condition = "allocsiteOneHop != -1"; + if( !hopTargets.isEmpty() ) { - output.print( " || " ); + condition += " && "; } - + Iterator aItr = hopTargets.iterator(); while( aItr.hasNext() ) { Alloc a = aItr.next(); - output.print( "allocsiteOneHop == "+ - a.getUniqueAllocSiteID() ); + condition += + "allocsiteOneHop != "+ + a.getUniqueAllocSiteID(); if( aItr.hasNext() ) { - output.print( " || " ); + condition += " && "; } } - - output.print( " );" ); + + output.println( "if( "+condition+" ) {" ); + printConditionFailed( output, condition ); + output.println( "}" ); } - - output.println( " break;" ); + + output.println( "break;" ); } - - output.println( " default: assert( 0 ); break;" ); + + output.println( "default:" ); + output.println( "// the previous condition for "+x+ + " should already report this failure point" ); + output.println( "break;" ); output.println( "}" ); output.println( "}" ); output.println( "}\n" ); diff --git a/Robust/src/IR/Flat/BCXallocsiteObjectField.java b/Robust/src/IR/Flat/BCXallocsiteObjectField.java index 230b20a7..096de3ec 100644 --- a/Robust/src/IR/Flat/BCXallocsiteObjectField.java +++ b/Robust/src/IR/Flat/BCXallocsiteObjectField.java @@ -17,12 +17,15 @@ import java.util.*; public class BCXallocsiteObjectField implements BuildCodeExtension { protected BuildCode buildCode; + protected TypeUtil typeUtil; protected HeapAnalysis heapAnalysis; public BCXallocsiteObjectField( BuildCode buildCode, + TypeUtil typeUtil, HeapAnalysis heapAnalysis ) { this.buildCode = buildCode; + this.typeUtil = typeUtil; this.heapAnalysis = heapAnalysis; } @@ -32,10 +35,44 @@ public class BCXallocsiteObjectField implements BuildCodeExtension { } public void additionalCodeForCommandLineArgs(PrintWriter outmethod, String argsVar) { + + ClassDescriptor cdString = typeUtil.getClass( typeUtil.StringClass ); + assert cdString != null; + + FieldDescriptor argBytes = null; + Iterator sFieldsItr = cdString.getFields(); + while( sFieldsItr.hasNext() ) { + FieldDescriptor fd = (FieldDescriptor) sFieldsItr.next(); + if( fd.getSymbol().equals( typeUtil.StringClassValueField ) ) { + argBytes = fd; + break; + } + } + assert argBytes != null; + + String argsAccess = "((struct "+cdString.getSafeSymbol()+ + " **)(((char *)& "+argsVar+"->___length___)+sizeof(int)))"; + outmethod.println(argsVar+"->allocsite = "+ heapAnalysis.getCmdLineArgsAlloc().getUniqueAllocSiteID()+ ";" ); + outmethod.println("{"); + outmethod.println(" int i;" ); + outmethod.println(" for( i = 0; i < "+argsVar+"->___length___; ++i ) {"); + outmethod.println(" "+argsAccess+"[i]->allocsite = "+ + heapAnalysis.getCmdLineArgAlloc().getUniqueAllocSiteID()+ + ";" + ); + outmethod.println(" "+argsAccess+"[i]->"+ + argBytes.getSafeSymbol()+ + "->allocsite = "+ + heapAnalysis.getCmdLineArgBytesAlloc().getUniqueAllocSiteID()+ + ";" + ); + outmethod.println(" }"); + outmethod.println("}"); + outmethod.println(""); } public void additionalCodeNewObject(PrintWriter outmethod, String dstVar, FlatNew flatNew) { diff --git a/Robust/src/IR/Flat/BuildCode.java b/Robust/src/IR/Flat/BuildCode.java index 94c78da9..6544c721 100644 --- a/Robust/src/IR/Flat/BuildCode.java +++ b/Robust/src/IR/Flat/BuildCode.java @@ -42,7 +42,7 @@ public class BuildCode { public static String arraytype="ArrayObject"; public static int flagcount = 0; Virtual virtualcalls; - TypeUtil typeutil; + public TypeUtil typeutil; protected int maxtaskparams=0; protected int maxcount=0; ClassDescriptor[] cdarray; diff --git a/Robust/src/IR/TypeUtil.java b/Robust/src/IR/TypeUtil.java index 81704720..2921e1e5 100644 --- a/Robust/src/IR/TypeUtil.java +++ b/Robust/src/IR/TypeUtil.java @@ -8,6 +8,7 @@ import Main.Main; public class TypeUtil { public static String StringClass; + public static String StringClassValueField; public static String ObjectClass; public static String StartupClass; public static String TagClass; @@ -26,6 +27,7 @@ public class TypeUtil { this.bir=bir; if (state.JNI) { StringClass="java.lang.String"; + StringClassValueField="value"; ObjectClass="java.lang.Object"; StartupClass="StartupObject"; TagClass="TagDescriptor"; @@ -33,6 +35,7 @@ public class TypeUtil { TaskClass="Task"; } else { StringClass="String"; + StringClassValueField="value"; ObjectClass="Object"; StartupClass="StartupObject"; TagClass="TagDescriptor"; diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java index cfdbe051..63e5888b 100644 --- a/Robust/src/Main/Main.java +++ b/Robust/src/Main/Main.java @@ -672,7 +672,7 @@ public class Main { heapAnalysis != null ) { // use this extension to generate the allocsite field of Object and // ArrayObject for whatever other extensions and systems need it - BCXallocsiteObjectField bcx = new BCXallocsiteObjectField( bc, heapAnalysis ); + BCXallocsiteObjectField bcx = new BCXallocsiteObjectField( bc, tu, heapAnalysis ); bc.registerExtension( bcx ); }