Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feat rust operators #5380

Merged
merged 4 commits into from
Apr 29, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
2 changes: 1 addition & 1 deletion .github/workflows/msbuild.yml
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ jobs:
run: dotnet tool restore
- name: Check whitespace and style
working-directory: dafny
run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
- name: Get Boogie Version
run: |
sudo apt-get update
Expand Down
2 changes: 1 addition & 1 deletion .pre-commit-config.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,5 @@ repos:
- id: dotnet-format
name: dotnet-format
language: system
entry: dotnet format whitespace Source/Dafny.sln --include
entry: dotnet format whitespace Source/Dafny.sln -v:d --include
types_or: ["c#"]
4 changes: 2 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ dfyprod: dfyprodformat dfyprodinit
(cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser

dfydevinit:
(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify --no-format)
(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify)

dfydev: dfydevinit
(cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
Expand Down Expand Up @@ -73,7 +73,7 @@ z3-ubuntu:
chmod +x ${DIR}/Binaries/z3/bin/z3-*

format:
dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs

clean:
(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
Expand Down
11 changes: 11 additions & 0 deletions Source/DafnyCore.Test/GeneratedDafnyTest.cs
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
using System.Collections.Concurrent;
using Microsoft.Dafny;

namespace DafnyCore.Test;

public class GeneratedDafnyTest {
[Fact]
public void TestDafnyGeneratedCode() {
DafnyToRustCompilerCoverage.RASTCoverage.__default.TestExpr();
}
}

Large diffs are not rendered by default.

4 changes: 4 additions & 0 deletions Source/DafnyCore/AST/Expressions/Variables/IVariable.cs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,10 @@ string UniqueName {
string SanitizedName {
get;
}
string SanitizedNameShadowable { // A name suitable for compilation, but without the unique identifier.
// Useful to generate readable identifiers in the generated source code.
get;
}
string CompileName {
get;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,13 @@ public string SanitizedName {
throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
}
}

public string SanitizedNameShadowable {
get {
Contract.Ensures(Contract.Result<string>() != null);
throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
}
}
public string CompileName {
get {
Contract.Ensures(Contract.Result<string>() != null);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -74,9 +74,14 @@ public static string SanitizeName(string nm) {
}
}

private string sanitizedNameShadowable;

public virtual string SanitizedNameShadowable =>
sanitizedNameShadowable ??= SanitizeName(Name);

private string sanitizedName;
public virtual string SanitizedName =>
sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizeName(Name)}";
sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";

protected string compileName;
public virtual string CompileName =>
Expand Down
8 changes: 7 additions & 1 deletion Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs
Original file line number Diff line number Diff line change
Expand Up @@ -68,9 +68,15 @@ public string AssignUniqueName(FreshIdGenerator generator) {
return uniqueName ??= generator.FreshId(Name + "#");
}

private string sanitizedNameShadowable;

public string SanitizedNameShadowable =>
sanitizedNameShadowable ??= NonglobalVariable.SanitizeName(Name);

private string sanitizedName;

public string SanitizedName =>
sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{NonglobalVariable.SanitizeName(Name)}";
sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";

string compileName;
public string CompileName =>
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ public class NativeType {
public readonly BigInteger LowerBound;
public readonly BigInteger UpperBound;
public readonly int Bitwidth; // for unassigned types, this shows the number of bits in the type; else is 0
public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long }
public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long, UDoubleLong, DoubleLong }
public readonly Selection Sel;
public NativeType(string Name, BigInteger LowerBound, BigInteger UpperBound, int bitwidth, Selection sel) {
Contract.Requires(Name != null);
Expand Down
7 changes: 4 additions & 3 deletions Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -3422,15 +3422,16 @@ protected override ConcreteSyntaxTree EmitMapBuilder_Add(MapType mt, IToken tok,
return termLeftWriter;
}

protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) {
protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName,
ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) {
if (ct is SetType) {
var typeName = TypeName(ct.Arg, wr, tok);
return string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})");
wr.Write(string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})"));
} else if (ct is MapType) {
var mt = (MapType)ct;
var domtypeName = TypeName(mt.Domain, wr, tok);
var rantypeName = TypeName(mt.Range, wr, tok);
return $"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})";
wr.Write($"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})");
} else {
Contract.Assume(false); // unexpected collection type
throw new cce.UnreachableException(); // please compiler
Expand Down
5 changes: 3 additions & 2 deletions Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2455,9 +2455,10 @@ protected override ConcreteSyntaxTree EmitMapBuilder_Add(MapType mt, IToken tok,
throw new UnsupportedFeatureException(tok, Feature.MapComprehensions);
}

protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) {
protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName,
ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) {
// collections are built in place
return collName;
wr.Write(collName);
}

protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBody, string type,
Expand Down
68 changes: 58 additions & 10 deletions Source/DafnyCore/Backends/Dafny/AST.dfy
Original file line number Diff line number Diff line change
@@ -1,3 +1,22 @@
module {:extern "DAST.Format"} DAST.Format
/* Cues about how to format different AST elements if necessary,
e.g. to generate idiomatic code when needed. */
{
// Dafny AST compilation tenets:
// - The Compiled Dafny AST should be minimal
// - The generated code should look idiomatic and close to the original Dafny file if possible
// Since the two might conflict, the second one is taken care of by adding formatting information

datatype UnaryOpFormat =
| NoFormat
| CombineFormat
datatype BinaryOpFormat =
| NoFormat
| ImpliesFormat
| EquivalenceFormat
| ReverseFormat
}

module {:extern "DAST"} DAST {
import opened Std.Wrappers

Expand All @@ -19,13 +38,22 @@ module {:extern "DAST"} DAST {
Set(element: Type) |
Multiset(element: Type) |
Map(key: Type, value: Type) |
SetBuilder(element: Type) |
MapBuilder(key: Type, value: Type) |
Arrow(args: seq<Type>, result: Type) |
Primitive(Primitive) | Passthrough(string) |
TypeArg(Ident)

datatype Primitive = Int | Real | String | Bool | Char

datatype ResolvedType = Datatype(path: seq<Ident>) | Trait(path: seq<Ident>) | Newtype(Type)
datatype NewtypeRange =
| U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | BigInt
| NoRange

datatype ResolvedType =
| Datatype(path: seq<Ident>)
| Trait(path: seq<Ident>)
| Newtype(baseType: Type, range: NewtypeRange, erase: bool)

datatype Ident = Ident(id: string)

Expand All @@ -37,7 +65,7 @@ module {:extern "DAST"} DAST {

datatype DatatypeCtor = DatatypeCtor(name: string, args: seq<Formal>, hasAnyArgs: bool /* includes ghost */)

datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)
datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, range: NewtypeRange, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)

datatype ClassItem = Method(Method)

Expand All @@ -47,14 +75,18 @@ module {:extern "DAST"} DAST {

datatype Method = Method(isStatic: bool, hasBody: bool, overridingPath: Option<seq<Ident>>, name: string, typeParams: seq<Type>, params: seq<Formal>, body: seq<Statement>, outTypes: seq<Type>, outVars: Option<seq<Ident>>)

datatype CallName =
Name(name: string) |
MapBuilderAdd | MapBuilderBuild | SetBuilderAdd | SetBuilderBuild

datatype Statement =
DeclareVar(name: string, typ: Type, maybeValue: Option<Expression>) |
Assign(lhs: AssignLhs, value: Expression) |
If(cond: Expression, thn: seq<Statement>, els: seq<Statement>) |
Labeled(lbl: string, body: seq<Statement>) |
While(cond: Expression, body: seq<Statement>) |
Foreach(boundName: string, boundType: Type, over: Expression, body: seq<Statement>) |
Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
Return(expr: Expression) |
EarlyReturn() |
Break(toLabel: Option<string>) |
Expand All @@ -72,13 +104,21 @@ module {:extern "DAST"} DAST {

datatype BinOp =
Eq(referential: bool, nullable: bool) |
Neq(referential: bool, nullable: bool) |
Div() | EuclidianDiv() |
Mod() | EuclidianMod() |
Implies() | // TODO: REplace by Not Or
Lt() | // a <= b is !(b < a)
LtChar() |
Plus() | Minus() | Times() |
BitwiseAnd() | BitwiseOr() | BitwiseXor() |
BitwiseShiftRight() | BitwiseShiftLeft() |
And() | Or() |
In() |
NotIn() | // TODO: Replace by Not In
SetDifference() |
SeqProperPrefix() | SeqPrefix() |
SetMerge() | SetSubtraction() | SetIntersection() |
Subset() | ProperSubset() | SetDisjoint() |
MapMerge() | MapSubtraction() |
MultisetMerge() | MultisetSubtraction() | MultisetIntersection() |
Submultiset() | ProperSubmultiset() | MultisetDisjoint() |
Concat() |
Passthrough(string)

Expand All @@ -94,18 +134,26 @@ module {:extern "DAST"} DAST {
SeqConstruct(length: Expression, elem: Expression) |
SeqValue(elements: seq<Expression>, typ: Type) |
SetValue(elements: seq<Expression>) |
MultisetValue(elements: seq<Expression>) |
MapValue(mapElems: seq<(Expression, Expression)>) |
MapBuilder(keyType: Type, valueType: Type) |
SeqUpdate(expr: Expression, indexExpr: Expression, value: Expression) |
MapUpdate(expr: Expression, indexExpr: Expression, value: Expression) |
SetBuilder(elemType: Type) |
ToMultiset(Expression) |
This() |
Ite(cond: Expression, thn: Expression, els: Expression) |
UnOp(unOp: UnaryOp, expr: Expression) |
BinOp(op: BinOp, left: Expression, right: Expression) |
UnOp(unOp: UnaryOp, expr: Expression, format1: Format.UnaryOpFormat) |
BinOp(op: BinOp, left: Expression, right: Expression, format2: Format.BinaryOpFormat) |
ArrayLen(expr: Expression, dim: nat) |
MapKeys(expr: Expression) |
MapValues(expr: Expression) |
Select(expr: Expression, field: string, isConstant: bool, onDatatype: bool) |
SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) |
Index(expr: Expression, collKind: CollKind, indices: seq<Expression>) |
IndexRange(expr: Expression, isArray: bool, low: Option<Expression>, high: Option<Expression>) |
TupleSelect(expr: Expression, index: nat) |
Call(on: Expression, name: Ident, typeArgs: seq<Type>, args: seq<Expression>) |
Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>) |
Lambda(params: seq<Formal>, retType: Type, body: seq<Statement>) |
BetaRedex(values: seq<(Formal, Expression)>, retType: Type, expr: Expression) |
IIFE(name: Ident, typ: Type, value: Expression, iifeBody: Expression) |
Expand Down
Loading
Loading