@@ -31,6 +31,11 @@ namespace whyr {
3131 } else if (type->isArrayTy ()) {
3232 info.
arrayTypes .
insert (cast<ArrayType>(type));
3333 getTypeInfo (info, type->getArrayElementType ());
34+ } else if (type->isStructTy ()) {
35+ info.structTypes .insert (cast<StructType>(type));
36+ for (unsigned i = 0 ; i < type->getStructNumElements (); i++) {
37+ getTypeInfo (info, type->getStructElementType (i));
38+ }
3439 } else if (type->isVoidTy () || type->isLabelTy ()) {
3540 // do nothing
3641 } else {
@@ -265,6 +270,17 @@ namespace whyr {
265270 return " Double"
266271 } else if (type->isArrayTy ()) {
267272 return " Array" getWhy3TheoryName (type->getArrayElementType ()) + " _" to_string (type->getArrayNumElements ());
273+ } else if (type->isStructTy ()) {
274+ if (type->getStructName ().empty ()) {
275+ ostringstream name;
276+ name << " Struct"
277+ for (unsigned i = 0 ; i < type->getStructNumElements (); i++) {
278+ name << " _" getWhy3TheoryName (type->getStructElementType (i));
279+ }
280+ return name.str ();
281+ } else {
282+ return " Type_" getWhy3SafeName (string (type->getStructName ().data ()));
283+ }
268284 } else {
269285 throw llvm_exception (" Unknown type in LLVM input"
270286 }
@@ -281,6 +297,17 @@ namespace whyr {
281297 return " double"
282298 } else if (type->isArrayTy ()) {
283299 return " a" getWhy3TypeName (type->getArrayElementType ()) + " _" to_string (type->getArrayNumElements ());
300+ } else if (type->isStructTy ()) {
301+ if (type->getStructName ().empty ()) {
302+ ostringstream name;
303+ name << " struct"
304+ for (unsigned i = 0 ; i < type->getStructNumElements (); i++) {
305+ name << " _" getWhy3TypeName (type->getStructElementType (i));
306+ }
307+ return name.str ();
308+ } else {
309+ return " type_" getWhy3SafeName (string (type->getStructName ().data ()));
310+ }
284311 } else {
285312 throw llvm_exception (" Unknown type in LLVM input"
286313 }
@@ -370,6 +397,10 @@ namespace whyr {
370397 return string (" global_" getWhy3SafeName (global->getName ().data ());
371398 }
372399
400+ string getWhy3StructFieldName (AnnotatedModule* module , StructType* type, unsigned index) {
401+ return getWhy3TypeName (type) + " _field_" to_string (index);
402+ }
403+
373404 // ABOUT CustomTruncate BELOW:
374405 // There is a bug in Alt-Ergo that causes all proofs to run forever when Why3's real.Truncate theory is imported.
375406 // We add a custom truncation theory that is more limited than Why3's. This reduces the impact of the bug, but does not eliminate it.
424455 for (unordered_set<ArrayType*>::iterator ii = data.
info ->
arrayTypes .
begin (); ii != data.
info ->
arrayTypes .
end (); ii++) {
425456 out << " use import " getWhy3TheoryName (*ii) << endl;
426457 }
458+ for (unordered_set<StructType*>::iterator ii = data.info ->structTypes .begin (); ii != data.info ->structTypes .end (); ii++) {
459+ out << " use import " getWhy3TheoryName (*ii) << endl;
460+ }
427461 if (data.info ->usesAlloc ) {
428462 out << " use import Alloc"
429463 }
507541 addOperand (out, module , cc->getElementAsConstant (i), func);
508542 out << " ]"
509543 }
544+ } else if (isa<ConstantStruct>(operand)) {
545+ ConstantStruct* cc = cast<ConstantStruct>(operand);
546+ out << " { "
547+ for (unsigned i = 0 ; i < operand->getType ()->getStructNumElements (); i++) {
548+ out << getWhy3TheoryName (operand->getType ()) << " ." getWhy3StructFieldName (module , cc->getType (), i) << " = "
549+ addOperand (out, module , cc->getAggregateElement (i));
550+ out << " ; "
551+ }
552+ out << " }"
510553 } else if (isa<ConstantAggregateZero>(operand)) {
511554 if (operand->getType ()->isArrayTy ()) {
512555 Constant* value = cast<ConstantAggregateZero>(operand)->getSequentialElement ();
517560 addOperand (out, module , value, func);
518561 out << " ]"
519562 }
563+ } else if (operand->getType ()->isStructTy ()) {
564+ ConstantAggregateZero* cc = cast<ConstantAggregateZero>(operand);
565+ out << " { "
566+ for (unsigned i = 0 ; i < operand->getType ()->getStructNumElements (); i++) {
567+ out << getWhy3TheoryName (operand->getType ()) << " ." getWhy3StructFieldName (module , cast<StructType>(operand->getType ()), i) << " = "
568+ addOperand (out, module , cc->getStructElement (i));
569+ out << " ; "
570+ }
571+ out << " }"
520572 } else {
521573 throw type_exception (" Instantiation of aggregate zero of type '" LogicTypeLLVM (operand->getType ()).toString () + " ' currently unsupported"
522574 }
945997 addOperand (out, func->getModule (), ii->get (), func);
946998 out << " ))"
947999 currentType = currentType->getArrayElementType ();
1000+ } else if (currentType->isStructTy ()) {
1001+ unsigned index = cast<ConstantInt>(ii->get ())->getLimitedValue ();
1002+ unsigned offset = func->getModule ()->rawIR ()->getDataLayout ().getStructLayout (cast<StructType>(currentType))->getElementOffsetInBits (index);
1003+ out << offset;
1004+ currentType = currentType->getStructElementType (index);
9481005 }
9491006 }
9501007 out << " )))"
@@ -956,8 +1013,15 @@ end
9561013 addOperand (out, func->getModule (), inst, func);
9571014 out << " = "
9581015 addOperand (out, func->getModule (), exInst->getAggregateOperand (), func);
1016+ Type* operandType = exInst->getAggregateOperand ()->getType ();
9591017 for (ExtractValueInst::idx_iterator ii = exInst->idx_begin (); ii != exInst->idx_end (); ii++) {
960- out << " [" " ]"
1018+ if (operandType->isArrayTy ()) {
1019+ out << " [" " ]"
1020+ operandType = operandType->getArrayElementType ();
1021+ } else if (operandType->isStructTy ()) {
1022+ out << " ." getWhy3StructFieldName (func->getModule (), cast<StructType>(operandType), *ii);
1023+ operandType = operandType->getStructElementType (*ii);
1024+ }
9611025 }
9621026 break ;
9631027 }
@@ -967,19 +1031,48 @@ end
9671031 addOperand (out, func->getModule (), inst, func);
9681032 out << " = "
9691033
970- int i = 0 ;
1034+ int i = 0 ; Type* operandType = insInst-> getAggregateOperand ()-> getType ();
9711035 for (InsertValueInst::idx_iterator ii = insInst->idx_begin (); ii != insInst->idx_end (); ii++) {
972- addOperand (out, func->getModule (), insInst->getAggregateOperand (), func);
973- for (int j = 0 ; j < i; j++) {
1036+ if (operandType->isStructTy ()) {
1037+ out << " {"
1038+ }
1039+ addOperand (out, func->getModule (), insInst->getAggregateOperand (), func);
1040+
1041+ Type* operandType2 = insInst->getAggregateOperand ()->getType ();
1042+ for (int j = 0 ; j < i; j++) {
1043+ if (operandType2->isArrayTy ()) {
9741044 out << " [" idx_begin ()+j) << " ]"
1045+ operandType2 = operandType2->getArrayElementType ();
1046+ } else if (operandType2->isStructTy ()) {
1047+ out << " ." getWhy3StructFieldName (func->getModule (), cast<StructType>(operandType2), *(insInst->idx_begin ()+j));
1048+ operandType2 = operandType2->getStructElementType (*(insInst->idx_begin ()+j));
9751049 }
1050+ }
1051+
1052+ if (operandType->isArrayTy ()) {
9761053 out << " [" " <- "
1054+ operandType = operandType->getArrayElementType ();
1055+ } else if (operandType->isStructTy ()) {
1056+ out << " with " getWhy3TheoryName (operandType) << " ." getWhy3StructFieldName (func->getModule (), cast<StructType>(operandType), *ii) << " = "
1057+ operandType = operandType->getStructElementType (*ii);
1058+ }
1059+
9771060 i++;
9781061 }
1062+
1063+ Type* operandType3 = insInst->getAggregateOperand ()->getType ();
9791064 addOperand (out, func->getModule (), insInst->getInsertedValueOperand (), func);
1065+ string ending;
9801066 for (int j = 0 ; j < i; j++) {
981- out << " ]"
1067+ if (operandType3->isArrayTy ()) {
1068+ ending = " ]"
1069+ operandType3 = operandType3->getArrayElementType ();
1070+ } else if (operandType3->isStructTy ()) {
1071+ ending = " ;}"
1072+ operandType3 = operandType3->getStructElementType (*(insInst->idx_begin ()+j));
1073+ }
9821074 }
1075+ out << ending;
9831076 break ;
9841077 }
9851078 case Instruction::OtherOps::ICmp: {
@@ -1786,11 +1879,39 @@ end
17861879 out << " end"
17871880 }
17881881
1882+ void addCommonStructType (ostream &out, AnnotatedModule* module ) {
1883+ // do nothing. Currently, no memory models require we have any common code.
1884+ }
1885+
1886+ void addStructType (ostream &out, AnnotatedModule* module , StructType* type) {
1887+ // find the imports we need
1888+ unordered_set<Type*> imports;
1889+ for (unsigned i = 0 ; i < type->getStructNumElements (); i++) {
1890+ imports.insert (type->getStructElementType (i));
1891+ }
1892+
1893+ // add the theory
1894+ out << " theory " getWhy3TheoryName (type) << endl;
1895+ for (unordered_set<Type*>::iterator ii = imports.begin (); ii != imports.end (); ii++) {
1896+ out << " use import " getWhy3TheoryName (*ii) << endl;
1897+ }
1898+ out << " constant size : int = " module ->rawIR ()->getDataLayout ().getStructLayout (type)->getSizeInBits () << endl;
1899+ out << " type " getWhy3TypeName (type) << " = {"
1900+ for (unsigned i = 0 ; i < type->getStructNumElements (); i++) {
1901+ Type* elem = type->getStructElementType (i);
1902+ out << " " getWhy3StructFieldName (module , type, i) << " : " getWhy3FullName (elem) << " ;"
1903+ }
1904+ out << " }"
1905+ out << " end"
1906+ }
1907+
17891908 void addDerivedType (ostream &out, AnnotatedModule* module , Type* type) {
17901909 if (type->isPointerTy ()) {
17911910 addPtrType (out,
module , cast<PointerType>(type));
17921911 } else if (type->isArrayTy ()) {
17931912 addArrayType (out,
module , cast<ArrayType>(type));
1913+ } else if (type->isStructTy ()) {
1914+ addStructType (out, module , cast<StructType>(type));
17941915 }
17951916 }
17961917
@@ -1987,6 +2108,7 @@ end
19872108 unordered_set<Type*> notSeen;
19882109 notSeen.insert (info.ptrTypes .begin (), info.ptrTypes .end ());
19892110 notSeen.insert (info.arrayTypes .begin (), info.arrayTypes .end ());
2111+ notSeen.insert (info.structTypes .begin (), info.structTypes .end ());
19902112
19912113 // while there's still more nodes in need of calculation; that is, if the state changed since last iteration...
19922114 bool changed;
@@ -2006,6 +2128,13 @@ end
20062128 if (notSeen.find ((*ii)->getArrayElementType ()) != notSeen.end ()) {
20072129 allSeen = false ;
20082130 }
2131+ } else if ((*ii)->isStructTy ()) {
2132+ for (unsigned i = 0 ; i < (*ii)->getStructNumElements (); i++) {
2133+ if (notSeen.find ((*ii)->getStructElementType (i)) != notSeen.end ()) {
2134+ allSeen = false ;
2135+ break ;
2136+ }
2137+ }
20092138 }
20102139
20112140 if (allSeen) {
@@ -2135,6 +2264,10 @@ end
21352264 addCommonArrayType (out, module );
21362265 }
21372266
2267+ if (!info.structTypes .empty ()) {
2268+ addCommonStructType (out, module );
2269+ }
2270+
21382271 list<Type*> types;
21392272 getCorrectDerivedTypeOrder (types, info, module );
21402273
0 commit comments