Skip to content

Commit

Permalink
structs and typedefs mostly working, fixes #347, fixes #348
Browse files Browse the repository at this point in the history
  • Loading branch information
pieter-bos committed Dec 10, 2019
1 parent 5677dc8 commit 3e5efc1
Show file tree
Hide file tree
Showing 34 changed files with 368 additions and 87 deletions.
37 changes: 37 additions & 0 deletions examples/basic/struct.c
Original file line number Diff line number Diff line change
@@ -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);
}
11 changes: 5 additions & 6 deletions src/main/java/vct/antlr4/parser/ANTLRtoCOL.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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.*;
Expand Down Expand Up @@ -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)));
Expand All @@ -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);
Expand Down
80 changes: 64 additions & 16 deletions src/main/java/vct/antlr4/parser/CMLtoCOL.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -27,6 +28,7 @@

import java.util.ArrayList;

import static hre.lang.System.Abort;
import static hre.lang.System.Debug;

/**
Expand All @@ -39,6 +41,11 @@
* @author <a href="mailto:[email protected]">Stefan Blom</a>
*/
public class CMLtoCOL extends ANTLRtoCOL implements CMLVisitor<ASTNode> {
/**
* 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 extends ASTSequence<?>> 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);
Expand Down Expand Up @@ -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");
Expand All @@ -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()
);

Expand All @@ -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;
}
Expand Down Expand Up @@ -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<decls.length;i++){
if (decls[i] instanceof ASTDeclaration){
res.add((ASTDeclaration)decls[i]);
Expand All @@ -258,6 +289,7 @@ public ASTNode visitDeclaration(DeclarationContext ctx) {
return null;
}
}
flag_in_typedef = false;
return res;
}
return null;
Expand Down Expand Up @@ -302,7 +334,7 @@ public ASTNode visitDeclarationSpecifiers(DeclarationSpecifiersContext ctx) {
} else if (t instanceof NameExpression){
type=create.class_type(((NameExpression)t).getName());
} else {
hre.lang.System.Abort("cannot convert %s/%s to type",tmp.toStringTree(parser),t.getClass());
Abort("cannot convert %s/%s to type",tmp.toStringTree(parser),t.getClass());
}
i=i-1;
while(i>=0){
Expand All @@ -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));
Expand All @@ -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));
Expand Down Expand Up @@ -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);
Expand All @@ -383,15 +417,21 @@ 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;
}
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);
}

}
}

Expand Down Expand Up @@ -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",")"))){
Expand All @@ -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");
Expand Down Expand Up @@ -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;
}
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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];
Expand Down Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions src/main/java/vct/antlr4/parser/ColIParser.java
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
8 changes: 4 additions & 4 deletions src/main/java/vct/antlr4/parser/Java7JMLtoCol.java
Original file line number Diff line number Diff line change
Expand Up @@ -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<vars.length;i++){
DeclarationStatement tmp;
if (vars[i] instanceof NameExpression){
Expand Down Expand Up @@ -1021,14 +1021,14 @@ public ASTNode visitForInit(ForInitContext ctx) {
@Override
public ASTNode visitFormalParameter(FormalParameterContext ctx) {
if (match(ctx,null,null)){
VariableDeclaration decl=create.variable_decl(checkType(convert(ctx,0)));
MultipleDeclaration decl=create.multiple_decl(checkType(convert(ctx,0)));
DeclarationStatement var=getVariableDeclaratorId((ParserRuleContext)ctx.getChild(1));
decl.add(var);
DeclarationStatement vars[]=decl.flatten();
if (vars.length==1) return vars[0];
}
if (match(ctx,"final",null,null)){
VariableDeclaration decl=create.variable_decl(checkType(convert(ctx,1)));
MultipleDeclaration decl=create.multiple_decl(checkType(convert(ctx,1)));
DeclarationStatement var=getVariableDeclaratorId((ParserRuleContext)ctx.getChild(2));
decl.add(var);
DeclarationStatement vars[]=decl.flatten();
Expand Down Expand Up @@ -1186,7 +1186,7 @@ public ASTNode visitJavaStatements(JavaStatementsContext ctx) {
@Override
public ASTNode visitLastFormalParameter(LastFormalParameterContext ctx) {
if (match(ctx,null,"...",null)){
VariableDeclaration decl=create.variable_decl(checkType(convert(ctx,0)));
MultipleDeclaration decl=create.multiple_decl(checkType(convert(ctx,0)));
DeclarationStatement var=getVariableDeclaratorId((ParserRuleContext)ctx.getChild(2));
decl.add(var);
DeclarationStatement vars[]=decl.flatten();
Expand Down
6 changes: 3 additions & 3 deletions src/main/java/vct/antlr4/parser/Java8JMLtoCol.java
Original file line number Diff line number Diff line change
Expand Up @@ -395,7 +395,7 @@ public ASTNode getExpression(ParserRuleContext ctx) {

public DeclarationStatement getFormalParameter(ParserRuleContext ctx) {
if (match(ctx,null,null)){
VariableDeclaration decl=create.variable_decl(checkType(convert(ctx,0)));
MultipleDeclaration decl=create.multiple_decl(checkType(convert(ctx,0)));
DeclarationStatement var=getVariableDeclaratorId((ParserRuleContext)ctx.getChild(1));
decl.add(var);
DeclarationStatement vars[]=decl.flatten();
Expand Down Expand Up @@ -434,7 +434,7 @@ public ASTNode getImportDeclaration(ParserRuleContext ctx) {

public DeclarationStatement getLastFormalParameter(ParserRuleContext ctx) {
if (match(ctx,null,"...",null)){
VariableDeclaration decl=create.variable_decl(checkType(convert(ctx,0)));
MultipleDeclaration decl=create.multiple_decl(checkType(convert(ctx,0)));
DeclarationStatement var=getVariableDeclaratorId((ParserRuleContext)ctx.getChild(2));
decl.add(var);
DeclarationStatement vars[]=decl.flatten();
Expand Down Expand Up @@ -665,7 +665,7 @@ private ASTNode getVariableDeclaration(ParserRuleContext ctx) {
}
Type t=checkType(convert(ctx,base));
ASTNode vars[]=convert_list((ParserRuleContext)ctx.getChild(base+1),",");
VariableDeclaration decl=create.variable_decl(t);
MultipleDeclaration decl=create.multiple_decl(t);
for(int i=0;i<vars.length;i++){
DeclarationStatement tmp;
if (vars[i] instanceof NameExpression){
Expand Down
Loading

0 comments on commit 3e5efc1

Please sign in to comment.