001package daikon.simplify; 002 003/** Utility functions for the simplify package. */ 004public class SimpUtil { 005 private SimpUtil() { 006 throw new Error("do not instantiate"); 007 } 008 009 public static void assert_well_formed(String s) { 010 boolean assert_enabled = false; 011 assert (assert_enabled = true); 012 if (!assert_enabled) { 013 return; 014 } 015 016 // Unfortunately, most of the tests here aren't sensible if the 017 // string can contain quoted strings (like |))|). To do this 018 // right, the paren counter would also have to be smarter about 019 // details like the rules for | delimiting strings, and how it can 020 // be escaped. 021 022 assert s != null; 023 // XXX not with strings 024 // if (s.indexOf("((") != -1) 025 // throw new Error("'((' may not appear, '" + s + "'"); 026 assert s.length() >= 4 : "too short, '" + s + "'"; 027 if (s.charAt(0) != '(') { 028 throw new Error("starts with lparen, '" + s + "'"); 029 } 030 if (s.charAt(s.length() - 1) != ')') { 031 throw new Error("ends with rparen, '" + s + "'"); 032 } 033 034 @SuppressWarnings("UnusedVariable") 035 int paren = 0; 036 char[] cs = s.toCharArray(); 037 for (int i = 0; i < cs.length; i++) { 038 char c = cs[i]; 039 if (c == '(') { 040 paren++; 041 } else if (c == ')') { 042 // XXX not with strings 043 // if (paren <= 0) 044 // assert paren > 0 : // "too deep at char " + i + " in '" + s + "'"; 045 paren--; 046 // This check is only sensible for some callers; it needs a flag. 047 // if (paren == 0 && i < cs.length -1) 048 // throw new Error("multiple SEXPs in " + s); 049 } 050 } 051 // XXX not with strings 052 // if (paren != 0) 053 // assert paren == 0 : "unbalanced parens in '" + s + "'"; 054 } 055 056 /** 057 * Represent a Java long integer as an uninterpreted function applied to 6 moderately sized 058 * integers, to work around Simplify's numeric limitations. The first integer is a sign, and the 059 * rest are 13-bit (base 8192) limbs in order from most to least significant. 060 */ 061 public static String formatInteger(long i) { 062 int sign; 063 int[] limbs = new int[5]; // limbs[0] is most significant 064 if (i == 0) { 065 sign = limbs[0] = limbs[1] = limbs[2] = limbs[3] = limbs[4] = 0; 066 } else if (i == Long.MIN_VALUE) { 067 sign = -1; 068 limbs[0] = 2048; 069 limbs[1] = limbs[2] = limbs[3] = limbs[4] = 0; 070 } else { 071 sign = 1; 072 if (i < 0) { 073 sign = -1; 074 i = -i; 075 } 076 for (int j = 4; j >= 0; j--) { 077 limbs[j] = (int) (i % 8192); 078 i /= 8192; 079 } 080 } 081 return "(|long-int| " 082 + sign 083 + " " 084 + limbs[0] 085 + " " 086 + limbs[1] 087 + " " 088 + limbs[2] 089 + " " 090 + limbs[3] 091 + " " 092 + limbs[4] 093 + ")"; 094 } 095}