From 01a7df74a55c10ca3181241ccabec30e2c218add Mon Sep 17 00:00:00 2001 From: yeom Date: Tue, 26 Jul 2011 08:15:17 +0000 Subject: [PATCH] changes. --- Robust/src/Analysis/SSJava/FlowDownCheck.java | 147 +++- .../ssJava/mp3decoder/LayerIIIDecoder.java | 635 ++++++++++-------- 2 files changed, 485 insertions(+), 297 deletions(-) diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 89afe624..2a0b8a7a 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -537,7 +537,8 @@ public class FlowDownCheck { Set inputGLB = new HashSet(); inputGLB.add(returnValueLoc); inputGLB.add(constraint); - returnValueLoc = CompositeLattice.calculateGLB(inputGLB); + returnValueLoc = + CompositeLattice.calculateGLB(inputGLB, generateErrorMessage(md.getClassDesc(), rn)); } // check if return value is equal or higher than RETRUNLOC of method @@ -621,7 +622,7 @@ public class FlowDownCheck { Set inputSet = new HashSet(); inputSet.add(currentCon); inputSet.add(newCon); - return CompositeLattice.calculateGLB(inputSet); + return CompositeLattice.calculateGLB(inputSet, ""); } } @@ -818,7 +819,7 @@ public class FlowDownCheck { glbInputSet.add(trueLoc); glbInputSet.add(falseLoc); - return CompositeLattice.calculateGLB(glbInputSet); + return CompositeLattice.calculateGLB(glbInputSet, generateErrorMessage(cd, tn)); } private CompositeLocation checkLocationFromMethodInvokeNode(MethodDescriptor md, @@ -954,7 +955,7 @@ public class FlowDownCheck { Set inputGLB = new HashSet(); inputGLB.add(arrayLoc); inputGLB.add(indexLoc); - return CompositeLattice.calculateGLB(inputGLB); + return CompositeLattice.calculateGLB(inputGLB, generateErrorMessage(cd, aan)); } } @@ -1027,7 +1028,9 @@ public class FlowDownCheck { Set inputSet = new HashSet(); inputSet.add(leftLoc); inputSet.add(rightLoc); - CompositeLocation glbCompLoc = CompositeLattice.calculateGLB(inputSet); + CompositeLocation glbCompLoc = + CompositeLattice.calculateGLB(inputSet, generateErrorMessage(cd, on)); + System.out.println("# glbCompLoc=" + glbCompLoc); return glbCompLoc; default: @@ -1212,7 +1215,7 @@ public class FlowDownCheck { if (constraint != null) { inputGLBSet.add(rhsLocation); inputGLBSet.add(constraint); - srcLocation = CompositeLattice.calculateGLB(inputGLBSet); + srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an)); } else { srcLocation = rhsLocation; } @@ -1232,11 +1235,15 @@ public class FlowDownCheck { if (constraint != null) { inputGLBSet.add(rhsLocation); inputGLBSet.add(constraint); - srcLocation = CompositeLattice.calculateGLB(inputGLBSet); + srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an)); } else { srcLocation = rhsLocation; } + System.out.println("srcLocation=" + srcLocation); + System.out.println("rhsLocation=" + rhsLocation); + System.out.println("constraint=" + constraint); + if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) { throw new Error("Location " + destLocation + " is not allowed to have the value flow that moves within the same location at " @@ -1358,7 +1365,7 @@ public class FlowDownCheck { SSJavaLattice localLattice = CompositeLattice.getLatticeByDescriptor(md); Location localLoc = new Location(md, localLocId); if (localLattice == null || (!localLattice.containsKey(localLocId))) { - System.out.println("locDec="+locDec); + System.out.println("locDec=" + locDec); throw new Error("Location " + localLocId + " is not defined in the local variable lattice at " + md.getClassDesc().getSourceFileName() + "::" + (n != null ? n.getNumLine() : md) + "."); @@ -1650,9 +1657,9 @@ public class FlowDownCheck { } - public static CompositeLocation calculateGLB(Set inputSet) { + public static CompositeLocation calculateGLB(Set inputSet, String errMsg) { - // System.out.println("Calculating GLB=" + inputSet); + System.out.println("Calculating GLB=" + inputSet); CompositeLocation glbCompLoc = new CompositeLocation(); // calculate GLB of the first(priority) element @@ -1667,6 +1674,7 @@ public class FlowDownCheck { int maxTupleSize = 0; CompositeLocation maxCompLoc = null; + Location prevPriorityLoc = null; for (Iterator iterator = inputSet.iterator(); iterator.hasNext();) { CompositeLocation compLoc = (CompositeLocation) iterator.next(); if (compLoc.getSize() > maxTupleSize) { @@ -1688,10 +1696,14 @@ public class FlowDownCheck { // check if priority location are coming from the same lattice if (priorityDescriptor == null) { priorityDescriptor = priorityLoc.getDescriptor(); - } else if (!priorityDescriptor.equals(priorityLoc.getDescriptor())) { - throw new Error("Failed to calculate GLB of " + inputSet - + " because they are from different lattices."); + } else { + priorityDescriptor = getCommonParentDescriptor(priorityLoc, prevPriorityLoc, errMsg); } + prevPriorityLoc = priorityLoc; + // else if (!priorityDescriptor.equals(priorityLoc.getDescriptor())) { + // throw new Error("Failed to calculate GLB of " + inputSet + // + " because they are from different lattices."); + // } } SSJavaLattice locOrder = getLatticeByDescriptor(priorityDescriptor); @@ -1726,7 +1738,6 @@ public class FlowDownCheck { } if (compSet.size() == 1) { - // if GLB(x1,x2)==x1 or x2 : GLB case 2,3 CompositeLocation comp = compSet.iterator().next(); for (int i = 1; i < comp.getSize(); i++) { @@ -1744,26 +1755,24 @@ public class FlowDownCheck { // if more than one location shares the same priority GLB // need to calculate the rest of GLB loc - // int compositeLocSize = compSet.iterator().next().getSize(); - int compositeLocSize = maxFromCompSet.getSize(); - - Set glbInputSet = new HashSet(); - Descriptor currentD = null; - for (int i = 1; i < compositeLocSize; i++) { - for (Iterator iterator = compSet.iterator(); iterator.hasNext();) { - CompositeLocation compositeLocation = (CompositeLocation) iterator.next(); - if (compositeLocation.getSize() > i) { - Location currentLoc = compositeLocation.get(i); - currentD = currentLoc.getDescriptor(); - // making set of the current location sharing the same idx - glbInputSet.add(currentLoc.getLocIdentifier()); - } + // setup input set starting from the second tuple item + Set innerGLBInput = new HashSet(); + for (Iterator iterator = compSet.iterator(); iterator.hasNext();) { + CompositeLocation compLoc = (CompositeLocation) iterator.next(); + CompositeLocation innerCompLoc = new CompositeLocation(); + for (int idx = 1; idx < compLoc.getSize(); idx++) { + innerCompLoc.addLocation(compLoc.get(idx)); + } + if (innerCompLoc.getSize() > 0) { + innerGLBInput.add(innerCompLoc); } - // calculate glb for the current lattice + } - SSJavaLattice currentLattice = getLatticeByDescriptor(currentD); - String currentGLBLocId = currentLattice.getGLB(glbInputSet); - glbCompLoc.addLocation(new Location(currentD, currentGLBLocId)); + if (innerGLBInput.size() > 0) { + CompositeLocation innerGLB = CompositeLattice.calculateGLB(innerGLBInput, errMsg); + for (int idx = 0; idx < innerGLB.getSize(); idx++) { + glbCompLoc.addLocation(innerGLB.get(idx)); + } } // if input location corresponding to glb is a delta, need to apply @@ -1782,6 +1791,7 @@ public class FlowDownCheck { } } + System.out.println("GLB=" + glbCompLoc); return glbCompLoc; } @@ -1804,6 +1814,77 @@ public class FlowDownCheck { return lattice; } + static Descriptor getCommonParentDescriptor(Location loc1, Location loc2, String msg) { + + Descriptor d1 = loc1.getDescriptor(); + Descriptor d2 = loc2.getDescriptor(); + + Descriptor descriptor; + + if (d1 instanceof ClassDescriptor && d2 instanceof ClassDescriptor) { + + if (d1.equals(d2)) { + descriptor = d1; + } else { + // identifying which one is parent class + Set d1SubClassesSet = ssjava.tu.getSubClasses((ClassDescriptor) d1); + Set d2SubClassesSet = ssjava.tu.getSubClasses((ClassDescriptor) d2); + + if (d1 == null && d2 == null) { + throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2 + + " because they are not comparable at " + msg); + } else if (d1SubClassesSet != null && d1SubClassesSet.contains(d2)) { + descriptor = d1; + } else if (d2SubClassesSet != null && d2SubClassesSet.contains(d1)) { + descriptor = d2; + } else { + throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2 + + " because they are not comparable at " + msg); + } + } + + } else if (d1 instanceof MethodDescriptor && d2 instanceof MethodDescriptor) { + + if (d1.equals(d2)) { + descriptor = d1; + } else { + + // identifying which one is parent class + MethodDescriptor md1 = (MethodDescriptor) d1; + MethodDescriptor md2 = (MethodDescriptor) d2; + + if (!md1.matches(md2)) { + throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2 + + " because they are not comparable at " + msg); + } + + Set d1SubClassesSet = + ssjava.tu.getSubClasses(((MethodDescriptor) d1).getClassDesc()); + Set d2SubClassesSet = + ssjava.tu.getSubClasses(((MethodDescriptor) d2).getClassDesc()); + + if (d1 == null && d2 == null) { + throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2 + + " because they are not comparable at " + msg); + } else if (d1 != null && d1SubClassesSet.contains(d2)) { + descriptor = d1; + } else if (d2 != null && d2SubClassesSet.contains(d1)) { + descriptor = d2; + } else { + throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2 + + " because they are not comparable at " + msg); + } + } + + } else { + throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2 + + " because they are not comparable at " + msg); + } + + return descriptor; + + } + } class ComparisonResult { @@ -1867,7 +1948,7 @@ class ReturnLocGenerator { // compute GLB of arguments subset that are same or higher than return // location - CompositeLocation glb = CompositeLattice.calculateGLB(inputGLB); + CompositeLocation glb = CompositeLattice.calculateGLB(inputGLB, ""); return glb; } } diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java index ff6d4a16..06179f85 100644 --- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java +++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java @@ -4,7 +4,7 @@ * 18/06/01 Michael Scheerer, Fixed bugs which causes * negative indexes in method huffmann_decode and in method * dequanisize_sample. - * + * * 16/07/01 Michael Scheerer, Catched a bug in method * huffmann_decode, which causes an outOfIndexException. * Cause : Indexnumber of 24 at SfBandIndex, @@ -32,66 +32,93 @@ *---------------------------------------------------------------------- */ - /** * Class Implementing Layer 3 Decoder. * * @since 0.0 */ -@LATTICE("FS>> 3; + for (i = 0; i < nSlots; i++) { + br.hputbuf(stream.get_bits(8)); + } + + main_data_end = br.hsstell() >>> 3; if ((flush_main = (br.hsstell() & 7)) != 0) { // flush_main < br br.hgetbits(8 - flush_main); // br < flush_main - main_data_end++; // main_data_end* + main_data_end++; // main_data_end* } // bytes_to_discard < GLB(frame_start,main_data_end,si) - // TODO does bytes_to_discard need to go back to si??? bytes_to_discard = frame_start - main_data_end - si.main_data_begin; // frame_start should be * frame_start += nSlots; - if (bytes_to_discard < 0) + if (bytes_to_discard < 0) { return; + } - if (main_data_end > 4096) { // main_data_end should be > than 'frame_start' and 'br' + if (main_data_end > 4096) { // main_data_end should be > than 'frame_start' + // and 'br' frame_start -= 4096; br.rewindNbytes(4096); } - for (; bytes_to_discard > 0; bytes_to_discard--) // bytes_to_discard > br + for (; bytes_to_discard > 0; bytes_to_discard--){ + // bytes_to_discard > br br.hgetbits(8); - + } + // doing something from here - + // here 'gr' and 'max_gr' should be higher than 'ch','channels', and more - for (gr = 0; gr < max_gr; gr++) { // two granules per channel - // in the loop body, access set={part2_start} - + for (gr = 0; gr < max_gr; gr++) { // two granules per channel + // in the loop body, access set={part2_start} + // 'ch', 'channels' should be higher than all locs in the below body - for (ch = 0; ch < channels; ch++) { + for (ch = 0; ch < channels; ch++) { part2_start = br.hsstell(); // part2_start < br - // grab scale factors from the main data. + // grab scale factors from the main data. // following the scale factors is the actual compressed data if (header.version() == Header.MPEG1) get_scale_factors(ch, gr); // no need to care from this side - // here move scale factor data from 'br' buffer to 'scalefac' field + // here move scale factor data from 'br' buffer to 'scalefac' field else // MPEG-2 LSF, SZD: MPEG-2.5 LSF get_LSF_scale_factors(ch, gr); // no need to care from this side - // here, decoding the compressed audio data + // here, decoding the compressed audio data huffman_decode(ch, gr); // no need to care from this side // System.out.println("CheckSum HuffMan = " + CheckSumHuff); dequantize_sample(ro[ch], ch, gr); // no need to care from this side @@ -336,16 +371,19 @@ final class LayerIIIDecoder implements FrameDecoder { stereo(gr); // no need to care from this side - if ((which_channels == OutputChannels.DOWNMIX_CHANNELS) && (channels > 1)) + if ((which_channels == OutputChannels.DOWNMIX_CHANNELS) && (channels > 1)) { do_downmix(); + } - for (ch = first_channel; ch <= last_channel; ch++) { // 'ch' and 'first_channel' > the body + for (ch = first_channel; ch <= last_channel; ch++) { // 'ch' and + // 'first_channel' > + // the body // in the body // read set= lr,ch,gr,out_1d, sb18, ss, SSLIMIT, out_1d // write set= out_1d - - reorder(lr[ch], ch, gr); + + reorder(lr[ch], ch, gr); antialias(ch, gr); // for (int hb = 0;hb<576;hb++) CheckSumOut1d = CheckSumOut1d + // out_1d[hb]; @@ -357,14 +395,18 @@ final class LayerIIIDecoder implements FrameDecoder { // out_1d[hb]; // System.out.println("CheckSumOut1d = "+CheckSumOut1d); - for (sb18 = 18; sb18 < 576; sb18 += 36) // sb18 > ss, SSLIMIT, out1d + for (sb18 = 18; sb18 < 576; sb18 += 36) { + // sb18 > ss, SSLIMIT, out1d // Frequency inversion - for (ss = 1; ss < SSLIMIT; ss += 2) // 'ss','SSLIMIT' > out_1d + for (ss = 1; ss < SSLIMIT; ss += 2) { + // 'ss','SSLIMIT' > out_1d out_1d[sb18 + ss] = -out_1d[sb18 + ss]; // out1d* + } + } // 'ch', 'which_channels' should be higher than if/else body! - // location set written by if/else body - // = {samples1, samples2, filter1, filter2} + // location set written by if/else body + // = {samples1, samples2, filter1, filter2} if ((ch == 0) || (which_channels == OutputChannels.RIGHT_CHANNEL)) { for (ss = 0; ss < SSLIMIT; ss++) { // Polyphase synthesis sb = 0; @@ -413,7 +455,7 @@ final class LayerIIIDecoder implements FrameDecoder { * Reads the side info from the stream, assuming the entire. frame has been * read already. Mono : 136 bits (= 17 bytes) Stereo : 256 bits (= 32 bytes) */ - @RETURNLOC("OUT") + @RETURNLOC("OUT") private boolean get_side_info() { @LOC("IN") int ch; @LOC("IN") int gr; @@ -640,8 +682,9 @@ final class LayerIIIDecoder implements FrameDecoder { */ // MDM: new_slen is fully initialized before use, no need // to reallocate array. - @LOC("NS") private final int[] new_slen = new int[4]; - + @LOC("NS") + private final int[] new_slen = new int[4]; + @LATTICE("THIS 0) @@ -1050,7 +1099,7 @@ final class LayerIIIDecoder implements FrameDecoder { * xr[sb][ss] *= pow(2.0, -0.5 * (1.0+gr_info.scalefac_scale) * (scalefac[ch].l[cb] + gr_info.preflag * pretab[cb])); */ - @LOC("IDX") int idx = scalefac[ch].l[cb]; + @LOC("IDX") int idx = scalefac[ch].l[cb]; if (gr_info.preflag != 0) idx += pretab[cb]; @@ -1080,12 +1129,14 @@ final class LayerIIIDecoder implements FrameDecoder { */ @LATTICE("THIS= 3; sfb--) { i = sfBandIndex[sfreq].s[sfb]; @@ -1320,8 +1376,8 @@ final class LayerIIIDecoder implements FrameDecoder { } // for (; sfb<8 ... } // for (j=0 ... } else { // if (gr_info.mixed_block_flag) - for (@LOC("THIS,LayerIIIDecoder.J") int j = 0; j < 3; j++) { - @LOC("THIS,LayerIIIDecoder.SH") int sfbcnt; + for (@LOC("THIS,LayerIIIDecoder.J") int j = 0; j < 3; j++) { + @LOC("THIS,LayerIIIDecoder.SH") int sfbcnt; sfbcnt = -1; for (sfb = 12; sfb >= 0; sfb--) { temp = sfBandIndex[sfreq].s[sfb]; @@ -1462,12 +1518,15 @@ final class LayerIIIDecoder implements FrameDecoder { /** * */ - @LATTICE("THIS