diff --git a/Makefile.test262 b/Makefile.test262 index c163192..9040882 100644 --- a/Makefile.test262 +++ b/Makefile.test262 @@ -23,8 +23,8 @@ test262-core-negative: $(TEST262_CORE_NEGATIVE:%=%.out.negative) define krun-test262 ( cat prelude.js $(1) >$(1).prelude && \ ./jsmassage.sh -f $(1).prelude >$(1).prelude.massage && \ - krun -d . --pattern-matching $(1).prelude.massage >$(1).out 2>$(1).err && \ - test "`sed -n '//,/<\/k>/{ p }' $(1).out | tr -d ' \n'`" = "@Normal"; \ + krun -d . $(1).prelude.massage --output-file $(1).out 2>$(1).err && \ + test "`sed -n '//,/<\/k>/{ p }' $(1).out`" = "`cat normal-completion-configuration.txt`"; \ echo $$? >$(1).exitcode ) @if [ $(2) = "positive" ]; then \ if [ `cat $(1).exitcode` -eq 0 ]; then echo "#### $(1) succeed"; else echo "#### $(1) failed"; exit 1; fi; \ diff --git a/es6/js-syntax.k b/es6/js-syntax.k new file mode 100644 index 0000000..be2f4a4 --- /dev/null +++ b/es6/js-syntax.k @@ -0,0 +1,366 @@ +module JS-SYNTAX + +////////////////////////////////////////////////////////////////////// +// A.1 Lexical Grammar +////////////////////////////////////////////////////////////////////// + +syntax RegularExpressionLiteral // TODO + +////////////////////////////////////////////////////////////////////// +// A.2 Expressions +////////////////////////////////////////////////////////////////////// + +// IdentifierReference, BindingIdentifier, LabelIdentifier +syntax Identifier ::= r"[\\_\\$A-Za-z][\\_\\$A-Za-z0-9]*" [token] + +syntax PrimaryExpression ::= "this" + | Identifier /* IdentifierReference */ + | Literal + | "[" Elements "]" /* ArrayLiteral */ + | "{" PropertyDefinitions "}" /* ObjectLiteral */ [klabel('{_}::PropertyAssignments->PrimaryExpression)] + | Function /* FunctionExpression */ + | Class /* ClassExpression */ + | Generator /* GeneratorExpression */ + | RegularExpressionLiteral + | TemplateLiteral + | "(" Expression ")" /* ParenthesizedExpression */ /* CoverParenthesizedExpressionAndArrowParameterList */ [klabel('(_)::ExpressionS->PrimaryExpression)] + +syntax Literal ::= NullLiteral + | Bool // TODO: BooleanLiteral + | Int | Float // TODO: NumericLiteral + | String // TODO: StringLiteral + +syntax NullLiteral ::= "null" + +syntax Bool +syntax Int +syntax Float +syntax String + +// ElementList, Arguments, ArgumentList +syntax Elements ::= List{Element, ","} +syntax Element ::= "" /* Elision */ /* NOTE: not allowed in Arguments and ArgumentList */ [avoid, onlyLabel, klabel('epsilonElement)] + | Expression /* AssignmentExpression */ + | "..." Expression /* SpreadElement */ /* AssignmentExpression */ + +// TODO: merge with Element +syntax ExpressionOpt ::= Expression + | "" [avoid, onlyLabel, klabel('epsilonExpression)] + +// PropertyDefinitionList +syntax PropertyDefinitions ::= List{PropertyDefinition, ","} [klabel('_,_::PropertyAssignment*PropertyAssignments->PropertyAssignments)] +syntax PropertyDefinition ::= SingleNameBinding /* IdentifierReference, CoverInitializedName */ + | PropertyName ":" Expression /* AssignmentExpression */ [klabel('_:_::PropertyName*Expression->PropertyAssignment)] + | MethodDefinition + +syntax PropertyName ::= LiteralPropertyName + | ComputedPropertyName + +syntax LiteralPropertyName ::= Identifier | NullLiteral | Bool // TODO: IdentifierName + | String // TODO: StringLiteral + | Int | Float // TODO: NumericLiteral + +syntax ComputedPropertyName ::= "[" Expression "]" /* AssignmentExpression */ + +syntax TemplateLiteral // TODO + +// MemberExpression, NewExpression, CallExpression +syntax LeftHandSideExpression ::= PrimaryExpression + | LeftHandSideExpression "[" Expression "]" [klabel('_[_]::Expression*Expression->Expression)] + | LeftHandSideExpression "." Identifier /* TODO: IdentifierName */ [klabel('_._::Expression*Name->Expression)] + | LeftHandSideExpression "(" Elements ")" /* Arguments */ + | LeftHandSideExpression TemplateLiteral + | "super" "[" Expression "]" /* SuperProperty */ + | "super" "." Identifier /* SuperProperty */ /* TODO: IdentifierName */ + | "super" "(" Elements ")" /* SuperCall */ /* Arguments */ + | "new" LeftHandSideExpression "(" Elements ")" /* Arguments */ + | "new" LeftHandSideExpression + | "new" "." "target" /* MetaProperty */ /* NewTarget */ + +// AssignmentExpression +syntax Expression ::= LeftHandSideExpression + // PostfixExpression + > Expression "++" + | Expression "--" + // UnaryExpression + > "delete" Expression + | "void" Expression + | "typeof" Expression + | "++" Expression [prefer] + | "--" Expression [prefer] + | "+" Expression + | "-" Expression + | "~" Expression + | "!" Expression + // MultiplicativeExpression + > left: + Expression "*" Expression [left] + | Expression "/" Expression [left] + | Expression "%" Expression [left] + // AdditiveExpression + > left: + Expression "+" Expression [left] + | Expression "-" Expression [left] + // ShiftExpression + > left: + Expression "<<" Expression [left] + | Expression ">>" Expression [left] + | Expression ">>>" Expression [left] + // RelationalExpression + > left: + Expression "<" Expression [left] + | Expression ">" Expression [left] + | Expression "<=" Expression [left] + | Expression ">=" Expression [left] + | Expression "instanceof" Expression [left,prefer] + | Expression "in" Expression [left, klabel('_in_::Expression*Expression->Expression)] + // EqualityExpression + > left: + Expression "==" Expression [left] + | Expression "!=" Expression [left] + | Expression "===" Expression [left] + | Expression "!==" Expression [left] + // BitwiseANDExpression + > left: + Expression "&" Expression [left] + // BitwiseXORExpression + > left: + Expression "^" Expression [left] + // BitwiseORExpression + > left: + Expression "|" Expression [left] + // LogicalANDExpression + > left: + Expression "&&" Expression [left] + // LogicalORExpression + > left: + Expression "||" Expression [left] + // ConditionalExpression + > Expression "?" Expression ":" Expression + // AssignmentExpression + > right: + LeftHandSideExpression "=" Expression [right] + | LeftHandSideExpression "*=" Expression [right] + | LeftHandSideExpression "/=" Expression [right] + | LeftHandSideExpression "%=" Expression [right] + | LeftHandSideExpression "+=" Expression [right] + | LeftHandSideExpression "-=" Expression [right] + | LeftHandSideExpression "<<=" Expression [right] + | LeftHandSideExpression ">>=" Expression [right] + | LeftHandSideExpression ">>>=" Expression [right] + | LeftHandSideExpression "&=" Expression [right] + | LeftHandSideExpression "^=" Expression [right] + | LeftHandSideExpression "|=" Expression [right] + +// AssignmentExpression +syntax Expression ::= YieldExpression + | ArrowFunction + +syntax Expression ::= Expression "," Expression [left] + +////////////////////////////////////////////////////////////////////// +// A.3 Statements +////////////////////////////////////////////////////////////////////// + +// StatementList, FunctionBody, FunctionStatementList, GeneratorBody +syntax Statements ::= List{Statement, ""} + +// StatementListItem +syntax Statement ::= +/* BlockStatement, Block */ "{" Statements "}" /* StatementList */ +/* EmptyStatement */ | ";" +/* ExpressionStatement */ | Expression ";" +/* IfStatement */ | "if" "(" Expression ")" Statement "else" Statement + | "if" "(" Expression ")" Statement +/* IterationStatement, BreakableStatement */ + | "do" Statement "while" "(" Expression ")" ";" + | "while" "(" Expression ")" Statement + // for + | "for" "(" ExpressionOpt ";" ExpressionOpt ";" ExpressionOpt ")" Statement + | "for" "(" LexicalDeclaration ExpressionOpt ";" ExpressionOpt ")" Statement + // for-in + | "for" "(" LeftHandSideExpression "in" Expression ")" Statement + | "for" "(" LexicalDeclaration "in" Expression ")" Statement /* ForDeclaration, ForBinding */ + // for-of + | "for" "(" LeftHandSideExpression "of" Expression ")" Statement /* AssignmentExpression */ + | "for" "(" LexicalDeclaration "of" Expression ")" Statement /* ForDeclaration, ForBinding */ /* AssignmentExpression */ +/* ContinueStatement */ | "continue" ";" + | "continue" Identifier ";" /* LabelIdentifier */ +/* BreakStatement */ | "break" ";" + | "break" Identifier ";" /* LabelIdentifier */ +/* ReturnStatement */ | "return" ";" + | "return" Expression ";" +/* WithStatement */ | "with" "(" Expression ")" Statement +/* LabelledStatement */ | Identifier ":" Statement /* LabelIdentifier */ /* LabelledItem */ [klabel('_:_::Name*Statement->Statement)] +/* ThrowStatement */ | "throw" Expression ";" +/* TryStatement */ | "try" "{" Statements "}" "catch" "(" Binding ")" "{" Statements "}" /* CatchParameter */ + | "try" "{" Statements "}" "{" Statements "}" "finally" "{" Statements "}" + | "try" "{" Statements "}" "catch" "(" Binding ")" "{" Statements "}" "finally" "{" Statements "}" /* CatchParameter */ +/* DebuggerStatement */ | "debugger" ";" +/* SwitchStatement, BreakableStatement */ + | "switch" "(" Expression ")" "{" CaseClauses "}" /* CaseBlock */ + | "switch" "(" Expression ")" "{" CaseClauses DefaultClause CaseClauses "}" /* CaseBlock */ +syntax CaseClauses ::= List{CaseClause, ""} [klabel('__::CaseClause*CaseClauses->CaseClauses)] +syntax CaseClause ::= "case" Expression ":" Statements /* StatementList */ +syntax DefaultClause ::= "default" ":" Statements /* StatementList */ + +// Declaration, StatementListItem +syntax Statement ::= Function /* FunctionDeclaration */ /* HoistableDeclaration */ + | Generator /* GeneratorDeclaration */ /* HoistableDeclaration */ + | Class /* ClassDeclaration */ + | LexicalDeclaration + +// ForDeclaration +syntax LexicalDeclaration ::= "var" Bindings ";" /* VariableStatement */ + | "let" Bindings ";" /* LetOrConst */ + | "const" Bindings ";" /* LetOrConst */ + +// BindingList, VariableDeclarationList, FormalsList +syntax Bindings ::= List{Binding, ","} + +// LexicalBinding, VariableDeclaration, BindingElement, ForBinding, CatchParameter, FormalParameter, PropertySetParameterList +syntax Binding ::= SingleNameBinding + | DestructiveBinding +// CoverInitializedName, SingleNameBinding +syntax SingleNameBinding ::= Identifier "=" Expression /* Initializer */ /* BindingIdentifier */ // NOTE: not allowed in ForBinding and CatchParameter + | Identifier /* BindingIdentifier */ +syntax DestructiveBinding ::= BindingPattern "=" Expression /* Initializer */ // NOTE: not allowed in ForBinding and CatchParameter + | BindingPattern // NOTE: not allowed in LexicalBinding and VariableDeclaration + +syntax BindingPattern ::= "{" BindingProperties "}" /* ObjectBindingPattern */ // TODO: a trailing comma option + | "[" BindingOptsWithRest "]" /* ArrayBindingPattern */ + +// BindingPropertyList +syntax BindingProperties ::= List{BindingProperty, ","} +syntax BindingProperty ::= SingleNameBinding + | PropertyName ":" Binding /* BindingElement */ + +// NOTE: different with BindingsWithRest +syntax BindingOptsWithRest ::= "..." Identifier /* BindingRestElement */ + | BindingOpts /* BindingElementList */ + | BindingOpts "," "..." Identifier /* BindingElementList */ /* BindingRestElement */ + +// BindingElementList // NOTE: Bindings with Elision +syntax BindingOpts ::= List{BindingOpt, ","} +// BindingElisionElement // NOTE: Binding + Elision +syntax BindingOpt ::= Binding /* BindingElement */ + | "" /* Elision */ [avoid, onlyLabel, klabel('epsilonBinding)] + +////////////////////////////////////////////////////////////////////// +// A.4 Functions and Classes +////////////////////////////////////////////////////////////////////// + +// FunctionDeclaration, FunctionExpression +syntax Function ::= "function" Identifier "(" BindingsWithRest ")" "{" Statements "}" /* BindingIdentifier */ /* FormalParameters */ /* FunctionBody */ + | "function" "(" BindingsWithRest ")" "{" Statements "}" /* FormalParameters */ /* FunctionBody */ + +// StrictFormalParameters, FormalParameters, FormalParameterList // NOTE: different with BindingOptsWithRest +syntax BindingsWithRest ::= "..." Identifier /* FunctionRestParameter */ + | Bindings + | Bindings "," "..." Identifier /* FunctionRestParameter */ + +// ArrowParameters, ConciseBody, ArrowFormalParameters +syntax ArrowFunction ::= Identifier "=>" Expression /* BindingIdentifier */ /* AssignmentExpression */ + | Identifier "=>" "{" Statements "}" /* BindingIdentifier */ /* FunctionBody */ + | "(" BindingsWithRest ")" "=>" Expression /* CoverParenthesizedExpressionAndArrowParameterList, FormalParameters */ /* AssignmentExpression */ + | "(" BindingsWithRest ")" "=>" "{" Statements "}" /* CoverParenthesizedExpressionAndArrowParameterList, FormalParameters */ /* FunctionBody */ + +syntax MethodDefinition ::= PropertyName "(" BindingsWithRest ")" "{" Statements "}" /* FormalParameters */ /* FunctionBody */ + | "*" PropertyName "(" BindingsWithRest ")" "{" Statements "}" /* GeneratorMethod */ /* FormalParameters */ /* GeneratorBody */ + // accessor + | "get" PropertyName "(" ")" "{" Statements "}" /* FunctionBody */ + | "set" PropertyName "(" Binding ")" "{" Statements "}" /* PropertySetParameterList */ /* FunctionBody */ + +// GeneratorDeclaration, GeneratorExpression +syntax Generator ::= "function" "*" Identifier "(" BindingsWithRest ")" "{" Statements "}" /* BindingIdentifier */ /* FormalParameters */ /* GeneratorBody */ + | "function" "*" "(" BindingsWithRest ")" "{" Statements "}" /* FormalParameters */ /* GeneratorBody */ + +syntax YieldExpression ::= "yield" + | "yield" Expression /* AssignmentExpression */ + | "yield" "*" Expression /* AssignmentExpression */ + +// ClassDeclaration, ClassExpression, ClassTail +syntax Class ::= "class" Identifier "extends" LeftHandSideExpression "{" ClassElements "}" /* BindingIdentifier */ /* ClassHeritage */ /* ClassBody */ + | "class" Identifier "{" ClassElements "}" /* BindingIdentifier */ /* ClassBody */ + | "class" "extends" LeftHandSideExpression "{" ClassElements "}" /* ClassHeritage */ /* ClassBody */ + | "class" "{" ClassElements "}" /* ClassBody */ +// ClassBody, ClassElementList +syntax ClassElements ::= List{ClassElement, ""} +syntax ClassElement ::= MethodDefinition + | "static" MethodDefinition + +////////////////////////////////////////////////////////////////////// +// A.5 Scripts and Modules +////////////////////////////////////////////////////////////////////// + +syntax Program ::= Script + | Module + +// ScriptBody +syntax Script ::= Statements + +// ModuleBody +syntax Module ::= ModuleItems + +// ModuleItemList +syntax ModuleItems ::= List{ModuleItem, ""} + +syntax ModuleItem ::= ImportDeclaration + | ExportDeclaration + | Statement + +syntax ImportDeclaration ::= "import" Identifier "from" ModuleSpecifier ";" /* ImportClause */ /* ImportedDefaultBinding, ImportedBinding, BindingIdentifier */ /* FromClause */ + | "import" "*" "as" Identifier "from" ModuleSpecifier ";" /* ImportClause */ /* NameSpaceImport */ /* ImportedBinding, BindingIdentifier */ /* FromClause */ + | "import" Identifier "," "*" "as" Identifier "from" ModuleSpecifier ";" /* ImportClause */ /* ImportedDefaultBinding */ /* NameSpaceImport */ /* ImportedBinding, BindingIdentifier */ /* FromClause */ + | "import" "{" ImportExportSpecifiers "}" "from" ModuleSpecifier ";" /* ImportClause */ /* NamedImports */ /* ImportsList */ /* TODO: a trailing comma option */ /* FromClause */ + | "import" Identifier "," "{" ImportExportSpecifiers "}" "from" ModuleSpecifier ";" /* ImportClause */ /* ImportedDefaultBinding */ /* NamedImports */ /* ImportsList */ /* TODO: a trailing comma option */ /* FromClause */ + | "import" ModuleSpecifier ";" + +// ImportsList, ExportsList +syntax ImportExportSpecifiers ::= List{ImportExportSpecifier, ","} +// ImportSpecifier, ExportSpecifier +syntax ImportExportSpecifier ::= Identifier /* ImportedBinding for ImportSpecifier */ /* IdentifierName for ExportSpecifier */ + | Identifier "as" Identifier /* IdentifierName */ /* ImportedBinding for ImportSpecifier */ /* IdentifierName for ExportSpecifier */ + +syntax ModuleSpecifier ::= String // TODO: StringLiteral + +syntax ExportDeclaration ::= "export" "*" "from" ModuleSpecifier ";" /* FromClause */ + | "export" "{" ImportExportSpecifiers "}" "from" ModuleSpecifier ";" /* ExportClause */ /* TODO: a trailing comma option */ /* FromClause */ + | "export" "{" ImportExportSpecifiers "}" ";" /* ExportClause */ /* TODO: a trailing comma option */ + // + | "export" Function /* FunctionDeclaration */ /* Declaration */ + | "export" Generator /* GeneratorDeclaration */ /* Declaration */ + | "export" Class /* ClassDeclaration */ /* Declaration */ + | "export" LexicalDeclaration /* VariableStatement */ /* Declaration */ + | "export" "default" Function /* FunctionDeclaration */ /* HoistableDeclaration */ + | "export" "default" Generator /* GeneratorDeclaration */ /* HoistableDeclaration */ + | "export" "default" Class /* ClassDeclaration */ + | "export" "default" Expression /* AssignmentExpression */ + +endmodule + +/* + array, spread element, rest element, destructive binding + + In array expression (i.e., Elements), a spread element "... e" is supposed to be flattened. + e.g., a = [1,2,3]; + b = [10,20,...a,30]; // [10,20,1,2,3,30] + c = [10, ,...a,30]; // [10,undefined,1,2,3,30] + A list of arguments (i.e., Arguments) is also a kind of array expression, but do not allow elision. + e.g., foo(1,2,3); + foo(1, ,3); // invalid + + In binding, two kinds of binding declaration: + - var, let, const declaration: only a list of bindings (i.e., Bindings) + - formal parameters: a list of bindings with optional rest elements "... x" (i.e., BindingsWithRest) + In both bindings, + array pattern destructive binding is also a list of bindings with optional rest elements, + but the list of bindings can have elision. (i.e., BindingOptsWithRest) + e.g., let x, y, z; // only a list of bindings + function foo(x, y, z, ...w) { e; } // a list of bindings with rest element + let [x,y,z,...w] = e; // array pattern with rest element + let [x, ,z,...w] = e; // array pattern with elision and rest element + That is, + - declaration (Bindings) and formal parameters (BindingsWithRest) are same except rest elements + - formal parameters (BindingsWithRest) and array pattern (BindingOptsWithRest) are same except elision + */ diff --git a/es6/tests/programs/arr.js b/es6/tests/programs/arr.js new file mode 100644 index 0000000..d89d5e3 --- /dev/null +++ b/es6/tests/programs/arr.js @@ -0,0 +1,2 @@ +//a = new Array(); +var a = [1, 2, 3]; diff --git a/es6/tests/programs/asgn.js b/es6/tests/programs/asgn.js new file mode 100644 index 0000000..55826ed --- /dev/null +++ b/es6/tests/programs/asgn.js @@ -0,0 +1 @@ +x += y; diff --git a/es6/tests/programs/bool.js b/es6/tests/programs/bool.js new file mode 100644 index 0000000..32f7866 --- /dev/null +++ b/es6/tests/programs/bool.js @@ -0,0 +1 @@ +var yes = true; diff --git a/es6/tests/programs/break.js b/es6/tests/programs/break.js new file mode 100644 index 0000000..ee35daf --- /dev/null +++ b/es6/tests/programs/break.js @@ -0,0 +1,9 @@ +var x,i=0; +for (i=0;i<10;i++) + { + if (i==3) + { + break; + } + x*=i; + } diff --git a/es6/tests/programs/continue.js b/es6/tests/programs/continue.js new file mode 100644 index 0000000..893c306 --- /dev/null +++ b/es6/tests/programs/continue.js @@ -0,0 +1,9 @@ +var x,i=0; +for (i=0;i<10;i++) + { + if (i==3) + { + continue; + } + x*=i; + } diff --git a/es6/tests/programs/dowhile.js b/es6/tests/programs/dowhile.js new file mode 100644 index 0000000..4066128 --- /dev/null +++ b/es6/tests/programs/dowhile.js @@ -0,0 +1,7 @@ +var x,i=0; +do + { + x*=i; + i++; + } +while (i<5) diff --git a/es6/tests/programs/float.js b/es6/tests/programs/float.js new file mode 100644 index 0000000..957fc1b --- /dev/null +++ b/es6/tests/programs/float.js @@ -0,0 +1 @@ +var pi = 3.14; diff --git a/es6/tests/programs/for.js b/es6/tests/programs/for.js new file mode 100644 index 0000000..e0498e0 --- /dev/null +++ b/es6/tests/programs/for.js @@ -0,0 +1,5 @@ +var x,i; +for (i=0;i<5;i++) +{ + x *= i; +} diff --git a/es6/tests/programs/forin.js b/es6/tests/programs/forin.js new file mode 100644 index 0000000..05c091f --- /dev/null +++ b/es6/tests/programs/forin.js @@ -0,0 +1,8 @@ +var x; +var txt=""; +var person={fname:"John",lname:"Doe",age:25}; + +for (x in person) +{ +txt=txt + person[x]; +} diff --git a/es6/tests/programs/func.js b/es6/tests/programs/func.js new file mode 100644 index 0000000..f53095f --- /dev/null +++ b/es6/tests/programs/func.js @@ -0,0 +1,16 @@ +function declaredTwice() { +} + + +function main(a, b) { + undeclared(); +} + +function unused(c) { +} + +function declaredTwice() { +} +/* +main(); +*/ diff --git a/es6/tests/programs/func2.js b/es6/tests/programs/func2.js new file mode 100644 index 0000000..6a34fbf --- /dev/null +++ b/es6/tests/programs/func2.js @@ -0,0 +1,6 @@ +function myFunction() +{ +return ("Hello world!"); +} + +myFunction(); diff --git a/es6/tests/programs/func3.js b/es6/tests/programs/func3.js new file mode 100644 index 0000000..1a23ee2 --- /dev/null +++ b/es6/tests/programs/func3.js @@ -0,0 +1,6 @@ +function myFunction(a,b) +{ +return a*b; +} + +myFunction(3,5); diff --git a/es6/tests/programs/if.js b/es6/tests/programs/if.js new file mode 100644 index 0000000..bed5900 --- /dev/null +++ b/es6/tests/programs/if.js @@ -0,0 +1,6 @@ +if ( true ) { + false; +} else { + false; +} + diff --git a/es6/tests/programs/multipvar.js b/es6/tests/programs/multipvar.js new file mode 100644 index 0000000..266ebd7 --- /dev/null +++ b/es6/tests/programs/multipvar.js @@ -0,0 +1 @@ +var cat, dog; diff --git a/es6/tests/programs/null.js b/es6/tests/programs/null.js new file mode 100644 index 0000000..1228bd0 --- /dev/null +++ b/es6/tests/programs/null.js @@ -0,0 +1 @@ +cars = null; diff --git a/es6/tests/programs/person.js b/es6/tests/programs/person.js new file mode 100644 index 0000000..1774518 --- /dev/null +++ b/es6/tests/programs/person.js @@ -0,0 +1,5 @@ +//person=new Object(); +person.firstname="John"; +person.lastname="Doe"; +person.age=50; +person.eyecolor="blue"; diff --git a/es6/tests/programs/postfix.js b/es6/tests/programs/postfix.js new file mode 100644 index 0000000..a70ed01 --- /dev/null +++ b/es6/tests/programs/postfix.js @@ -0,0 +1 @@ +y++; diff --git a/es6/tests/programs/prefix.js b/es6/tests/programs/prefix.js new file mode 100644 index 0000000..ecb1a10 --- /dev/null +++ b/es6/tests/programs/prefix.js @@ -0,0 +1 @@ +++y; diff --git a/es6/tests/programs/string.js b/es6/tests/programs/string.js new file mode 100644 index 0000000..d448d29 --- /dev/null +++ b/es6/tests/programs/string.js @@ -0,0 +1 @@ +var name = "cansu"; diff --git a/es6/tests/programs/switch.js b/es6/tests/programs/switch.js new file mode 100644 index 0000000..1d5e980 --- /dev/null +++ b/es6/tests/programs/switch.js @@ -0,0 +1,25 @@ +var x, d = 6; +switch (d) + { + case 0: +   x="Today it's Sunday"; +   break; + case 1: +   x="Today it's Monday"; +   break; + case 2: +   x="Today it's Tuesday"; +   break; + case 3: +   x="Today it's Wednesday"; +   break; + case 4: +   x="Today it's Thursday"; +   break; + case 5: +   x="Today it's Friday"; +   break; + case 6: +   x="Today it's Saturday"; +   break; + } diff --git a/es6/tests/programs/trycatch.js b/es6/tests/programs/trycatch.js new file mode 100644 index 0000000..06832b7 --- /dev/null +++ b/es6/tests/programs/trycatch.js @@ -0,0 +1,15 @@ +//?? + +function message() +{ +try + { + adddlert("Welcome guest!"); + } +catch(err) + { + txt="There was an error on this page.\n\n"; + txt+="Error description: " + err.message + "\n\n"; + txt+="Click OK to continue.\n\n"; + } +} diff --git a/es6/tests/programs/var.js b/es6/tests/programs/var.js new file mode 100644 index 0000000..36759b9 --- /dev/null +++ b/es6/tests/programs/var.js @@ -0,0 +1 @@ +var person; diff --git a/es6/tests/programs/while.js b/es6/tests/programs/while.js new file mode 100644 index 0000000..8708f9c --- /dev/null +++ b/es6/tests/programs/while.js @@ -0,0 +1,7 @@ +var x = 5; +var y = 0; + +while(y < 7){ + x = y; + y++; +} diff --git a/es6/tests/regressiontest/empty_array.js b/es6/tests/regressiontest/empty_array.js new file mode 100644 index 0000000..6dcf356 --- /dev/null +++ b/es6/tests/regressiontest/empty_array.js @@ -0,0 +1 @@ +arr = []; diff --git a/es6/tests/regressiontest/empty_stmt.js b/es6/tests/regressiontest/empty_stmt.js new file mode 100644 index 0000000..3e4d7ea --- /dev/null +++ b/es6/tests/regressiontest/empty_stmt.js @@ -0,0 +1,5 @@ +function f() +{ + 1; +} +; diff --git a/es6/tests/regressiontest/escape_char.js b/es6/tests/regressiontest/escape_char.js new file mode 100644 index 0000000..33c2936 --- /dev/null +++ b/es6/tests/regressiontest/escape_char.js @@ -0,0 +1 @@ +"\U"; diff --git a/es6/tests/regressiontest/get_attribute.js b/es6/tests/regressiontest/get_attribute.js new file mode 100644 index 0000000..cd3eaaa --- /dev/null +++ b/es6/tests/regressiontest/get_attribute.js @@ -0,0 +1,7 @@ + Object.defineProperty(arr, "0", { + get : (function () + { + supportsArrayIndexGettersOnArrays = true; + return 0; + }) + }); diff --git a/es6/tests/regressiontest/lexp1.js b/es6/tests/regressiontest/lexp1.js new file mode 100644 index 0000000..46e6eb9 --- /dev/null +++ b/es6/tests/regressiontest/lexp1.js @@ -0,0 +1 @@ +div.find(".text").html(width + " %"); diff --git a/es6/tests/regressiontest/new_complex.js b/es6/tests/regressiontest/new_complex.js new file mode 100644 index 0000000..0bc5ebf --- /dev/null +++ b/es6/tests/regressiontest/new_complex.js @@ -0,0 +1 @@ +new C(x).y(z); diff --git a/es6/tests/regressiontest/new_exp.js b/es6/tests/regressiontest/new_exp.js new file mode 100644 index 0000000..f0e4165 --- /dev/null +++ b/es6/tests/regressiontest/new_exp.js @@ -0,0 +1 @@ +throw new Error("Test '" + path + "'failed: " + error); diff --git a/es6/tests/regressiontest/new_id.js b/es6/tests/regressiontest/new_id.js new file mode 100644 index 0000000..7b91dee --- /dev/null +++ b/es6/tests/regressiontest/new_id.js @@ -0,0 +1,4 @@ +function J() +{ + return (new Date).getTime(); +} diff --git a/es6/tests/regressiontest/regexp.js b/es6/tests/regressiontest/regexp.js new file mode 100644 index 0000000..add1e8a --- /dev/null +++ b/es6/tests/regressiontest/regexp.js @@ -0,0 +1,5 @@ +/^[^<]*(<[\w\W]+>)[^>]*$|^#([\w-]+)$/; +/^.[^:#\[\.,]*$/; +/\S/; +/^(\s|\u00A0)+|(\s|\u00A0)+$/g; +/^<(\w+)\s*\/?>(?:<\/\1>)?$/; diff --git a/es6/tests/regressiontest/str.js b/es6/tests/regressiontest/str.js new file mode 100644 index 0000000..a634bcf --- /dev/null +++ b/es6/tests/regressiontest/str.js @@ -0,0 +1,2 @@ +'.pro'; +".pro"; diff --git a/js-main.k b/js-main.k index c6f2294..bff932e 100644 --- a/js-main.k +++ b/js-main.k @@ -112,7 +112,8 @@ syntax KItem ::= "@pseudo" "(" K "," Map ")" // 8.8 The List Specification Type syntax Vals ::= "@Cons" "(" Val "," Vals ")" | "@Nil" -syntax Val ::= UndefinedType // "Undefined" // 8.1 The Undefined Type +syntax Val ::= UserVal +syntax UserVal ::= UndefinedType // "Undefined" // 8.1 The Undefined Type | NullType // "@NullVal" // 8.2 The Null Type | Primitive | Oid @@ -1627,6 +1628,7 @@ rule GetIdentifierReference(E:Eid,N:Var,Strict:Bool) E' _ +// when E =/=K @NullEid // NOTE: Redundant: there is no with @NullEid as // 10.2.2.2 NewDeclarativeEnvironment (E) @@ -1643,7 +1645,6 @@ rule NewDeclarativeEnvironment(E:Eid, Strict:Bool) => @e(!N) ... _ - // 10.2.2.3 NewObjectEnvironment (O, E) syntax KItem /* Eid */ ::= "NewObjectEnvironment" "(" K /* Oid */ "," K /* Eid */ "," K /* Bool */ "," K /* Bool */ ")" [seqstrict] @@ -4135,8 +4136,6 @@ syntax Int ::= "@MAX_INT" rule @MAX_INT => 4294967296 /* 2^32 */ [macro] rule @MIN_INT => -4294967296 /* 2^32 */ [macro] -syntax UserVal ::= UndefinedType | NullType | Primitive | Oid - endmodule module JS diff --git a/kjs.sh b/kjs.sh index f7e5cc9..eba2d00 100755 --- a/kjs.sh +++ b/kjs.sh @@ -7,7 +7,7 @@ trap cleanup INT TERM for i in "$@"; do "$dir"/jsmassage.sh -f "$i" >"$tmp".js && \ - krun -d "$dir" --pattern-matching --output-file "$tmp".out "$tmp".js && \ + krun -d "$dir" --output-file "$tmp".out "$tmp".js && \ if [ "`sed -n '//,/<\/k>/{ p }' "$tmp".out | tr -d ' \n'`" = "@Normal" ]; then cleanup else diff --git a/normal-completion-configuration.txt b/normal-completion-configuration.txt new file mode 100644 index 0000000..bdd1146 --- /dev/null +++ b/normal-completion-configuration.txt @@ -0,0 +1,3 @@ + + @Normal + diff --git a/test262-coverage/Makefile b/test262-coverage/Makefile index e6837e9..0c461da 100644 --- a/test262-coverage/Makefile +++ b/test262-coverage/Makefile @@ -13,7 +13,7 @@ test262-core-coverage: $(TEST262_CORE_COVERAGE:%=%.coverage) define krun-test262 ( cat ../prelude.js $(1) >$(1).prelude && \ ../jsmassage.sh -f $(1).prelude >$(1).prelude.massage && \ - krun -d ../ --pattern-matching --coverage-file $(CURDIR)/$(1).cov $(1).prelude.massage >$(1).out 2>$(1).err && \ + krun -d ../ --coverage-file $(CURDIR)/$(1).cov $(1).prelude.massage >$(1).out 2>$(1).err && \ test "`sed -n '//,/<\/k>/{ p }' $(1).out | tr -d ' \n'`" = "@Normal"; \ echo $$? >$(1).exitcode ) endef diff --git a/verification/Makefile b/verification/Makefile index 2a173b0..5448bfd 100644 --- a/verification/Makefile +++ b/verification/Makefile @@ -1,8 +1,5 @@ SHELL=/bin/bash -K?=../k -K_Z3=$(K)/k-distribution/include/z3 - .PHONY: all all: build prove @@ -12,26 +9,56 @@ build: clean kompile -d patterns/tree_float --no-prelude --backend java --main-module JS-VERIFIER --syntax-module JS-SYNTAX patterns/tree_float/js-verifier.k kompile -d patterns/list --no-prelude --backend java --main-module JS-VERIFIER --syntax-module JS-SYNTAX patterns/list/js-verifier.k +.PHONY: list +list: + @echo "List" + krun -d patterns/list --smt none --prove list/head_spec.k list/list.js + krun -d patterns/list --smt none --prove list/tail_spec.k list/list.js + krun -d patterns/list --smt none --prove list/add_spec.k list/list.js + krun -d patterns/list --smt none --prove list/swap_spec.k list/list.js +# krun -d patterns/list --smt none --prove list/length_recursive_spec.k list/list.js +# krun -d patterns/list --smt none --prove list/length_iterative_spec.k list/list.js +# krun -d patterns/list --smt none --prove list/sum_recursive_spec.k list/list.js +# krun -d patterns/list --smt none --prove list/sum_iterative_spec.k list/list.js + krun -d patterns/list --smt none --prove list/reverse_spec.k list/list.js + krun -d patterns/list --smt none --prove list/append_spec.k list/list.js +# krun -d patterns/list --smt none --prove list/copy.k list/list.js + +.PHONY: list-smt +list-smt: + @echo "List" + krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/head_spec.k list/list.js + krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/tail_spec.k list/list.js + krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/add_spec.k list/list.js + krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/swap_spec.k list/list.js +# krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/length_recursive_spec.k list/list.js +# krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/length_iterative_spec.k list/list.js +# krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/sum_recursive_spec.k list/list.js +# krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/sum_iterative_spec.k list/list.js + krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/reverse_spec.k list/list.js + krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/append_spec.k list/list.js +# krun -d patterns/list --smt_prelude patterns/list/list.smt2 --prove list/copy.k list/list.js + .PHONY: prove prove: @echo "List" - krun -d patterns/list --smt none --prove list/reverse_spec.k list/reverse.js - krun -d patterns/list --smt none --prove list/append_spec.k list/append.js + krun -d patterns/list --smt none --prove list/reverse_spec.k list/reverse.js + krun -d patterns/list --smt none --prove list/append_spec.k list/append.js @echo "BST String" - krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst/string_find_spec.k bst/find.js - krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst/string_insert_spec.k bst/insert.js - krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst/string_delete_spec.k bst/delete.js + krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_find_spec.k bst/find.js + krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_insert_spec.k bst/insert.js + krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_delete_spec.k bst/delete.js @echo "BST OOP String" - krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst-oop/bst_find_spec.k bst-oop/bst.js - krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst-oop/bst_insert_spec.k bst-oop/bst.js + krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst-oop/bst_find_spec.k bst-oop/bst.js + krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst-oop/bst_insert_spec.k bst-oop/bst.js @echo "BST Float" - krun -d patterns/tree_float --smt_prelude $(K_Z3)/float.smt2 --prove bst/float_find_spec.k bst/find.js - krun -d patterns/tree_float --smt_prelude $(K_Z3)/float.smt2 --prove bst/float_insert_spec.k bst/insert.js - krun -d patterns/tree_float --smt_prelude $(K_Z3)/float.smt2 --prove bst/float_delete_spec.k bst/delete.js + krun -d patterns/tree_float --smt_prelude patterns/tree_float/float.smt2 --prove bst/float_find_spec.k bst/find.js + krun -d patterns/tree_float --smt_prelude patterns/tree_float/float.smt2 --prove bst/float_insert_spec.k bst/insert.js + krun -d patterns/tree_float --smt_prelude patterns/tree_float/float.smt2 --prove bst/float_delete_spec.k bst/delete.js @echo "AVL String" - krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove avl/avl_find_spec.k avl/avl.js - krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove avl/avl_insert_spec.k avl/avl.js - krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove avl/avl_delete_spec.k avl/avl.js + krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_find_spec.k avl/avl.js + krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_insert_spec.k avl/avl.js + krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_delete_spec.k avl/avl.js .PHONY: clean clean: diff --git a/verification/bst-visitor/bst.js b/verification/bst-visitor/bst.js new file mode 100644 index 0000000..2fc2763 --- /dev/null +++ b/verification/bst-visitor/bst.js @@ -0,0 +1,69 @@ +BST = function () { +}; + +BST.prototype.root = null; + +BST.prototype.insert = function (v) { + if (this.root == null) { + this.root = new BST.Node(v); + return; + } + this.traverse(function (current) { + var next = null; + if (v < current.value) { + next = current.left; + if (current.left == null) { + current.left = new BST.Node(v); + } + } else if (v > current.value) { + next = current.right; + if (current.right == null) { + current.right = new BST.Node(v); + } + } + return next; + }); +}; + +BST.prototype.find = function (v) { + var found = false; + this.traverse(function (current) { + var next = null; + if (v < current.value) { + next = current.left; + } else if (v > current.value) { + next = current.right; + } else { + found = true; + } + return next; + }); + return found; +}; + +BST.prototype.traverse = function (f) { + var current = this.root; + while (current) { + current = f.call(this, current); + } +}; + + +BST.Node = function (v) { + this.value = v; +}; + +BST.Node.prototype.left = null; + +BST.Node.prototype.right = null; + + +// var t = new BST(); +// t.insert(2); +// t.insert(1); +// t.insert(3); +// console.log(t); +// console.log(t.find(1)); +// console.log(t.find(2)); +// console.log(t.find(3)); +// console.log(t.find(4)); diff --git a/verification/bst-visitor/bst_find_spec.k b/verification/bst-visitor/bst_find_spec.k new file mode 100644 index 0000000..2407a32 --- /dev/null +++ b/verification/bst-visitor/bst_find_spec.k @@ -0,0 +1,31 @@ +require "../patterns/tree_string/js-verifier.k" + +module BST-SPEC +imports JS-VERIFIER + +rule + + ... + ENVS:Bag + (.Bag => ?_:Bag) + ... + + + ... + OBJS:Bag + tree(O)(T:StringTree)(@o(10)) + (.Bag => ?_:Bag) + ... + + + Call(@o(5), O:Oid, @Cons(V:String, @Nil)) + => + V inStringSet tree_keys(T) + ... + + requires bst(T) + +// @o(10): BST.Node.prototype +// @o(5) : BST.prototype.find + +endmodule diff --git a/verification/list/add_spec.k b/verification/list/add_spec.k new file mode 100644 index 0000000..c43e6e7 --- /dev/null +++ b/verification/list/add_spec.k @@ -0,0 +1,26 @@ +require "../patterns/list/js-verifier.k" + +module ADD-SPEC +imports JS-VERIFIER + +rule + ... + ENVS:Bag + (.Bag => ?_:Bag) + ... + ... + (list(O)(L:List) => list(?O2)(ListItem(V) L)) + OBJS:Bag + (.Bag => ?_:Bag) + ... + + Call( + @o(6), // %var("add"), + Undefined, + @Cons(V:UserVal, @Cons(O:NullableObject, @Nil)) + ) + => + ?O2:NullableObject + ... + +endmodule diff --git a/verification/list/append_spec.k b/verification/list/append_spec.k index 5057ff1..b1606bc 100644 --- a/verification/list/append_spec.k +++ b/verification/list/append_spec.k @@ -66,7 +66,7 @@ rule [func-spec]: Call( // %var("append"), - @o(2), + @o(20), Undefined, @Cons(OX:NullableObject, @Cons(OY:NullableObject, @Nil))) => diff --git a/verification/list/head_spec.k b/verification/list/head_spec.k new file mode 100644 index 0000000..7ce7515 --- /dev/null +++ b/verification/list/head_spec.k @@ -0,0 +1,26 @@ +require "../patterns/list/js-verifier.k" + +module HEAD-SPEC +imports JS-VERIFIER + +rule + ... + ENVS:Bag + (.Bag => ?_:Bag) + ... + ... + list(@o(O:Int))(ListItem(V:UserVal) _:List) + OBJS:Bag + (.Bag => ?_:Bag) + ... + + Call( + // %var("head"), + @o(2), + Undefined, + @Cons(@o(O:Int), @Nil)) + => + V + ... + +endmodule diff --git a/verification/list/length_recursive_spec.k b/verification/list/length_recursive_spec.k new file mode 100644 index 0000000..3b995f8 --- /dev/null +++ b/verification/list/length_recursive_spec.k @@ -0,0 +1,27 @@ +require "../patterns/list/js-verifier.k" + +module LENGTH-RECURSIVE-SPEC +imports JS-VERIFIER + +rule + ... + ENVS:Bag + (.Bag => ?_:Bag) + ... + ... + list(O)(L:List) + OBJS:Bag + (.Bag => ?_:Bag) + ... + + Call( + @o(10), // %var("length_recursive"), + Undefined, + @Cons(O:NullableObject, @Nil) + ) + => + size(L) + ... + requires size(L) Call( // %var("reverse"), - @o(2), + @o(18), Undefined, @Cons(O1:NullableObject, @Nil)) => diff --git a/verification/list/swap_spec.k b/verification/list/swap_spec.k new file mode 100644 index 0000000..94574ac --- /dev/null +++ b/verification/list/swap_spec.k @@ -0,0 +1,30 @@ +require "../patterns/list/js-verifier.k" + +module SWAP-SPEC +imports JS-VERIFIER + +rule + ... + ENVS:Bag + (.Bag => ?_:Bag) + ... + ... + ( + list(O)(ListItem(V1:UserVal) ListItem(V2:UserVal) L:List) + => + list(?O2)(ListItem(V2) ListItem(V1) L) + ) + OBJS:Bag + (.Bag => ?_:Bag) + ... + + Call( + @o(8), // %var("swap"), + Undefined, + @Cons(O:NullableObject, @Nil) + ) + => + ?O2:NullableObject + ... + +endmodule diff --git a/verification/list/tail_spec.k b/verification/list/tail_spec.k new file mode 100644 index 0000000..4277e13 --- /dev/null +++ b/verification/list/tail_spec.k @@ -0,0 +1,38 @@ +require "../patterns/list/js-verifier.k" + +module TAIL-SPEC +imports JS-VERIFIER + +rule + ... + ENVS:Bag + (.Bag => ?_:Bag) + ... + ... + + @o(O:Int) + + "value" |-> @desc("Value" |-> _:UserVal "Writable" |-> true "Enumerable" |-> true "Configurable" |-> true) + "next" |-> @desc("Value" |-> Tail:NullableObject "Writable" |-> true "Enumerable" |-> true "Configurable" |-> true) + + + "Class" |-> "Object" + "Extensible" |-> true + "Prototype" |-> @ObjectProtoOid + + + list(Tail)(L:List) + OBJS:Bag + (.Bag => ?_:Bag) + ... + + Call( + // %var("tail"), + @o(4), + Undefined, + @Cons(@o(O:Int), @Nil)) + => + Tail + ... + +endmodule diff --git a/verification/patterns/list/list.smt2 b/verification/patterns/list/list.smt2 new file mode 100644 index 0000000..8195cf1 --- /dev/null +++ b/verification/patterns/list/list.smt2 @@ -0,0 +1,42 @@ +(set-option :auto-config false) +(set-option :smt.mbqi false) + +; int extra +(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x)) +(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y)) +(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x)) + +; bool to int +(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0)) + +; set axioms +(declare-sort IntSet) + +(declare-fun smt_set_cup (IntSet IntSet) IntSet) +(declare-fun smt_set_ele (Int) IntSet) +(declare-fun smt_set_emp () IntSet) +(declare-fun smt_set_mem (Int IntSet) Bool) + +(declare-fun smt_set_lt ((IntSet) (IntSet)) Bool) +(declare-fun smt_set_le ((IntSet) (IntSet)) Bool) + +; sequence axioms +(declare-sort IntSeq) + +(declare-fun smt_seq_concat (IntSeq IntSeq) IntSeq) +(declare-fun smt_seq_elem (Int) IntSeq) +(declare-fun smt_seq_nil () IntSeq) +(declare-fun smt_seq_len (IntSeq) Int) + +(declare-fun smt_seq2set (IntSeq) IntSet) +(declare-fun smt_seq_sorted (IntSeq) Bool) + +(assert (forall ((s1 IntSeq) (s2 IntSeq)) (! (= (smt_seq_sorted (smt_seq_concat s1 s2)) (and (smt_set_le (smt_seq2set s1) (smt_seq2set s2)) (smt_seq_sorted s1) (smt_seq_sorted s2))) + :pattern ((smt_seq_sorted (smt_seq_concat s1 s2))) + :pattern ((smt_seq_sorted s1) (smt_seq_sorted s2)) +))) + +(assert (forall ((e1 Int) (e2 Int) (s1 IntSeq) (s2 IntSeq)) (= (= (smt_seq_concat (smt_seq_elem e1) s1) (smt_seq_concat (smt_seq_elem e2) s2)) (and (= e1 e2) (= s1 s2))))) + +(declare-fun smt_seq_filter (Int IntSeq) IntSeq) +(assert (forall ((v Int) (e Int)) (= (smt_seq_filter v (smt_seq_elem e)) (ite (= v e) smt_seq_nil (smt_seq_elem e))))) diff --git a/verification/patterns/list/list_pattern.k b/verification/patterns/list/list_pattern.k index 087f18f..ff6f739 100644 --- a/verification/patterns/list/list_pattern.k +++ b/verification/patterns/list/list_pattern.k @@ -2,16 +2,46 @@ module LIST-PATTERN imports MAP imports JS + rule size(L1:List L2:List) => size(L1) +Int size(L2) [lemma] + rule size(ListItem(_)) => 1 [lemma] + rule size(.List) => 0 [lemma] + + syntax Int ::= sum(List) [function, smtlib(smt_seq_sum)] +/* + rule sum(L1:List L2:List) => sum(L1) +Int sum(L2) [lemma] + rule sum(ListItem(I:Int)) => I [lemma] + rule sum(.List) => 0 [lemma] +*/ + syntax List ::= rev(List) [function] rule rev(L1:List L2:List) => rev(L2) rev(L1) [lemma] - rule rev(ListItem(V:Val)) => ListItem(V) [lemma] + rule rev(ListItem(V:UserVal)) => ListItem(V) [lemma] rule rev(.List) => .List [lemma] +/* + syntax IntSet ::= list2set(List) [function, smtlib(smt_seq2set)] + rule list2set(L1:List L2:List) => list2set(L1) U list2set(L2) + [lemma, smt-lemma] + rule list2set(ListItem(V:UserVal)) => { V } [lemma, smt-lemma] + rule list2set(.List) => .IntSet [lemma, smt-lemma] +*/ + + syntax Bool ::= sorted(List) [function, smtlib(smt_seq_sorted)] +/* + // TODO(AndreiS): add support for specifying Z3 triggers + //rule sorted(L1 @ L2) + // => intseq2intset(L1) <=IntSet intseq2intset(L2) andBool sorted(L1) andBool sorted(L2) + // [smt-lemma] + rule sorted(ListItem(I)) => true [smt-lemma] + rule sorted(.List) => true [smt-lemma] +*/ + + /* list pattern */ syntax Bag ::= "list" "(" Val ")" "(" List ")" [pattern(1)] rule ... - list(@o(O:Int))(ListItem(V:Val) L:List) + list(@o(O:Int))(ListItem(V:UserVal) L:List) => @o(O) @@ -35,7 +65,7 @@ module LIST-PATTERN syntax Bag ::= "lseg" "(" Val "," Val ")" "(" List ")" [pattern(2)] rule ... - lseg(@o(O:Int), P:NullableObject)(ListItem(V:Val) L:List) + lseg(@o(O:Int), P:NullableObject)(ListItem(V:UserVal) L:List) => @o(O) diff --git a/verification/patterns/tree_float/float.smt2 b/verification/patterns/tree_float/float.smt2 new file mode 100644 index 0000000..3ad37eb --- /dev/null +++ b/verification/patterns/tree_float/float.smt2 @@ -0,0 +1,35 @@ +; floats as uninterpreted with a partial order relation +(declare-sort Float) +(declare-fun float_nan () Float) +(declare-fun float_zero () Float) + +(declare-fun float_lt (Float Float) Bool) +; transitivity +(assert (forall ((x1 Float) (x2 Float) (x3 Float)) (implies (and (float_lt x1 x2) (float_lt x2 x3)) (float_lt x1 x3)))) +; irreflexivity +(assert (forall ((x1 Float) (x2 Float)) (not (and (float_lt x1 x2) (float_lt x2 x1))))) +; total order without nan +(assert (forall ((x1 Float) (x2 Float)) (implies (and (not (= x1 float_nan)) (not (= x2 float_nan))) (or (float_lt x1 x2) (= x1 x2) (float_lt x2 x1))))) +; nan +(assert (forall ((x Float)) (and (not (float_lt x float_nan)) (not (float_lt float_nan x))))) + +(define-fun float_le ((x1 Float) (x2 Float)) Bool (or (float_lt x1 x2) (= x1 x2))) +(define-fun float_gt ((x1 Float) (x2 Float)) Bool (float_lt x2 x1)) +(define-fun float_ge ((x1 Float) (x2 Float)) Bool (float_le x2 x1)) + +(define-fun float_max ((x Float) (y Float)) Float (ite (float_lt x y) y x)) +(define-fun float_min ((x Float) (y Float)) Float (ite (float_lt x y) x y)) + +; float sets as arrays +(define-sort FloatSet () (Array Float Bool)) +(define-fun float_set_mem ((x Float) (s FloatSet)) Bool (select s x)) +(define-fun float_set_add ((s FloatSet) (x Float)) FloatSet (store s x true)) +(define-fun float_set_emp () FloatSet ((as const FloatSet) false)) +(define-fun float_set_cup ((s1 FloatSet) (s2 FloatSet)) FloatSet ((_ map or) s1 s2)) +(define-fun float_set_cap ((s1 FloatSet) (s2 FloatSet)) FloatSet ((_ map and) s1 s2)) +(define-fun float_set_com ((s FloatSet)) FloatSet ((_ map not) s)) +(define-fun float_set_ele ((x Float)) FloatSet (float_set_add float_set_emp x)) +(define-fun float_set_dif ((s1 FloatSet) (s2 FloatSet)) FloatSet (float_set_cap s1 (float_set_com s2))) +(define-fun float_set_sub ((s1 FloatSet) (s2 FloatSet)) Bool (= float_set_emp (float_set_dif s1 s2))) +(define-fun float_set_lt ((s1 FloatSet) (s2 FloatSet)) Bool (forall ((i Float) (j Float)) (implies (and (select s1 i) (select s2 j)) (float_lt i j)))) +(define-fun float_set_le ((s1 FloatSet) (s2 FloatSet)) Bool (forall ((i Float) (j Float)) (implies (and (select s1 i) (select s2 j)) (float_le i j)))) diff --git a/verification/patterns/tree_string/string.smt2 b/verification/patterns/tree_string/string.smt2 new file mode 100644 index 0000000..9e15fb1 --- /dev/null +++ b/verification/patterns/tree_string/string.smt2 @@ -0,0 +1,43 @@ +; strings as uninterpreted with a total order relation +(declare-sort String) + +(declare-fun string_lt (String String) Bool) +; transitivity +(assert (forall ((x1 String) (x2 String) (x3 String)) (implies (and (string_lt x1 x2) (string_lt x2 x3)) (string_lt x1 x3)))) +; irreflexivity +(assert (forall ((x1 String) (x2 String)) (not (and (string_lt x1 x2) (string_lt x2 x1))))) +; total order +(assert (forall ((x1 String) (x2 String)) (or (string_lt x1 x2) (= x1 x2) (string_lt x2 x1)))) + +(define-fun string_le ((x1 String) (x2 String)) Bool (or (string_lt x1 x2) (= x1 x2))) +(define-fun string_gt ((x1 String) (x2 String)) Bool (string_lt x2 x1)) +(define-fun string_ge ((x1 String) (x2 String)) Bool (string_le x2 x1)) + +; string sets as arrays +(define-sort StringSet () (Array String Bool)) +(define-fun string_set_mem ((x String) (s StringSet)) Bool (select s x)) +(define-fun string_set_add ((s StringSet) (x String)) StringSet (store s x true)) +(define-fun string_set_emp () StringSet ((as const StringSet) false)) +(define-fun string_set_cup ((s1 StringSet) (s2 StringSet)) StringSet ((_ map or) s1 s2)) +(define-fun string_set_cap ((s1 StringSet) (s2 StringSet)) StringSet ((_ map and) s1 s2)) +(define-fun string_set_com ((s StringSet)) StringSet ((_ map not) s)) +(define-fun string_set_ele ((x String)) StringSet (string_set_add string_set_emp x)) +(define-fun string_set_dif ((s1 StringSet) (s2 StringSet)) StringSet (string_set_cap s1 (string_set_com s2))) +(define-fun string_set_sub ((s1 StringSet) (s2 StringSet)) Bool (= string_set_emp (string_set_dif s1 s2))) +(define-fun string_set_lt ((s1 StringSet) (s2 StringSet)) Bool (forall ((i String) (j String)) (implies (and (select s1 i) (select s2 j)) (string_lt i j)))) +(define-fun string_set_le ((s1 StringSet) (s2 StringSet)) Bool (forall ((i String) (j String)) (implies (and (select s1 i) (select s2 j)) (string_le i j)))) + +; sequence axioms +(declare-sort IntSeq) +(declare-fun smt_seq_concat (IntSeq IntSeq) IntSeq) +(declare-fun smt_seq_elem (Int) IntSeq) +(declare-fun smt_seq_nil () IntSeq) + +; int extra +(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x)) +(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y)) +(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x)) + +; bool to int +(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0)) + diff --git a/verification/verification.out b/verification/verification.out index 2e490c9..b78d811 100644 --- a/verification/verification.out +++ b/verification/verification.out @@ -3,46 +3,46 @@ kompile -d patterns/tree_float --no-prelude --backend java --main-module JS-VER kompile -d patterns/list --no-prelude --backend java --main-module JS-VERIFIER --syntax-module JS-SYNTAX patterns/list/js-verifier.k List -krun -d patterns/list --smt none --prove list/reverse_spec.k list/reverse.js +krun -d patterns/list --smt none --prove list/reverse_spec.k list/reverse.js true -krun -d patterns/list --smt none --prove list/append_spec.k list/append.js +krun -d patterns/list --smt none --prove list/append_spec.k list/append.js true BST String -krun -d patterns/tree_string --smt_prelude ../k/k-distribution/include/z3/string.smt2 --prove bst/string_find_spec.k bst/find.js +krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_find_spec.k bst/find.js true -krun -d patterns/tree_string --smt_prelude ../k/k-distribution/include/z3/string.smt2 --prove bst/string_insert_spec.k bst/insert.js +krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_insert_spec.k bst/insert.js true -krun -d patterns/tree_string --smt_prelude ../k/k-distribution/include/z3/string.smt2 --prove bst/string_delete_spec.k bst/delete.js +krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_delete_spec.k bst/delete.js true BST OOP String -krun -d patterns/tree_string --smt_prelude ../k/k-distribution/include/z3/string.smt2 --prove bst-oop/bst_find_spec.k bst-oop/bst.js +krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst-oop/bst_find_spec.k bst-oop/bst.js true -krun -d patterns/tree_string --smt_prelude ../k/k-distribution/include/z3/string.smt2 --prove bst-oop/bst_insert_spec.k bst-oop/bst.js +krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst-oop/bst_insert_spec.k bst-oop/bst.js true BST Float -krun -d patterns/tree_float --smt_prelude ../k/k-distribution/include/z3/float.smt2 --prove bst/float_find_spec.k bst/find.js +krun -d patterns/tree_float --smt_prelude patterns/tree_float/float.smt2 --prove bst/float_find_spec.k bst/find.js true -krun -d patterns/tree_float --smt_prelude ../k/k-distribution/include/z3/float.smt2 --prove bst/float_insert_spec.k bst/insert.js +krun -d patterns/tree_float --smt_prelude patterns/tree_float/float.smt2 --prove bst/float_insert_spec.k bst/insert.js true -krun -d patterns/tree_float --smt_prelude ../k/k-distribution/include/z3/float.smt2 --prove bst/float_delete_spec.k bst/delete.js +krun -d patterns/tree_float --smt_prelude patterns/tree_float/float.smt2 --prove bst/float_delete_spec.k bst/delete.js true AVL String -krun -d patterns/tree_string --smt_prelude ../k/k-distribution/include/z3/string.smt2 --prove avl/avl_find_spec.k avl/avl.js +krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_find_spec.k avl/avl.js true -krun -d patterns/tree_string --smt_prelude ../k/k-distribution/include/z3/string.smt2 --prove avl/avl_insert_spec.k avl/avl.js +krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_insert_spec.k avl/avl.js true -krun -d patterns/tree_string --smt_prelude ../k/k-distribution/include/z3/string.smt2 --prove avl/avl_delete_spec.k avl/avl.js +krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_delete_spec.k avl/avl.js true