diff --git a/examples/basic/struct.c b/examples/basic/struct.c new file mode 100644 index 0000000000..db8da2a633 --- /dev/null +++ b/examples/basic/struct.c @@ -0,0 +1,37 @@ +void test() { + int *x = NULL; +} + +struct A { + int x; + int y; +}; + +typedef struct A Adef, Adef2; + +typedef struct B { + int x; + int y; +} Bdef; + +typedef struct C { + int x; + int y; +} *Cpdef; + +typedef struct { + int x; + int y; +} Anondef; + + +/*@ context Perm(adef->x, write); +@*/ +void otherMethod(Adef *adef) { +} + +/*@ context Perm(adef->x, write); +@*/ +void method(struct A *a, Adef *adef, struct B *b, Bdef *bdef, struct C *c, Cpdef cpdef, Anondef *anondef) { + otherMethod(adef); +} \ No newline at end of file diff --git a/src/main/java/vct/antlr4/parser/ANTLRtoCOL.java b/src/main/java/vct/antlr4/parser/ANTLRtoCOL.java index 4906e61c1c..8700128f54 100644 --- a/src/main/java/vct/antlr4/parser/ANTLRtoCOL.java +++ b/src/main/java/vct/antlr4/parser/ANTLRtoCOL.java @@ -8,7 +8,6 @@ import hre.ast.FileOrigin; import hre.ast.Origin; -import hre.lang.Failure; import hre.lang.HREError; import org.antlr.v4.runtime.BufferedTokenStream; @@ -35,7 +34,7 @@ import vct.col.ast.type.PrimitiveSort; import vct.col.ast.expr.StandardOperator; import vct.col.ast.type.Type; -import vct.col.ast.stmt.decl.VariableDeclaration; +import vct.col.ast.stmt.decl.MultipleDeclaration; import vct.col.syntax.Syntax; import vct.col.util.ASTFactory; import static hre.lang.System.*; @@ -741,8 +740,8 @@ public Contract getContract(ParserRuleContext ctx){ decl.setGhost(true); if (decl instanceof DeclarationStatement){ cb.given((DeclarationStatement)decl); - } else if (decl instanceof VariableDeclaration){ - cb.given((VariableDeclaration)convert(clause,1)); + } else if (decl instanceof MultipleDeclaration){ + cb.given((MultipleDeclaration)convert(clause,1)); } } else if (match(clause,"given",null,null,";")){ DeclarationStatement decl=create.field_decl(getIdentifier(clause,2),checkType(convert(clause,1))); @@ -752,8 +751,8 @@ public Contract getContract(ParserRuleContext ctx){ ASTNode decl=convert(clause,1); if (decl instanceof DeclarationStatement){ cb.yields((DeclarationStatement)convert(clause,1)); - } else if (decl instanceof VariableDeclaration){ - cb.yields((VariableDeclaration)convert(clause,1)); + } else if (decl instanceof MultipleDeclaration){ + cb.yields((MultipleDeclaration)convert(clause,1)); } } else { throw hre.lang.System.Failure("bad clause %s",t); diff --git a/src/main/java/vct/antlr4/parser/CMLtoCOL.java b/src/main/java/vct/antlr4/parser/CMLtoCOL.java index 0be8d7f9e6..4a53516dfe 100644 --- a/src/main/java/vct/antlr4/parser/CMLtoCOL.java +++ b/src/main/java/vct/antlr4/parser/CMLtoCOL.java @@ -19,6 +19,7 @@ import vct.col.ast.stmt.decl.ASTSpecial.Kind; import vct.col.ast.type.PrimitiveSort; import vct.col.ast.type.Type; +import vct.col.ast.type.TypeExpression; import vct.col.ast.type.TypeOperator; import vct.col.syntax.CSyntax; import vct.col.syntax.Syntax; @@ -27,6 +28,7 @@ import java.util.ArrayList; +import static hre.lang.System.Abort; import static hre.lang.System.Debug; /** @@ -39,6 +41,11 @@ * @author Stefan Blom */ public class CMLtoCOL extends ANTLRtoCOL implements CMLVisitor { + /** + * Since regular declarations ("int x;") and typedefs ("typedef struct S{} name;") share the same grammatical structure, + * we need to remember whether a type ("typedef struct S{}") was marked as typedef, in addition to the type returned. + */ + private boolean flag_in_typedef = false; private static > E convert(E unit, ParseTree tree, String file_name, BufferedTokenStream tokens, org.antlr.v4.runtime.Parser parser) { ANTLRtoCOL visitor=new CMLtoCOL(unit, CSyntax.getCML(),file_name,tokens,parser,CMLLexer.Identifier,CMLLexer.CH_COMMENT); @@ -100,6 +107,21 @@ private void doblock(BlockStatement block, ParserRuleContext ctx) { } } + private Type addPointer(Type t) { + if(t instanceof TypeExpression) { + if(t.nrOfArguments() != 1) { + throw hre.lang.System.Failure("Cannot add indirection to a type-expression which has non-unary arity."); + } + + return create.type_expression( + ((TypeExpression) t).operator(), + addPointer(((TypeExpression) t).firstType()) + ); + } else { + return create.primitive_type(PrimitiveSort.Pointer, t); + } + } + private ASTDeclaration getPointer(ASTDeclaration decl, ParserRuleContext ctx){ if(match(ctx,"*",null)){ Debug("pointer"); @@ -114,7 +136,7 @@ private ASTDeclaration getPointer(ASTDeclaration decl, ParserRuleContext ctx){ if(decl instanceof DeclarationStatement) { DeclarationStatement result = new DeclarationStatement( decl.name(), - create.primitive_type(PrimitiveSort.Pointer, ((DeclarationStatement) decl).type()), + addPointer(((DeclarationStatement) decl).type()), ((DeclarationStatement) decl).init() ); @@ -124,13 +146,21 @@ private ASTDeclaration getPointer(ASTDeclaration decl, ParserRuleContext ctx){ Method result = new Method( ((Method) decl).getKind(), ((Method) decl).getName(), - create.primitive_type(PrimitiveSort.Pointer, ((Method) decl).getReturnType()), + addPointer(((Method) decl).getReturnType()), ((Method) decl).getContract(), ((Method) decl).getArgs(), ((Method) decl).usesVarArgs(), ((Method) decl).getBody() ); + result.setOrigin(decl.getOrigin()); + return result; + } else if(decl instanceof TypeAlias) { + TypeAlias result = new TypeAlias( + addPointer(((TypeAlias) decl).aliasedType()), + decl.name() + ); + result.setOrigin(decl.getOrigin()); return result; } @@ -244,9 +274,10 @@ public ASTNode visitDeclaration(DeclarationContext ctx) { expect=null; return res; } else if (match(ctx,null,null,";")){ - VariableDeclaration res=create.variable_decl(checkType(convert(ctx,0))); + Type t = checkType(convert(ctx,0)); ParserRuleContext list=(ParserRuleContext)ctx.getChild(1); ASTNode decls[]=convert_linked_list(list,","); + MultipleDeclaration res=create.multiple_decl(t); for(int i=0;i=0){ @@ -312,14 +344,16 @@ public ASTNode visitDeclarationSpecifiers(DeclarationSpecifiersContext ctx) { Debug("\"class:\" %s",sclass); switch(sclass){ case "typedef": - return create.field_decl(name,create.primitive_type(PrimitiveSort.Class) ,type); + this.flag_in_typedef = true; + break; case "extern": type=create.__extern(type); + break; case "static": type=create.__static(type); break; default: - hre.lang.System.Abort("missing case"); + Abort("missing case"); } } else if (match((ParserRuleContext)ctx.getChild(i),"TypeQualifier")){ Debug("\"tspec:\" %s",ctx.getChild(i).toStringTree(parser)); @@ -341,7 +375,7 @@ public ASTNode visitDeclarationSpecifiers(DeclarationSpecifiersContext ctx) { type=create.__long(type); break; default: - hre.lang.System.Abort("unknown type modifier: %s",modifier); + Abort("unknown type modifier: %s",modifier); } } else if (match((ParserRuleContext)ctx.getChild(i),"TypeSpecifier")){ Debug("\"tspec:\" %s",ctx.getChild(i).toStringTree(parser)); @@ -372,7 +406,7 @@ public ASTNode visitDeclarationSpecifiers(DeclarationSpecifiersContext ctx) { type=create.__local(type); break; default: - hre.lang.System.Abort("unknown type modifier: %s",modifier); + Abort("unknown type modifier: %s",modifier); } } else { ASTNode n=convert(ctx,i); @@ -383,7 +417,7 @@ public ASTNode visitDeclarationSpecifiers(DeclarationSpecifiersContext ctx) { } type.addLabel(l); } else { - hre.lang.System.Abort("cannot handle modifier %s at %s",ctx.getChild(i).toStringTree(parser),n.getOrigin()); + Abort("cannot handle modifier %s at %s",ctx.getChild(i).toStringTree(parser),n.getOrigin()); } } i=i-1; @@ -391,7 +425,13 @@ public ASTNode visitDeclarationSpecifiers(DeclarationSpecifiersContext ctx) { if (name==null){ return type; } else { - return create.field_decl(name,type); + if(flag_in_typedef) { + flag_in_typedef = false; + return create.type_alias(type, name); + } else { + return create.field_decl(name,type); + } + } } @@ -436,7 +476,11 @@ public ASTNode visitDirectAbstractDeclarator( public ASTNode visitDirectDeclarator(DirectDeclaratorContext ctx) { if (match(ctx,(String)null)){ String name=getIdentifier(ctx,0); - return create.field_decl(name, VariableDeclaration.common_type); + if(flag_in_typedef) { + return create.type_alias(MultipleDeclaration.common_type, name); + } else { + return create.field_decl(name, MultipleDeclaration.common_type); + } } boolean pars=false; if (match(ctx,null,"(",")")||(pars=match(ctx,null,"(","ParameterTypeList",")"))){ @@ -450,7 +494,9 @@ public ASTNode visitDirectDeclarator(DirectDeclaratorContext ctx) { Type t=args.get(args.size()-1).getType(); varargs=t.isPrimitive(PrimitiveSort.CVarArgs); } - return create.method_kind(Method.Kind.Plain, VariableDeclaration.common_type, null, name, args, varargs, null); + Method result = create.method_kind(Method.Kind.Plain, MultipleDeclaration.common_type, null, name, args, varargs, null); + result.setStatic(true); + return result; } if (match(ctx,null,"[","]")){ Debug("unspecified array dimension"); @@ -574,10 +620,11 @@ public ASTNode visitFunctionDefinition(FunctionDefinitionContext ctx) { } Type declSpec = (Type)convert(ctx,0); + if(flag_in_typedef) Abort("Parameters cannot be marked typedef"); Method declaration = (Method) convert(ctx, 1); declaration.setBody(convert(ctx, 2)); - VariableDeclaration result = create.variable_decl(declSpec); + MultipleDeclaration result = create.multiple_decl(declSpec); result.add(declaration); return result; } @@ -681,7 +728,7 @@ public ASTNode visitIterationStatement(IterationStatementContext ctx) { ofs+=2; } else if (match(ofs,true,ctx,"(",null,null,";")){ init=convert(ctx,ofs+1); - init=((VariableDeclaration)init).flatten()[0]; + init=((MultipleDeclaration)init).flatten()[0]; test=convert(ctx,ofs+2); ofs+=3; } else { @@ -765,11 +812,12 @@ public ASTNode visitNestedParenthesesBlock(NestedParenthesesBlockContext ctx) { public ASTNode visitParameterDeclaration(ParameterDeclarationContext ctx) { if (match(ctx,null,null)){ Type t=(Type)convert(ctx,0); + if(flag_in_typedef) Abort("Parameters cannot be marked typedef"); ParseTree var=ctx.getChild(1); if (var instanceof ParserRuleContext){ ASTNode v=convert(ctx,1); if (v instanceof DeclarationStatement){ - VariableDeclaration decl=create.variable_decl(t); + MultipleDeclaration decl=create.multiple_decl(t); decl.add((DeclarationStatement)v); ASTDeclaration vars[]=decl.flatten(); if (vars.length==1) return vars[0]; @@ -965,7 +1013,7 @@ public ASTNode visitStorageClassSpecifier(StorageClassSpecifierContext ctx) { public ASTNode visitStructDeclaration(StructDeclarationContext ctx) { if (match(ctx,null,null,";")){ Type t=checkType(convert(ctx,0)); - VariableDeclaration decl=create.variable_decl(t); + MultipleDeclaration decl=create.multiple_decl(t); ASTNode n = convert(ctx,1); decl.add((DeclarationStatement)n); return decl; diff --git a/src/main/java/vct/antlr4/parser/ColIParser.java b/src/main/java/vct/antlr4/parser/ColIParser.java index 92cde9f854..51d9e7ae91 100644 --- a/src/main/java/vct/antlr4/parser/ColIParser.java +++ b/src/main/java/vct/antlr4/parser/ColIParser.java @@ -72,9 +72,9 @@ protected ProgramUnit parse(String file_name,InputStream stream) throws IOExcept Debug("after desugaring",pu); // TODO: encoding as class should not be necessary. - pu=new EncodeAsClass(pu).rewriteAll(); - Progress("Encoding as class took %dms",tk.show()); - Debug("after encoding as class %s",pu); +// pu=new EncodeAsClass(pu).rewriteAll(); +// Progress("Encoding as class took %dms",tk.show()); +// Debug("after encoding as class %s",pu); pu=new FilterSpecIgnore(pu).rewriteAll(); pu=new StripUnusedExtern(pu).rewriteAll(); diff --git a/src/main/java/vct/antlr4/parser/Java7JMLtoCol.java b/src/main/java/vct/antlr4/parser/Java7JMLtoCol.java index 5840eca9f8..4f50be9c73 100644 --- a/src/main/java/vct/antlr4/parser/Java7JMLtoCol.java +++ b/src/main/java/vct/antlr4/parser/Java7JMLtoCol.java @@ -334,7 +334,7 @@ public ASTNode getType(ParserRuleContext ctx) { public ASTNode getVariableDeclaration(ParserRuleContext var_ctx, ASTNode ... list) { int N=list.length-1; ASTNode vars[]=convert_list(var_ctx,","); - VariableDeclaration decl=create.variable_decl(checkType(list[N])); + MultipleDeclaration decl=create.multiple_decl(checkType(list[N])); for(int i=0;i R accept_simple(ASTMapping1 map, A arg){ @@ -53,14 +53,14 @@ public R accept_simple(ASTMapping1 map, A arg){ /** * Multiple variable declarations on top of the given base type. */ - private ArrayList vars=new ArrayList(); + private ArrayList subDeclarations = new ArrayList(); /** * Create an empty list of variables. * * @param basetype */ - public VariableDeclaration(Type basetype){ + public MultipleDeclaration(Type basetype){ this.basetype=basetype; } @@ -98,14 +98,14 @@ public T accept_simple(ASTMapping map){ * @param decl */ public void add(ASTDeclaration decl){ - vars.add(decl); + subDeclarations.add(decl); } /** * Iterate over the (variable) declarations. */ public Iterable get(){ - return vars; + return subDeclarations; } /** @@ -128,7 +128,7 @@ private ArrayList flatten_list(){ AbstractRewriter rw=new MultiSubstitution(null,map); rw.create.setOrigin(getOrigin()); map.put(COMMON_NAME,basetype); - for(ASTDeclaration decl:vars){ + for(ASTDeclaration decl: subDeclarations){ if (decl instanceof DeclarationStatement){ DeclarationStatement d=(DeclarationStatement)decl; String name=d.name(); @@ -140,6 +140,8 @@ private ArrayList flatten_list(){ tmp.setStatic(isStatic()); } list.add(tmp); + } else if(decl instanceof TypeAlias) { + list.add(rw.rewrite(decl)); } else { Method m=(Method)decl; list.add(rw.rewrite(m)); diff --git a/src/main/java/vct/col/ast/stmt/decl/NameSpace.java b/src/main/java/vct/col/ast/stmt/decl/NameSpace.java index 4c1dfaa805..eeeb00fa9b 100644 --- a/src/main/java/vct/col/ast/stmt/decl/NameSpace.java +++ b/src/main/java/vct/col/ast/stmt/decl/NameSpace.java @@ -131,8 +131,8 @@ public Iterator iterator() { public NameSpace add(ASTNode item) { if (item instanceof ASTDeclaration){ space.add((ASTDeclaration)item); - } else if(item instanceof VariableDeclaration) { - for(DeclarationStatement d:((VariableDeclaration)item).flatten()){ + } else if(item instanceof MultipleDeclaration) { + for(DeclarationStatement d:((MultipleDeclaration)item).flatten()){ space.add(d); } } else if (item==null) { diff --git a/src/main/java/vct/col/ast/stmt/decl/ProgramUnit.java b/src/main/java/vct/col/ast/stmt/decl/ProgramUnit.java index 11fd9e0424..fcbc67d7b2 100644 --- a/src/main/java/vct/col/ast/stmt/decl/ProgramUnit.java +++ b/src/main/java/vct/col/ast/stmt/decl/ProgramUnit.java @@ -4,6 +4,7 @@ import java.util.*; +import hre.lang.Failure; import scala.collection.JavaConverters; import vct.col.ast.generic.ASTNode; import vct.col.ast.generic.ASTSequence; @@ -11,6 +12,7 @@ import vct.col.ast.stmt.decl.ASTClass.ClassKind; import vct.col.ast.type.ClassType; import vct.col.ast.type.PrimitiveSort; +import vct.col.ast.type.Type; import vct.col.ast.util.ASTVisitor; import vct.col.util.ASTFactory; import vct.util.ClassName; @@ -237,6 +239,12 @@ public ASTClass find(ClassName name) { if (cl==null){ cl=library.get(name); } + if (cl == null) { + ASTDeclaration decl = find_decl(name.name); + if (decl instanceof ASTClass) { + cl = (ASTClass) decl; + } + } return cl; } @@ -258,14 +266,34 @@ public Method find_predicate(String[] nameFull) { return m; } - public ASTDeclaration find_decl(String[] nameFull) { + public ASTDeclaration find_immediate_decl(String[] nameFull) { ClassName class_name=new ClassName(nameFull); ASTDeclaration res=decl_map.get(class_name); if (res==null){ res=library.get(class_name); } + return res; } + + public ASTDeclaration find_decl(String[] nameFull) { + ASTDeclaration res = find_immediate_decl(nameFull); + + if(res instanceof TypeAlias) { + TypeAlias typeAlias = (TypeAlias) res; + if(typeAlias.aliasedType() instanceof ClassType) { + return find_decl(((ClassType) typeAlias.aliasedType()).getNameFull()); + } else { + Fail("Cannot determine declaration site: %s names a type alias referring to %s, " + + "of which the name cannot be determined.", + nameFull[nameFull.length-1], + typeAlias.aliasedType()); + return null; + } + } else { + return res; + } + } public Method find_adt(String ... nameFull) { ClassName class_name=new ClassName(nameFull); @@ -287,8 +315,8 @@ public Iterator iterator() { public ProgramUnit add(ASTNode item) { if (item instanceof ASTDeclaration){ add((ASTDeclaration)item); - } else if(item instanceof VariableDeclaration) { - for(ASTDeclaration d:((VariableDeclaration)item).flatten_decl()){ + } else if(item instanceof MultipleDeclaration) { + for(ASTDeclaration d:((MultipleDeclaration)item).flatten_decl()){ add(d); } } else { diff --git a/src/main/java/vct/col/ast/stmt/decl/TypeAlias.scala b/src/main/java/vct/col/ast/stmt/decl/TypeAlias.scala new file mode 100644 index 0000000000..5e00d11576 --- /dev/null +++ b/src/main/java/vct/col/ast/stmt/decl/TypeAlias.scala @@ -0,0 +1,22 @@ +package vct.col.ast.stmt.decl + +import vct.col.ast.`type`.Type +import vct.col.ast.util.ASTVisitor +import vct.col.util.{ASTMapping, ASTMapping1} +import vct.util.ClassName + +/** + * A named alias for a type, used for e.g. typedef in C + * @param aliasedType The type that is aliased + * @param name The name of the type that is equivalent to the aliased type + */ +case class TypeAlias(aliasedType: Type, override val name: String) extends ASTDeclaration(name) { + override def getDeclName: ClassName = new ClassName(name) + + override def accept_simple[T](visitor: ASTVisitor[T]): Unit = visitor.visit(this) + override def accept_simple[T](map: ASTMapping[T]): T = map.map(this) + override def accept_simple[R, A](map: ASTMapping1[R, A], arg: A): R = map.map(this, arg) + + override def debugTreeChildrenFields: Iterable[String] = Seq() + override def debugTreePropertyFields: Iterable[String] = Seq("name", "aliasedType") +} diff --git a/src/main/java/vct/col/ast/util/ASTVisitor.java b/src/main/java/vct/col/ast/util/ASTVisitor.java index a3a2355b1b..c7808cef15 100644 --- a/src/main/java/vct/col/ast/util/ASTVisitor.java +++ b/src/main/java/vct/col/ast/util/ASTVisitor.java @@ -71,7 +71,7 @@ public interface ASTVisitor { public void visit(ASTSpecial special); - public void visit(VariableDeclaration variableDeclaration); + public void visit(MultipleDeclaration multipleDeclaration); public void visit(TupleType tupleType); @@ -105,6 +105,8 @@ public interface ASTVisitor { public void visit(Switch s); + public void visit(TypeAlias alias); + } diff --git a/src/main/java/vct/col/ast/util/AbstractVisitor.java b/src/main/java/vct/col/ast/util/AbstractVisitor.java index d1e8dc3eaa..aa606b2fe6 100644 --- a/src/main/java/vct/col/ast/util/AbstractVisitor.java +++ b/src/main/java/vct/col/ast/util/AbstractVisitor.java @@ -133,7 +133,7 @@ public void post_visit(ASTNode n){ @Override public void visit(ASTSpecial s){ visit_any(s); } - @Override public void visit(VariableDeclaration s) { visit_any(s); } + @Override public void visit(MultipleDeclaration s) { visit_any(s); } @Override public void visit(TupleType t) { visit_any(t); } @@ -165,6 +165,11 @@ public void post_visit(ASTNode n){ @Override public void visit(Switch s) { visit_any(s); } + @Override + public void visit(TypeAlias alias) { + visit_any(alias); + } + } diff --git a/src/main/java/vct/col/ast/util/ContractBuilder.java b/src/main/java/vct/col/ast/util/ContractBuilder.java index ee40cb0960..511ecdcebb 100644 --- a/src/main/java/vct/col/ast/util/ContractBuilder.java +++ b/src/main/java/vct/col/ast/util/ContractBuilder.java @@ -6,7 +6,7 @@ import vct.col.ast.stmt.decl.DeclarationStatement; import vct.col.ast.expr.OperatorExpression; import vct.col.ast.expr.StandardOperator; -import vct.col.ast.stmt.decl.VariableDeclaration; +import vct.col.ast.stmt.decl.MultipleDeclaration; import vct.col.ast.generic.ASTNode; import vct.col.ast.stmt.composite.BlockStatement; import vct.col.ast.stmt.decl.Contract; @@ -78,14 +78,14 @@ public void given(DeclarationStatement ... decls){ for(DeclarationStatement d:decls) given.add(d); } - public void given(VariableDeclaration decl){ + public void given(MultipleDeclaration decl){ empty=false; for(DeclarationStatement d:decl.flatten()){ given.add(d); } } - public void yields(VariableDeclaration decl){ + public void yields(MultipleDeclaration decl){ empty=false; for(DeclarationStatement d:decl.flatten()){ yields.add(d); diff --git a/src/main/java/vct/col/ast/util/EmptyVisitor.java b/src/main/java/vct/col/ast/util/EmptyVisitor.java index 72044966b0..554ce8002a 100644 --- a/src/main/java/vct/col/ast/util/EmptyVisitor.java +++ b/src/main/java/vct/col/ast/util/EmptyVisitor.java @@ -190,7 +190,7 @@ public void visit(ASTSpecial special) { } @Override - public void visit(VariableDeclaration variableDeclaration) { + public void visit(MultipleDeclaration multipleDeclaration) { // TODO Auto-generated method stub } @@ -296,5 +296,10 @@ public void visit(Switch s) { // TODO Auto-generated method stub } - + + @Override + public void visit(TypeAlias alias) { + + } + } diff --git a/src/main/java/vct/col/ast/util/RecursiveVisitor.java b/src/main/java/vct/col/ast/util/RecursiveVisitor.java index 425a150f82..806ba35726 100644 --- a/src/main/java/vct/col/ast/util/RecursiveVisitor.java +++ b/src/main/java/vct/col/ast/util/RecursiveVisitor.java @@ -321,7 +321,7 @@ public void visit(ASTSpecial s){ } @Override - public void visit(VariableDeclaration decl) { + public void visit(MultipleDeclaration decl) { dispatch(decl.basetype); for(ASTDeclaration d:decl.get()){ dispatch(d); @@ -403,4 +403,9 @@ public void visit(Switch s) { } } + @Override + public void visit(TypeAlias alias) { + dispatch(alias.aliasedType()); + } + } diff --git a/src/main/java/vct/col/ast/util/UndefinedMapping.java b/src/main/java/vct/col/ast/util/UndefinedMapping.java index 1cdb892520..98c8b894e1 100644 --- a/src/main/java/vct/col/ast/util/UndefinedMapping.java +++ b/src/main/java/vct/col/ast/util/UndefinedMapping.java @@ -1,7 +1,7 @@ package vct.col.ast.util; import hre.lang.HREError; -import vct.col.ast.stmt.decl.VariableDeclaration; +import vct.col.ast.stmt.decl.MultipleDeclaration; import vct.col.ast.stmt.composite.VectorBlock; import vct.col.ast.expr.*; import vct.col.ast.expr.constant.ConstantExpression; @@ -170,7 +170,7 @@ public T map(ASTSpecial special) { } @Override - public T map(VariableDeclaration variableDeclaration) { + public T map(MultipleDeclaration multipleDeclaration) { return null; } @@ -254,4 +254,9 @@ public T map(Switch s) { return null; } + @Override + public T map(TypeAlias alias) { + return null; + } + } diff --git a/src/main/java/vct/col/print/JavaPrinter.java b/src/main/java/vct/col/print/JavaPrinter.java index fe7aa9e613..7770c4ad9d 100644 --- a/src/main/java/vct/col/print/JavaPrinter.java +++ b/src/main/java/vct/col/print/JavaPrinter.java @@ -5,10 +5,7 @@ import hre.ast.TrackingTree; import hre.lang.HREError; -import java.io.PrintStream; import java.io.PrintWriter; -import java.util.List; -import java.util.Map.Entry; import org.apache.commons.lang3.StringEscapeUtils; @@ -1388,7 +1385,7 @@ public void visit(ConstantExpression ce){ } @Override - public void visit(VariableDeclaration decl){ + public void visit(MultipleDeclaration decl){ decl.basetype.accept(this); String sep=" "; for(ASTDeclaration dd:decl.get()){ @@ -1452,4 +1449,13 @@ public void visit(Constraining c){ out.print(")"); c.block().accept(this); } + + @Override + public void visit(TypeAlias alias) { + out.print("typedef "); + alias.aliasedType().accept(this); + out.print(" "); + out.print(alias.name()); + out.print(";\n"); + } } diff --git a/src/main/java/vct/col/rewrite/AbstractRewriter.java b/src/main/java/vct/col/rewrite/AbstractRewriter.java index ee1f75d17f..4ad794e8bf 100644 --- a/src/main/java/vct/col/rewrite/AbstractRewriter.java +++ b/src/main/java/vct/col/rewrite/AbstractRewriter.java @@ -664,8 +664,8 @@ public void visit(ASTSpecial special) { } @Override - public void visit(VariableDeclaration decl) { - VariableDeclaration res=create.variable_decl(decl.basetype); + public void visit(MultipleDeclaration decl) { + MultipleDeclaration res=create.multiple_decl(decl.basetype); for(ASTDeclaration d:decl.get()){ res.add(rewrite(d)); } @@ -870,4 +870,9 @@ public void visit(Switch s){ } result = create.switch_statement(expr, case_list); } + + @Override + public void visit(TypeAlias alias) { + result = create.type_alias(rewrite(alias.aliasedType()), alias.name()); + } } diff --git a/src/main/java/vct/col/rewrite/ConvertTypeExpressions.java b/src/main/java/vct/col/rewrite/ConvertTypeExpressions.java index 1a7f8c15a5..d5b23c3544 100644 --- a/src/main/java/vct/col/rewrite/ConvertTypeExpressions.java +++ b/src/main/java/vct/col/rewrite/ConvertTypeExpressions.java @@ -45,6 +45,28 @@ public void visit(DeclarationStatement d){ } result=res; } + + @Override + public void visit(TypeAlias alias) { + Type type = alias.aliasedType(); + + while(type instanceof TypeExpression) { + TypeExpression typeExpression = (TypeExpression) type; + switch(typeExpression.operator()) { + case Static: + type = typeExpression.firstType(); + break; + case Extern: + type = typeExpression.firstType(); + break; + default: + Fail("cannot deal with type operator %s", typeExpression.operator()); + } + } + + TypeAlias newAlias = create.type_alias(type, alias.name()); + result = newAlias; + } @Override public void visit(Method m){ diff --git a/src/main/java/vct/col/rewrite/FlattenVariableDeclarations.java b/src/main/java/vct/col/rewrite/FlattenVariableDeclarations.java index 7615c79bb0..ea823f3e2c 100644 --- a/src/main/java/vct/col/rewrite/FlattenVariableDeclarations.java +++ b/src/main/java/vct/col/rewrite/FlattenVariableDeclarations.java @@ -3,7 +3,7 @@ import vct.col.ast.stmt.decl.ASTFlags; import vct.col.ast.stmt.decl.DeclarationStatement; import vct.col.ast.stmt.decl.ProgramUnit; -import vct.col.ast.stmt.decl.VariableDeclaration; +import vct.col.ast.stmt.decl.MultipleDeclaration; public class FlattenVariableDeclarations extends AbstractRewriter { @@ -12,7 +12,7 @@ public FlattenVariableDeclarations(ProgramUnit source) { } @Override - public void visit(VariableDeclaration decl) { + public void visit(MultipleDeclaration decl) { for(DeclarationStatement tmp:decl.flatten()){ if (decl.isValidFlag(ASTFlags.STATIC)){ tmp.setStatic(decl.isStatic()); diff --git a/src/main/java/vct/col/rewrite/MultiSubstitution.java b/src/main/java/vct/col/rewrite/MultiSubstitution.java index 879a41f3c8..ace656916e 100644 --- a/src/main/java/vct/col/rewrite/MultiSubstitution.java +++ b/src/main/java/vct/col/rewrite/MultiSubstitution.java @@ -1,6 +1,7 @@ package vct.col.rewrite; import vct.col.ast.stmt.decl.Method; +import vct.col.ast.stmt.decl.TypeAlias; import vct.col.ast.type.ClassType; import vct.col.ast.stmt.decl.ProgramUnit; import vct.col.ast.type.Type; @@ -26,6 +27,13 @@ public void visit(Method m) { ); } + public void visit(TypeAlias alias) { + result = create.type_alias( + rewrite(alias.aliasedType()), + alias.name() + ); + } + public void visit(ClassType t){ String name[]=t.getNameFull(); if (name.length==1){ diff --git a/src/main/java/vct/col/rewrite/RewriteRecordPointers.scala b/src/main/java/vct/col/rewrite/RewriteRecordPointers.scala new file mode 100644 index 0000000000..944b767b08 --- /dev/null +++ b/src/main/java/vct/col/rewrite/RewriteRecordPointers.scala @@ -0,0 +1,50 @@ +package vct.col.rewrite + +import vct.col.ast.`type`.{ClassType, PrimitiveSort, PrimitiveType, Type} +import vct.col.ast.stmt.decl.{ASTClass, ProgramUnit, TypeAlias} +import hre.lang.System.Output +import vct.col.ast.expr.{NameExpression, OperatorExpression, StandardOperator} + +class RewriteRecordPointers(source: ProgramUnit) extends AbstractRewriter(source) { + override def visit(t: PrimitiveType): Unit = { + t.sort match { + case PrimitiveSort.Pointer => + t.firstarg match { + case classType: ClassType => + val definition = source.find_decl(classType.getNameFull) + if (definition.asInstanceOf[ASTClass].kind == ASTClass.ClassKind.Record) { + result = classType + } else { + super.visit(t) + } + case _ => super.visit(t) + } + case _ => + super.visit(t) + } + } + + override def visit(alias: TypeAlias): Unit = { + // We copy type aliases, as we can safely allow bare record types in type aliases. Only in resolved types we cannot + // allow bare record types. + result = copy_rw.rewrite(alias) + } + + override def visit(t: ClassType): Unit = { + source.find_immediate_decl(t.getNameFull) match { + case alias: TypeAlias => + result = rewrite(alias.aliasedType) + case cls: ASTClass if cls.kind == ASTClass.ClassKind.Record => + Fail("%s", "Unsupported: cannot refer to a struct without indirection") + case _ => + super.visit(t) + } + } + + override def visit(o: OperatorExpression): Unit = o.operator match { + case StandardOperator.StructDeref => + result = create.dereference(rewrite(o.arg(0)), o.arg(1).asInstanceOf[NameExpression].getName) + case _ => + super.visit(o) + } +} diff --git a/src/main/java/vct/col/rewrite/RewriteSystem.java b/src/main/java/vct/col/rewrite/RewriteSystem.java index f7f14cd928..d6f9e2e3ff 100644 --- a/src/main/java/vct/col/rewrite/RewriteSystem.java +++ b/src/main/java/vct/col/rewrite/RewriteSystem.java @@ -285,7 +285,7 @@ public Boolean map(ASTSpecial special, ASTNode a) { } @Override - public Boolean map(VariableDeclaration variableDeclaration, ASTNode a) { + public Boolean map(MultipleDeclaration multipleDeclaration, ASTNode a) { return null; } @@ -382,7 +382,12 @@ public Boolean map(Constraining c, ASTNode a) { public Boolean map(Switch s, ASTNode a) { return null; } - + + @Override + public Boolean map(TypeAlias alias, ASTNode a) { + return null; + } + } class MatchSubstitution extends AbstractRewriter { diff --git a/src/main/java/vct/col/rewrite/SatCheckRewriter.java b/src/main/java/vct/col/rewrite/SatCheckRewriter.java index 319d93c911..210b54a1f7 100644 --- a/src/main/java/vct/col/rewrite/SatCheckRewriter.java +++ b/src/main/java/vct/col/rewrite/SatCheckRewriter.java @@ -71,10 +71,11 @@ public void visit(Method m) { m.usesVarArgs(), blockStatement ); + assert_method.setStatic(m.isStatic()); blockStatement.setParent(assert_method); - currentTargetClass.add(assert_method); + target().add(assert_method); } } diff --git a/src/main/java/vct/col/util/ASTFactory.java b/src/main/java/vct/col/util/ASTFactory.java index 2789d473d3..5175fc1e3d 100644 --- a/src/main/java/vct/col/util/ASTFactory.java +++ b/src/main/java/vct/col/util/ASTFactory.java @@ -434,6 +434,17 @@ public DeclarationStatement field_decl(Origin o,String name, Type type,ASTNode i res.accept_if(post); return res; } + + public TypeAlias type_alias(Origin o, Type type, String name) { + TypeAlias res = new TypeAlias(type, name); + res.setOrigin(o); + res.accept_if(post); + return res; + } + + public TypeAlias type_alias(Type type, String name) { + return type_alias(origin_stack.get(), type, name); + } /** * Create a name expression that refers to a field name. @@ -1095,8 +1106,8 @@ public NameExpression unresolved_name(String name) { return res; } -public VariableDeclaration variable_decl(Type type) { - VariableDeclaration res=new VariableDeclaration(type); +public MultipleDeclaration multiple_decl(Type type) { + MultipleDeclaration res=new MultipleDeclaration(type); res.setOrigin(origin_stack.get()); res.accept_if(post); return res; diff --git a/src/main/java/vct/col/util/ASTMapping.java b/src/main/java/vct/col/util/ASTMapping.java index cb390a081f..d29f5f7ea4 100644 --- a/src/main/java/vct/col/util/ASTMapping.java +++ b/src/main/java/vct/col/util/ASTMapping.java @@ -68,7 +68,7 @@ public interface ASTMapping { public R map(ASTSpecial special); - public R map(VariableDeclaration variableDeclaration); + public R map(MultipleDeclaration multipleDeclaration); public R map(TupleType tupleType); @@ -102,4 +102,6 @@ public interface ASTMapping { public R map(Switch s); + public R map(TypeAlias alias); + } diff --git a/src/main/java/vct/col/util/ASTMapping1.java b/src/main/java/vct/col/util/ASTMapping1.java index 0e29fee149..88ee0e7ff5 100644 --- a/src/main/java/vct/col/util/ASTMapping1.java +++ b/src/main/java/vct/col/util/ASTMapping1.java @@ -70,7 +70,7 @@ public interface ASTMapping1 { public R map(ASTSpecial special, A1 a); - public R map(VariableDeclaration variableDeclaration,A1 a); + public R map(MultipleDeclaration multipleDeclaration, A1 a); public R map(TupleType tupleType, A1 a); @@ -101,4 +101,6 @@ public interface ASTMapping1 { public R map(Constraining c, A1 a); public R map(Switch s,A1 a); + + public R map(TypeAlias alias, A1 a); } diff --git a/src/main/java/vct/learn/CountVisitor.java b/src/main/java/vct/learn/CountVisitor.java index 4a1f83b714..e7886a40b5 100644 --- a/src/main/java/vct/learn/CountVisitor.java +++ b/src/main/java/vct/learn/CountVisitor.java @@ -23,7 +23,7 @@ import vct.col.ast.stmt.composite.VectorBlock; import vct.col.ast.stmt.decl.ASTDeclaration; import vct.col.ast.stmt.decl.ProgramUnit; -import vct.col.ast.stmt.decl.VariableDeclaration; +import vct.col.ast.stmt.decl.MultipleDeclaration; import vct.col.ast.stmt.terminal.AssignmentStatement; import vct.col.ast.stmt.terminal.ReturnStatement; import vct.col.ast.type.TypeVariable; @@ -186,7 +186,7 @@ public void visit(TypeVariable tv) { } @Override - public void visit(VariableDeclaration vd) { + public void visit(MultipleDeclaration vd) { counter.count(vd.getClass().getName()); super.visit(vd); } diff --git a/src/main/java/vct/main/Main.java b/src/main/java/vct/main/Main.java index 59c6c91525..ab5a502694 100644 --- a/src/main/java/vct/main/Main.java +++ b/src/main/java/vct/main/Main.java @@ -345,6 +345,7 @@ public static void main(String[] args) throws Throwable passes.add("dafny"); // run backend } else if (silver.used()||chalice.get()) { passes=new LinkedBlockingDeque(); + passes.add("record_pointers"); passes.add("java_resolve"); if (silver.used() && @@ -914,6 +915,11 @@ public ProgramUnit apply(ProgramUnit arg,String ... args){ return new Flatten(arg).rewriteAll(); } }); + defined_passes.put("record_pointers", new CompilerPass("rewrite pointers to record classes as plain classes") { + public ProgramUnit apply(ProgramUnit arg, String... args) { + return new RewriteRecordPointers(arg).rewriteAll(); + } + }); defined_passes.put("ghost-lift",new CompilerPass("Lift ghost code to real code"){ public ProgramUnit apply(ProgramUnit arg,String ... args){ return new GhostLifter(arg).rewriteAll(); diff --git a/src/main/java/vct/silver/SilverExpressionMap.java b/src/main/java/vct/silver/SilverExpressionMap.java index 1a48ab1762..3f2220747c 100644 --- a/src/main/java/vct/silver/SilverExpressionMap.java +++ b/src/main/java/vct/silver/SilverExpressionMap.java @@ -412,7 +412,7 @@ public E map(ASTSpecial special) { } @Override - public E map(VariableDeclaration variableDeclaration) { + public E map(MultipleDeclaration multipleDeclaration) { return null; } @@ -520,5 +520,10 @@ public E map(Constraining c) { public E map(Switch s) { return null; } - + + @Override + public E map(TypeAlias alias) { + return null; + } + } diff --git a/src/main/java/vct/silver/SilverStatementMap.java b/src/main/java/vct/silver/SilverStatementMap.java index f7f078f191..0a0ac7dcae 100644 --- a/src/main/java/vct/silver/SilverStatementMap.java +++ b/src/main/java/vct/silver/SilverStatementMap.java @@ -20,7 +20,6 @@ import vct.col.ast.type.*; import vct.col.util.ASTUtils; import static hre.lang.System.Abort; -import static hre.lang.System.Output; import viper.api.*; @@ -296,7 +295,7 @@ public S map(ASTSpecial special) { } @Override - public S map(VariableDeclaration variableDeclaration) { + public S map(MultipleDeclaration multipleDeclaration) { return null; } @@ -416,4 +415,9 @@ public S map(Constraining c) { public S map(Switch s) { return null; } + + @Override + public S map(TypeAlias alias) { + return null; + } } diff --git a/src/main/java/vct/silver/VerCorsProgramFactory.java b/src/main/java/vct/silver/VerCorsProgramFactory.java index ee5390801e..993130faae 100644 --- a/src/main/java/vct/silver/VerCorsProgramFactory.java +++ b/src/main/java/vct/silver/VerCorsProgramFactory.java @@ -10,19 +10,11 @@ import hre.ast.Origin; import hre.lang.HREError; import hre.tools.TimeKeeper; -import vct.col.ast.stmt.decl.ASTFlags; +import vct.col.ast.stmt.decl.*; import vct.col.ast.generic.ASTNode; -import vct.col.ast.stmt.decl.ASTSpecial; -import vct.col.ast.stmt.decl.ASTClass; -import vct.col.ast.stmt.decl.Axiom; -import vct.col.ast.stmt.decl.AxiomaticDataType; import vct.col.ast.stmt.composite.BlockStatement; -import vct.col.ast.stmt.decl.Contract; import vct.col.ast.type.PrimitiveSort; import vct.col.ast.util.ContractBuilder; -import vct.col.ast.stmt.decl.DeclarationStatement; -import vct.col.ast.stmt.decl.Method; -import vct.col.ast.stmt.decl.ProgramUnit; import vct.col.ast.expr.StandardOperator; import vct.col.ast.type.Type; import vct.col.util.ASTFactory; @@ -325,6 +317,8 @@ public P convert( throw new HREError("bad special declaration entry: %s",s.kind); } + } else if(entry instanceof TypeAlias) { + // There is nothing to do; type aliases are resolved to the correct type at the usage site. } else { throw new HREError("bad entry: %s",entry.getClass()); }