diff options
| author |  Jason Koenig <unknown> | 2011-07-14 18:09:44 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-14 18:09:44 -0700 |
| commit | 7ec320357c190999921d44cd404e2c1b87691b57 (patch) | |
| tree | e0e59e5befbf2cddb48d3d2fb46c609c4a80edcf | |
| parent | dd37b19e4afcb2d9475894d48c48e6a8308ec0a0 (diff) | |
| parent | a90b5d1fdf92e9f17eb8da23348d93bbbe46b88d (diff) | |
Merge
37 files changed, 1936 insertions, 843 deletions
diff --git a/BCT/BytecodeTranslator/Phone/PhoneTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneTraverser.cs index 98aa4461..5f4680a8 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneTraverser.cs @@ -12,10 +12,10 @@ using Microsoft.Cci; using Microsoft.Cci.MetadataReader;
using Microsoft.Cci.MutableCodeModel;
using Microsoft.Cci.Contracts;
-using Microsoft.Cci.ILToCodeModel;
using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
+using TranslationPlugins;
namespace BytecodeTranslator {
@@ -23,28 +23,235 @@ namespace BytecodeTranslator { /// <summary>
/// Traverse code looking for phone specific points of interest, possibly injecting necessary code in-between
/// </summary>
-
public class PhoneCodeTraverser : BaseCodeTraverser {
private readonly IMethodDefinition methodBeingTraversed;
- private static bool initializationEncountered;
+ private static bool initializationFound= false;
+ private PhoneControlsPlugin phonePlugin;
+ private MetadataReaderHost host;
+
+ private IAssemblyReference coreAssemblyRef;
+ private IAssemblyReference phoneAssembly;
+ private IAssemblyReference phoneSystemWindowsAssembly;
+ private INamespaceTypeReference checkBoxType;
+ private INamespaceTypeReference radioButtonType;
+ private INamespaceTypeReference buttonType;
+ private INamespaceTypeReference buttonBaseType;
+ private INamespaceTypeReference toggleButtonType;
+ private INamespaceTypeReference controlType;
+ private INamespaceTypeReference uiElementType;
+
+ private CompileTimeConstant trueConstant;
+ private CompileTimeConstant falseConstant;
- public PhoneCodeTraverser(IMethodDefinition traversedMethod) : base() {
+ private IMethodReference isEnabledSetter;
+ private IMethodReference isEnabledGetter;
+ private IMethodReference isCheckedSetter;
+ private IMethodReference isCheckedGetter;
+ private IMethodReference visibilitySetter;
+ private IMethodReference visibilityGetter;
+ private IMethodReference clickHandlerAdder;
+ private IMethodReference clickHandlerRemover;
+ private IMethodReference checkedHandlerAdder;
+ private IMethodReference checkedHandlerRemover;
+ private IMethodReference uncheckedHandlerAdder;
+ private IMethodReference uncheckedHandlerRemover;
+
+ private ITypeReference getTypeForClassname(String classname) {
+ if (classname == "Button") {
+ return buttonType;
+ } else if (classname == "RadioButton") {
+ return radioButtonType;
+ } else if (classname == "CheckBox") {
+ return checkBoxType;
+ } else {
+ // TODO avoid throwing exceptions, just log
+ throw new NotImplementedException("Type " + classname + " is not being monitored yet for phone controls");
+ }
+ }
+
+ public PhoneCodeTraverser(MetadataReaderHost host, IMethodDefinition traversedMethod, PhoneControlsPlugin phonePlugin) : base() {
this.methodBeingTraversed = traversedMethod;
+ this.phonePlugin = phonePlugin;
+ this.host = host;
+ InitializeTraverser();
+ }
+
+ private void InitializeTraverser() {
+ Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+ coreAssemblyRef = platform.CoreAssemblyRef;
+
+ // TODO obtain version, culture and signature data dynamically
+ AssemblyIdentity MSPhoneAssemblyId =
+ new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
+ new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+ AssemblyIdentity MSPhoneSystemWindowsAssemblyId =
+ new AssemblyIdentity(host.NameTable.GetNameFor("System.Windows"), coreAssemblyRef.Culture, coreAssemblyRef.Version,
+ coreAssemblyRef.PublicKeyToken, "");
+
+ phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
+ phoneSystemWindowsAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);
+
+ // TODO determine the needed types dynamically
+ checkBoxType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "CheckBox");
+ radioButtonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "RadioButton");
+ buttonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Button");
+ buttonBaseType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Primitives", "ButtonBase");
+ toggleButtonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Primitives", "ToggleButton");
+ controlType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Control");
+ uiElementType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "UIElement");
+
+ trueConstant = new CompileTimeConstant() {
+ Type = platform.SystemBoolean,
+ Value = true
+ };
+ falseConstant = new CompileTimeConstant() {
+ Type = platform.SystemBoolean,
+ Value = false
+ };
+
+ IEnumerable<IPropertyDefinition> controlProperties = controlType.ResolvedType.Properties;
+ IEnumerable<IPropertyDefinition> toggleButtonProperties = toggleButtonType.ResolvedType.Properties;
+ IEnumerable<IPropertyDefinition> uiElementProperties = uiElementType.ResolvedType.Properties;
+
+ IPropertyDefinition prop = controlProperties.Single(p => p.Name.Value == "IsEnabled");
+ isEnabledSetter = prop.Setter;
+ isEnabledGetter = prop.Getter;
+ prop = toggleButtonProperties.Single(p => p.Name.Value == "IsChecked");
+ isCheckedSetter = prop.Setter;
+ isCheckedGetter = prop.Getter;
+ prop = uiElementProperties.Single(p => p.Name.Value == "Visibility");
+ visibilitySetter = prop.Setter;
+ visibilityGetter = prop.Getter;
+
+ IEnumerable<IEventDefinition> buttonBaseEvents = buttonBaseType.ResolvedType.Events;
+ IEnumerable<IEventDefinition> toggleButtonEvents = toggleButtonType.ResolvedType.Events;
+ IEventDefinition evt = buttonBaseEvents.Single(e => e.Name.Value == "Click");
+ clickHandlerAdder = evt.Adder;
+ clickHandlerRemover = evt.Remover;
+ evt = toggleButtonEvents.Single(e => e.Name.Value == "Checked");
+ checkedHandlerAdder = evt.Adder;
+ checkedHandlerRemover = evt.Remover;
+ evt = toggleButtonEvents.Single(e => e.Name.Value == "Unchecked");
+ uncheckedHandlerAdder = evt.Adder;
+ uncheckedHandlerRemover = evt.Remover;
}
public void injectPhoneControlsCode(BlockStatement block) {
this.Visit(block);
}
- private void injectPhoneInitializationCode(IBlockStatement block, IStatement statementAfter) {
+ private Assignment MakeFieldAssigment(string assignType, string objectName, string objectType, string fieldName, string sourceObjName, string sourceObjType, string sourceObjFieldName) {
+ /* TODO */
+ return null;
+ }
+
+ private void injectPhoneInitializationCode(BlockStatement block, Statement statementAfter) {
+ // TODO check page name against container name
+ IEnumerable<ControlInfoStructure> controls= phonePlugin.getControlsForPage(methodBeingTraversed.Container.ToString());
+ IEnumerable<IStatement> injectedStatements = new List<IStatement>();
+ foreach (ControlInfoStructure controlInfo in controls) {
+ injectedStatements = injectedStatements.Concat(getCodeForSettingEnabledness(controlInfo));
+ injectedStatements = injectedStatements.Concat(getCodeForSettingCheckedState(controlInfo));
+ injectedStatements = injectedStatements.Concat(getCodeForSettingVisibility(controlInfo));
+ injectedStatements = injectedStatements.Concat(getCodeForSettingEventHandlers(controlInfo, "Click"));
+ injectedStatements = injectedStatements.Concat(getCodeForSettingEventHandlers(controlInfo, "Checked"));
+ injectedStatements = injectedStatements.Concat(getCodeForSettingEventHandlers(controlInfo, "Unchecked"));
+ }
+
+ int stmtPos= block.Statements.IndexOf(statementAfter);
+ block.Statements.InsertRange(stmtPos+1, injectedStatements);
+ }
+
+ private BoundExpression makeBoundControlFromControlInfo(ControlInfoStructure controlInfo) {
+ return new BoundExpression() {
+ Definition = new FieldDefinition() {
+ ContainingTypeDefinition = methodBeingTraversed.Container,
+ Name = host.NameTable.GetNameFor(controlInfo.Name),
+ Type = getTypeForClassname(controlInfo.ClassName),
+ IsStatic = false,
+ },
+ Instance = new ThisReference() { Type = methodBeingTraversed.Container },
+ };
+ }
+
+ private IEnumerable<IStatement> getCodeForSettingVisibility(ControlInfoStructure controlInfo) {
+ // TODO I do not want to import System.Windows into this project...and using the underlying uint won't work
+ /*
+ IList<IStatement> code = new List<IStatement>();
+ BoundExpression boundControl = makeBoundControlFromControlInfo(controlInfo);
+ MethodCall setVisibilityCall= new MethodCall() {
+ IsStaticCall = false,
+ IsVirtualCall = true,
+ IsTailCall = false,
+ Type = ((Microsoft.Cci.Immutable.PlatformType) host.PlatformType).SystemVoid,
+ MethodToCall = visibilitySetter,
+ ThisArgument = boundControl,
+ };
+
+ ITypeReference visibilityType= ((Microsoft.Cci.Immutable.PlatformType) host.PlatformType).CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Visibility");
+
+ switch (controlInfo.Visible) {
+ case Visibility.Visible:
+ setVisibilityCall.Arguments.Add(new CompileTimeConstant() {
+ Type = visibilityType,
+ Value = 0,
+ } ); // Visible
+ break;
+ case Visibility.Collapsed:
+ setVisibilityCall.Arguments.Add(new CompileTimeConstant() {
+ Type = visibilityType,
+ Value = 1,
+ } ); // Collapsed
+ break;
+ default:
+ throw new ArgumentException("Invalid visibility value for control " + controlInfo.Name + ": " + controlInfo.Visible);
+ }
+
+ ExpressionStatement callStmt = new ExpressionStatement() {
+ Expression = setVisibilityCall,
+ };
+ code.Add(callStmt);
+ return code;
+ * */
+ return new List<IStatement>();
+ }
+
+ private IEnumerable<IStatement> getCodeForSettingEnabledness(ControlInfoStructure controlInfo) {
+ IList<IStatement> code = new List<IStatement>();
+ BoundExpression boundControl = makeBoundControlFromControlInfo(controlInfo);
+ MethodCall setEnablednessCall = new MethodCall() {
+ IsStaticCall = false,
+ IsVirtualCall = true,
+ IsTailCall = false,
+ Type = ((Microsoft.Cci.Immutable.PlatformType) host.PlatformType).SystemVoid,
+ MethodToCall = isEnabledSetter,
+ ThisArgument = boundControl,
+ };
+
+ setEnablednessCall.Arguments.Add(controlInfo.IsEnabled ? trueConstant : falseConstant);
+ ExpressionStatement callStmt = new ExpressionStatement() {
+ Expression = setEnablednessCall,
+ };
+ code.Add(callStmt);
+ return code;
+ }
+
+ private IEnumerable<IStatement> getCodeForSettingCheckedState(ControlInfoStructure controlInfo) {
+ // TODO not implemented yet
+ return new List<IStatement>();
+ }
+
+ private IEnumerable<IStatement> getCodeForSettingEventHandlers(ControlInfoStructure controlInfo, string eventName) {
+ // TODO not implemented yet
+ return new List<IStatement>();
}
public override void Visit(IBlockStatement block) {
- initializationEncountered = false;
foreach (IStatement statement in block.Statements) {
this.Visit(statement);
- if (initializationEncountered) {
- injectPhoneInitializationCode(block, statement);
+ if (initializationFound) {
+ injectPhoneInitializationCode(block as BlockStatement, statement as Statement);
+ initializationFound = false;
break;
}
}
@@ -57,8 +264,7 @@ namespace BytecodeTranslator { methodCall.Arguments.Any())
return;
- // otherwise we need to insert the desired code after this call
- // TODO make sure I am dealing with the MUTABLE code model
+ initializationFound= true;
}
}
@@ -66,9 +272,13 @@ namespace BytecodeTranslator { /// Traverse metadata looking only for PhoneApplicationPage's constructors
/// </summary>
public class PhoneMetadataTraverser : BaseMetadataTraverser {
+ private PhoneControlsPlugin phoneControlsInfo;
+ private MetadataReaderHost host;
- public PhoneMetadataTraverser()
+ public PhoneMetadataTraverser(PhoneControlsPlugin phonePlugin, MetadataReaderHost host)
: base() {
+ this.phoneControlsInfo = phonePlugin;
+ this.host = host;
}
public override void Visit(IModule module) {
@@ -113,8 +323,8 @@ namespace BytecodeTranslator { if (!method.IsConstructor)
return;
- PhoneCodeTraverser codeTraverser = new PhoneCodeTraverser(method);
- var methodBody = method.Body as ISourceMethodBody;
+ PhoneCodeTraverser codeTraverser = new PhoneCodeTraverser(host, method, phoneControlsInfo);
+ var methodBody = method.Body as SourceMethodBody;
if (methodBody == null)
return;
var block = methodBody.Block as BlockStatement;
diff --git a/BCT/BytecodeTranslator/Phone/stubs.bpl b/BCT/BytecodeTranslator/Phone/stubs.bpl new file mode 100644 index 00000000..caa8210b --- /dev/null +++ b/BCT/BytecodeTranslator/Phone/stubs.bpl @@ -0,0 +1,328 @@ +// BEGIN INJECTED CODE
+
+procedure UpdateNavigation(uri:Ref);
+implementation UpdateNavigation(uri:Ref) {
+ CurrentNavigationPage := uri;
+}
+
+procedure DriveControls();
+implementation DriveControls() {
+ var isCurrentPage1: bool;
+ var isCurrentPage2: bool;
+ var isCurrentPage3: bool;
+ var isCurrentPage4: bool;
+
+ // TODO there can be parameters in the URI and other stuff that makes this checks quite unreliable
+ call isCurrentPage1 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page1.xaml_0);
+ call isCurrentPage2 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page2.xaml_1);
+ call isCurrentPage3 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page3.xaml_2);
+ call isCurrentPage4 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page4.xaml_3);
+
+ if (isCurrentPage1) {
+ call drivePage1Controls();
+ } else if (isCurrentPage2) {
+ call drivePage2Controls();
+ } else if (isCurrentPage3) {
+ call drivePage3Controls();
+ } else if (isCurrentPage4) {
+ call drivePage4Controls();
+ }
+}
+
+procedure drivePage1Controls();
+implementation drivePage1Controls() {
+ var $continueOnPage: bool;
+ var $activeControl: int;
+ var $control: Ref;
+ var $isEnabledRef: Ref;
+ var $isEnabled: bool;
+
+ $continueOnPage:=true;
+ havoc $activeControl;
+ while ($continueOnPage) {
+ if ($activeControl==0) {
+ // radio1 check
+ $control := SimpleNavigationApp.Page1.radioButton1[$page1];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==1) {
+ // radio2 check
+ $control := SimpleNavigationApp.Page1.radioButton2[$page1];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==2) {
+ // radio3 check
+ $control := SimpleNavigationApp.Page1.radioButton3[$page1];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==3) {
+ //radio4 check
+ $control := SimpleNavigationApp.Page1.radioButton4[$page1];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==4) {
+ //button click
+ $control := SimpleNavigationApp.Page1.btnNavigate[$page1];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call SimpleNavigationApp.Page1.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page1, null, null);
+ $continueOnPage := false;
+ }
+ }
+ }
+}
+
+procedure drivePage2Controls();
+implementation drivePage2Controls() {
+ var $continueOnPage: bool;
+ var $activeControl: int;
+ var $control: Ref;
+ var $isEnabledRef: Ref;
+ var $isEnabled: bool;
+
+ $continueOnPage:=true;
+ havoc $activeControl;
+ while ($continueOnPage) {
+ if ($activeControl==0) {
+ // radio1 check
+ $control := SimpleNavigationApp.Page2.radioButton1[$page2];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==1) {
+ // radio2 check
+ $control := SimpleNavigationApp.Page2.radioButton2[$page2];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==2) {
+ // radio3 check
+ $control := SimpleNavigationApp.Page2.radioButton3[$page2];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==3) {
+ //radio4 check
+ $control := SimpleNavigationApp.Page2.radioButton4[$page2];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==4) {
+ //button click
+ $control := SimpleNavigationApp.Page2.btnNavigate[$page2];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call SimpleNavigationApp.Page2.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page2, null, null);
+ $continueOnPage := false;
+ }
+ }
+ }
+}
+
+procedure drivePage3Controls();
+implementation drivePage3Controls() {
+ var $continueOnPage: bool;
+ var $activeControl: int;
+ var $control: Ref;
+ var $isEnabledRef: Ref;
+ var $isEnabled: bool;
+
+ $continueOnPage:=true;
+ havoc $activeControl;
+ while ($continueOnPage) {
+ if ($activeControl==0) {
+ // radio1 check
+ $control := SimpleNavigationApp.Page3.radioButton1[$page3];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==1) {
+ // radio2 check
+ $control := SimpleNavigationApp.Page3.radioButton2[$page3];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==2) {
+ // radio3 check
+ $control := SimpleNavigationApp.Page3.radioButton3[$page3];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==3) {
+ //radio4 check
+ $control := SimpleNavigationApp.Page3.radioButton4[$page3];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==4) {
+ //button click
+ $control := SimpleNavigationApp.Page3.btnNavigate[$page3];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call SimpleNavigationApp.Page3.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page3, null, null);
+ $continueOnPage := false;
+ }
+ }
+ }
+}
+
+procedure drivePage4Controls();
+implementation drivePage4Controls() {
+ var $continueOnPage: bool;
+ var $activeControl: int;
+ var $control: Ref;
+ var $isEnabledRef: Ref;
+ var $isEnabled: bool;
+
+ $continueOnPage:=true;
+ havoc $activeControl;
+ while ($continueOnPage) {
+ if ($activeControl==0) {
+ // radio1 check
+ $control := SimpleNavigationApp.Page4.radioButton1[$page4];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==1) {
+ // radio2 check
+ $control := SimpleNavigationApp.Page4.radioButton2[$page4];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==2) {
+ // radio3 check
+ $control := SimpleNavigationApp.Page4.radioButton3[$page4];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==3) {
+ //radio4 check
+ $control := SimpleNavigationApp.Page4.radioButton4[$page4];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
+ }
+ } else if ($activeControl==4) {
+ //button click
+ $control := SimpleNavigationApp.Page4.btnNavigate[$page4];
+ call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
+ $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
+ if ($isEnabled) {
+ call SimpleNavigationApp.Page4.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page4, null, null);
+ $continueOnPage := false;
+ }
+ }
+ }
+}
+
+var $page1: Ref;
+var $page2: Ref;
+var $page3: Ref;
+var $page4: Ref;
+
+procedure SimpleNavigationApp.Main();
+implementation SimpleNavigationApp.Main() {
+ var $doWork: bool;
+ var $activeControl: int;
+ var $isEnabledRef: Ref;
+ var $isEnabled: bool;
+ var $control: Ref;
+
+ call SimpleNavigationApp.Page1.#ctor($page1);
+ call SimpleNavigationApp.Page2.#ctor($page2);
+ call SimpleNavigationApp.Page3.#ctor($page3);
+ call SimpleNavigationApp.Page4.#ctor($page4);
+ call SimpleNavigationApp.Page1.Page1_Loaded$System.Object$System.Windows.RoutedEventArgs($page1, null, null);
+
+ CurrentNavigationPage := $string_literal_$Page1.xaml_0;
+
+ havoc $doWork;
+ while ($doWork) {
+ call DriveControls();
+ havoc $doWork;
+ }
+}
+
+function isControlEnabled(Ref) : bool;
+function isControlChecked(Ref) : bool;
+
+procedure System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
+procedure System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
+
+implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) {
+ $result := (a$in == b$in);
+}
+
+implementation System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) {
+ $result := (a$in != b$in);
+}
+
+procedure System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);
+implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool) {
+ assume isControlEnabled($this) == value$in;
+}
+
+procedure System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);
+implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref) {
+ var enabledness: bool;
+ enabledness := isControlEnabled($this);
+ $result := Box2Ref(Bool2Box(enabledness));
+}
+
+procedure System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);
+implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref) {
+ var check: bool;
+
+ check := Box2Bool(Ref2Box(value$in));
+ assume isControlChecked($this) == check;
+}
+
+procedure System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);
+implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref) {
+ var isChecked: bool;
+ isChecked := isControlChecked($this);
+ $result := Box2Ref(Bool2Box(isChecked));
+}
+
+var CurrentNavigationPage: Ref;
+var uriToNavigate: Ref;
+
+// END INJECTED CODE
\ No newline at end of file diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 7ce0c37a..28149cbd 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -17,6 +17,7 @@ using Microsoft.Cci.MutableContracts; using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
using Microsoft.Cci.MutableCodeModel.Contracts;
+using TranslationPlugins;
namespace BytecodeTranslator {
@@ -175,7 +176,7 @@ namespace BytecodeTranslator { var primaryModule = modules[0];
if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
- PhoneMetadataTraverser tr = new PhoneMetadataTraverser();
+ PhoneMetadataTraverser tr = new PhoneMetadataTraverser(new PhoneControlsPlugin(phoneControlsConfigFile), host);
tr.InjectPhoneCodeAssemblies(modules);
}
@@ -187,7 +188,6 @@ namespace BytecodeTranslator { Sink sink= new Sink(host, traverserFactory, heapFactory);
TranslationHelper.tmpVarCounter = 0;
-
MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
translator.TranslateAssemblies(modules);
diff --git a/BCT/TranslationPlugins/PhoneControlsPlugin.cs b/BCT/TranslationPlugins/PhoneControlsPlugin.cs index 9ed1c7df..ac017d38 100644 --- a/BCT/TranslationPlugins/PhoneControlsPlugin.cs +++ b/BCT/TranslationPlugins/PhoneControlsPlugin.cs @@ -26,7 +26,7 @@ namespace TranslationPlugins { public string[] ParameterTypes;
}
- class ControlInfoStructure {
+ public class ControlInfoStructure {
public string Name;
public string ClassName;
public bool IsEnabled;
@@ -80,6 +80,10 @@ namespace TranslationPlugins { public void setControlInfo(string controlName, ControlInfoStructure controlInfo) {
controlsInfo[controlName] = controlInfo;
}
+
+ public IEnumerable<ControlInfoStructure> getAllControlsInfo() {
+ return controlsInfo.Values.AsEnumerable();
+ }
}
public class PhoneControlsPlugin : TranslationPlugin {
@@ -186,7 +190,8 @@ namespace TranslationPlugins { }
}
- public void getControlsForPage(string pageClass) {
+ public IEnumerable<ControlInfoStructure> getControlsForPage(string pageClass) {
+ return pageStructureInfo[pageClass].getAllControlsInfo();
}
public string getXAMLForPage(string pageClass) {
diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs index 24b8cbc7..47313465 100644 --- a/Jennisys/Jennisys/Analyzer.fs +++ b/Jennisys/Jennisys/Analyzer.fs @@ -1,317 +1,417 @@ -module Analyzer - -open Ast -open AstUtils -open CodeGen -open DafnyModelUtils -open PipelineUtils -open Options -open Printer -open Resolver -open DafnyPrinter -open Utils - -open Microsoft.Boogie - -let VarsAreDifferent aa bb = - printf "false" - List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb - -let Rename suffix vars = - vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp)) - -let ReplaceName substMap nm = - match Map.tryFind nm substMap with - | Some(Var(name, tp)) -> name - | None -> nm - -let rec Substitute substMap = function - | IdLiteral(s) -> IdLiteral(ReplaceName substMap s) - | Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f) - | UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e) - | BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1) - | SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1) - | UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2) - | SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee) - | SeqLength(e) -> SeqLength(Substitute substMap e) - | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e) - | expr -> expr - -let GenMethodAnalysisCode comp m assertion = - let methodName = GetMethodName m - let signature = GetMethodSig m - let ppre,ppost = GetMethodPrePost m - let pre = Desugar ppre - let post = Desugar ppost - " method " + methodName + "()" + newline + - " modifies this;" + newline + - " {" + newline + - // print signature as local variables - (match signature with - | Sig(ins,outs) -> - List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf " var %s;" (PrintVarDecl vd)) + newline) "") + - " // assume precondition" + newline + - " assume " + (PrintExpr 0 pre) + ";" + newline + - " // assume invariant and postcondition" + newline + - " assume Valid();" + newline + - " assume " + (PrintExpr 0 post) + ";" + newline + - " // assume user defined invariant again because assuming Valid() doesn't always work" + newline + - (GetInvariantsAsList comp |> PrintSep newline (fun e -> " assume " + (PrintExpr 0 e) + ";")) + newline + - // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible - " // assert false to search for a model satisfying the assumed constraints" + newline + - " assert " + (PrintExpr 0 assertion) + ";" + newline + - " }" + newline - -let MethodAnalysisPrinter onlyForThisCompMethod assertion comp mthd = - match onlyForThisCompMethod with - | (c,m) when c = comp && m = mthd -> - match m with - | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp m assertion) + newline - | _ -> "" - | _ -> "" - -let rec IsArgsOnly args expr = - match expr with - | IdLiteral(id) -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false) - | UnaryExpr(_,e) -> IsArgsOnly args e - | BinaryExpr(_,_,e1,e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) - | Dot(e,_) -> IsArgsOnly args e - | SelectExpr(e1, e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) - | UpdateExpr(e1, e2, e3) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) && (IsArgsOnly args e3) - | SequenceExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true - | SeqLength(e) -> IsArgsOnly args e - | ForallExpr(vars,e) -> IsArgsOnly (List.concat [args; vars]) e - | IntLiteral(_) -> true - | Star -> true - -let rec GetUnifications expr args (heap,env,ctx) = - match expr with - | IntLiteral(_) - | IdLiteral(_) - | Star - | Dot(_) - | SelectExpr(_) // TODO: handle select expr - | UpdateExpr(_) // TODO: handle update expr - | SequenceExpr(_) - | SeqLength(_) - | ForallExpr(_) // TODO: handle forall expr - | UnaryExpr(_) -> Set.empty - | BinaryExpr(strength,op,e0,e1) -> - if op = "=" then - let v0 = Eval e0 (heap,env,ctx) - let v1 = Eval e1 (heap,env,ctx) - let argsOnly0 = IsArgsOnly args e0 - let argsOnly1 = IsArgsOnly args e1 - match v0,argsOnly1,argsOnly0,v1 with - | Some(c0),true,_,_ -> - Logger.DebugLine (" - adding unification " + (PrintConst c0) + " <--> " + (PrintExpr 0 e1)); - Set.ofList [c0, e1] - | _,_,true,Some(c1) -> - Logger.DebugLine (" - adding unification " + (PrintConst c1) + " <--> " + (PrintExpr 0 e0)); - Set.ofList [c1, e0] - | _ -> Logger.TraceLine (" - couldn't unify anything from " + (PrintExpr 0 expr)); - Set.empty - else - GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx)) - -let rec GetArgValueUnifications args env = - match args with - | Var(name,_) :: rest -> - match Map.tryFind (VarConst(name)) env with - | Some(c) -> - Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name); - Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env) - | None -> failwith ("couldn't find value for argument " + name) - | [] -> Set.empty - -let rec _GetObjRefExpr o (heap,env,ctx) visited = - if Set.contains o visited then - None - else - let newVisited = Set.add o visited - let refName = PrintObjRefName o (env,ctx) - match refName with - | Exact "this" _ -> Some(IdLiteral(refName)) - | _ -> - let rec __fff lst = - match lst with - | ((o,Var(fldName,_)),l) :: rest -> - match _GetObjRefExpr o (heap,env,ctx) newVisited with - | Some(expr) -> Some(Dot(expr, fldName)) - | None -> __fff rest - | [] -> None - let backPointers = heap |> Map.filter (fun (_,_) l -> l = o) |> Map.toList - __fff backPointers - -let GetObjRefExpr o (heap,env,ctx) = - _GetObjRefExpr o (heap,env,ctx) (Set.empty) - -let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = - let __CheckUnif o f e idx = - let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from this to " + (PrintObjRefName o (env,ctx))) - let fldName = PrintVarName f - let lhs = Dot(objRefExpr, fldName) |> Utils.IfDo1 (not (idx = -1)) (fun e -> SelectExpr(e, IntLiteral(idx))) - let assertionExpr = BinaryEq lhs e - // check if the assertion follows and if so update the env - let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr) - Logger.Debug(" - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ") - CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) - - match unifs with - | (c,e) :: rest -> - let restHeap,env,ctx = UpdateHeapEnv prog comp mthd rest (heap,env,ctx) - let newHeap = restHeap |> Map.fold (fun acc (o,f) l -> - let value = TryResolve l (env,ctx) - if value = c then - if __CheckUnif o f e -1 then - Logger.DebugLine " HOLDS" - // change the value to expression - acc |> Map.add (o,f) (ExprConst(e)) - else - Logger.DebugLine " DOESN'T HOLDS" - // don't change the value - acc |> Map.add (o,f) l - else - // see if it's a list, then try to match its elements, otherwise leave it as is - match value with - | SeqConst(clist) -> - let rec __UnifyOverLst lst cnt = - match lst with - | lstElem :: rest when lstElem = c -> - if __CheckUnif o f e cnt then - Logger.DebugLine " HOLDS" - ExprConst(e) :: __UnifyOverLst rest (cnt+1) - else - Logger.DebugLine " DOESN'T HOLDS" - lstElem :: __UnifyOverLst rest (cnt+1) - | lstElem :: rest -> - lstElem :: __UnifyOverLst rest (cnt+1) - | [] -> [] - let newLstConst = __UnifyOverLst clist 0 - acc |> Map.add (o,f) (SeqConst(newLstConst)) - | _ -> - acc |> Map.add (o,f) l - ) restHeap - (newHeap,env,ctx) - | [] -> (heap,env,ctx) - -let GeneralizeSolution prog comp mthd (heap,env,ctx) = - match mthd with - | Method(mName,Sig(ins, outs),pre,post,_) -> - let args = List.concat [ins; outs] - match args with - | [] -> (heap,env,ctx) - | _ -> - let unifs = GetUnifications (BinaryAnd pre post |> Desugar) args (heap,env,ctx) //TODO: we shouldn't use desugar here, but in UpdateHeapEnv - |> Set.union (GetArgValueUnifications args env) - UpdateHeapEnv prog comp mthd (Set.toList unifs) (heap,env,ctx) - | _ -> failwith ("not a method: " + mthd.ToString()) - -// ==================================================================================== -/// Returns whether the code synthesized for the given method can be verified with Dafny -// ==================================================================================== -let VerifySolution prog comp mthd (heap,env,ctx) = - // print the solution to file and try to verify it with Dafny - let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx) - let code = PrintImplCode prog solution (fun p -> [comp,mthd]) - CheckDafnyProgram code dafnyVerifySuffix - -// ============================================================================ +module Analyzer
+
+open Ast
+open AstUtils
+open CodeGen
+open DafnyModelUtils
+open PipelineUtils
+open Options
+open Printer
+open Resolver
+open DafnyPrinter
+open Utils
+
+open Microsoft.Boogie
+
+let VarsAreDifferent aa bb =
+ printf "false"
+ List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb
+
+let Rename suffix vars =
+ vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))
+
+let ReplaceName substMap nm =
+ match Map.tryFind nm substMap with
+ | Some(Var(name, tp)) -> name
+ | None -> nm
+
+let rec Substitute substMap = function
+ | IdLiteral(s) -> IdLiteral(ReplaceName substMap s)
+ | Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f)
+ | UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e)
+ | BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1)
+ | SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1)
+ | UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2)
+ | SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee)
+ | SeqLength(e) -> SeqLength(Substitute substMap e)
+ | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)
+ | expr -> expr
+
+let GenMethodAnalysisCode comp m assertion =
+ let methodName = GetMethodName m
+ let signature = GetMethodSig m
+ let ppre,ppost = GetMethodPrePost m
+ let pre = Desugar ppre
+ let post = Desugar ppost
+ " method " + methodName + "()" + newline +
+ " modifies this;" + newline +
+ " {" + newline +
+ // print signature as local variables
+ (match signature with
+ | Sig(ins,outs) ->
+ List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf " var %s;" (PrintVarDecl vd)) + newline) "") +
+ " // assume precondition" + newline +
+ " assume " + (PrintExpr 0 pre) + ";" + newline +
+ " // assume invariant and postcondition" + newline +
+ " assume Valid();" + newline +
+ " assume " + (PrintExpr 0 post) + ";" + newline +
+ " // assume user defined invariant again because assuming Valid() doesn't always work" + newline +
+ (GetInvariantsAsList comp |> PrintSep newline (fun e -> " assume " + (PrintExpr 0 e) + ";")) + newline +
+ // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible
+ " // assert false to search for a model satisfying the assumed constraints" + newline +
+ " assert " + (PrintExpr 0 assertion) + ";" + newline +
+ " }" + newline
+
+let MethodAnalysisPrinter onlyForThisCompMethod assertion comp mthd =
+ match onlyForThisCompMethod with
+ | (c,m) when c = comp && m = mthd ->
+ match m with
+ | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp m assertion) + newline
+ | _ -> ""
+ | _ -> ""
+
+let rec IsArgsOnly args expr =
+ match expr with
+ | IntLiteral(_) -> true
+ | BoolLiteral(_) -> true
+ | Star -> true
+ | VarLiteral(id)
+ | IdLiteral(id) -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)
+ | UnaryExpr(_,e) -> IsArgsOnly args e
+ | BinaryExpr(_,_,e1,e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2)
+ | IteExpr(c,e1,e2) -> (IsArgsOnly args c) && (IsArgsOnly args e1) && (IsArgsOnly args e2)
+ | Dot(e,_) -> IsArgsOnly args e
+ | SelectExpr(e1, e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2)
+ | UpdateExpr(e1, e2, e3) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) && (IsArgsOnly args e3)
+ | SequenceExpr(exprs) | SetExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true
+ | SeqLength(e) -> IsArgsOnly args e
+ | ForallExpr(vars,e) -> IsArgsOnly (List.concat [args; vars]) e
+
+let GetUnifications expr args (heap,env,ctx) =
+ // - first looks if the give expression talks only about method arguments (args)
+ // - then checks if it doesn't already exist in the unification map
+ // - then it tries to evaluate it to a constant
+ // - if all of these succeed, it adds a unification rule e <--> val(e) to the given unifMap map
+ let __AddUnif e unifMap =
+ let builder = new CascadingBuilder<_>(unifMap)
+ builder {
+ let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption
+ let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption
+ let! v = try Some(Eval (heap,env,ctx) true e |> Expr2Const) with ex -> None
+ Logger.DebugLine (" - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v));
+ return Map.add e v unifMap
+ }
+ // just recurses on all expressions
+ let rec __GetUnifications expr args unifs =
+ let unifs = __AddUnif expr unifs
+ match expr with
+ | IntLiteral(_)
+ | BoolLiteral(_)
+ | VarLiteral(_)
+ | IdLiteral(_)
+ | Star -> unifs
+ | Dot(e, _)
+ | SeqLength(e)
+ | ForallExpr(_,e)
+ | UnaryExpr(_,e) -> unifs |> __GetUnifications e args
+ | SelectExpr(e1, e2)
+ | BinaryExpr(_,_,e1,e2) -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args
+ | IteExpr(e1,e2,e3)
+ | UpdateExpr(e1, e2, e3) -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args |> __GetUnifications e3 args
+ | SetExpr(elst)
+ | SequenceExpr(elst) -> elst |> List.fold (fun acc e -> acc |> __GetUnifications e args) unifs
+ (* --- function body starts here --- *)
+ __GetUnifications expr args Map.empty
+
+// =======================================================
+/// Returns a map (Expr |--> Const) containing unifications
+/// found for the given method and heap/env/ctx
+// =======================================================
+let GetUnificationsForMethod comp m (heap,env,ctx) =
+ let rec GetArgValueUnifications args env =
+ match args with
+ | Var(name,_) :: rest ->
+ match Map.tryFind (Unresolved(name)) env with
+ | Some(c) ->
+ Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name);
+ Map.ofList [IdLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env)
+ | None -> failwith ("couldn't find value for argument " + name)
+ | [] -> Map.empty
+ (* --- function body starts here --- *)
+ match m with
+ | Method(mName,Sig(ins, outs),pre,post,_) ->
+ let args = List.concat [ins; outs]
+ match args with
+ | [] -> Map.empty
+ | _ -> GetUnifications (BinaryAnd pre post) args (heap,env,ctx)
+ |> Utils.MapAddAll (GetArgValueUnifications args env)
+ | _ -> failwith ("not a method: " + m.ToString())
+
+// =========================================================================
+/// For a given constant "o" (which is an object, something like "gensym32"),
+/// finds a path of field references from "this".
+///
+/// Implements a backtracking search over the heap entries to find that
+/// path. It starts from the given object, and follows the backpointers
+/// until it reaches the root ("this")
+// =========================================================================
+let objRef2ExprCache = new System.Collections.Generic.Dictionary<Const, Expr>()
+let GetObjRefExpr o (heap,env,ctx) =
+ let rec __GetObjRefExpr o (heap,env,ctx) visited =
+ if Set.contains o visited then
+ None
+ else
+ let newVisited = Set.add o visited
+ let refName = PrintObjRefName o (env,ctx)
+ match refName with
+ | "this" -> Some(IdLiteral(refName))
+ | _ ->
+ let rec __fff lst =
+ match lst with
+ | ((o,Var(fldName,_)),l) :: rest ->
+ match __GetObjRefExpr o (heap,env,ctx) newVisited with
+ | Some(expr) -> Some(Dot(expr, fldName))
+ | None -> __fff rest
+ | [] -> None
+ let backPointers = heap |> Map.filter (fun (_,_) l -> l = o) |> Map.toList
+ __fff backPointers
+ (* --- function body starts here --- *)
+ if objRef2ExprCache.ContainsKey(o) then
+ Some(objRef2ExprCache.[o])
+ else
+ let res = __GetObjRefExpr o (heap,env,ctx) (Set.empty)
+ match res with
+ | Some(e) -> objRef2ExprCache.Add(o, e)
+ | None -> ()
+ res
+
+// =======================================================
+/// Applies given unifications onto the given heap/env/ctx
+///
+/// If "conservative" is true, applies only those that
+/// can be verified to hold, otherwise applies all of them
+// =======================================================
+let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative =
+ let __CheckUnif o f e idx =
+ if not conservative || not Options.CONFIG.checkUnifications then
+ true
+ else
+ let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + (PrintObjRefName o (env,ctx)))
+ let fldName = PrintVarName f
+ let lhs = Dot(objRefExpr, fldName)
+ let assertionExpr = match f with
+ | Var(_, Some(SeqType(_))) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e
+ | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs
+ | _ -> BinaryEq lhs e
+ // check if the assertion follows and if so update the env
+ let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr)
+ Logger.Debug (" - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")
+ let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))
+ if ok then
+ Logger.DebugLine " HOLDS"
+ else
+ Logger.DebugLine " DOESN'T HOLD"
+ ok
+ (* --- function body starts here --- *)
+ match unifs with
+ | (e,c) :: rest ->
+ let restHeap,env,ctx = ApplyUnifications prog comp mthd rest (heap,env,ctx) conservative
+ let newHeap = restHeap |> Map.fold (fun acc (o,f) l ->
+ let value = TryResolve (env,ctx) l
+ if value = c then
+ if __CheckUnif o f e -1 then
+ // change the value to expression
+ Logger.TraceLine (sprintf " - applied: %s.%s --> %s" (PrintConst o) (GetVarName f) (PrintExpr 0 e) )
+ acc |> Map.add (o,f) (ExprConst(e))
+ else
+ // don't change the value unless "conservative = false"
+ acc |> Map.add (o,f) l
+ else
+ let rec __UnifyOverLst lst cnt =
+ match lst with
+ | lstElem :: rest when lstElem = c ->
+ if __CheckUnif o f e cnt then
+ Logger.TraceLine (sprintf " - applied: %s.%s[%d] --> %s" (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )
+ ExprConst(e) :: __UnifyOverLst rest (cnt+1)
+ else
+ lstElem :: __UnifyOverLst rest (cnt+1)
+ | lstElem :: rest ->
+ lstElem :: __UnifyOverLst rest (cnt+1)
+ | [] -> []
+ // see if it's a list, then try to match its elements, otherwise leave it as is
+ match value with
+ | SeqConst(clist) ->
+ let newLstConst = __UnifyOverLst clist 0
+ acc |> Map.add (o,f) (SeqConst(newLstConst))
+ | SetConst(cset) ->
+ let newLstConst = __UnifyOverLst (Set.toList cset) 0
+ acc |> Map.add (o,f) (SetConst(newLstConst |> Set.ofList))
+ | _ ->
+ acc |> Map.add (o,f) l
+ ) restHeap
+ (newHeap,env,ctx)
+ | [] -> (heap,env,ctx)
+
+// ====================================================================================
+/// Returns whether the code synthesized for the given method can be verified with Dafny
+// ====================================================================================
+let VerifySolution prog comp mthd (heap,env,ctx) =
+ // print the solution to file and try to verify it with Dafny
+ let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx)
+ let code = PrintImplCode prog solution (fun p -> [comp,mthd])
+ CheckDafnyProgram code dafnyVerifySuffix
+
+let TryInferConditionals prog comp m unifs (heap,env,ctx) =
+ let heap2,env2,ctx2 = ApplyUnifications prog comp m unifs (heap,env,ctx) false
+ // get expressions to evaluate:
+ // - add pre and post conditions
+ // - go through all objects on the heap and assert its invariant
+ let pre,post = GetMethodPrePost m
+ let prepostExpr = post //TODO: do we need the "pre" here as well?
+ let heapObjs = heap |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty
+ let expr = heapObjs |> Set.fold (fun acc o ->
+ let receiverOpt = GetObjRefExpr o (heap,env,ctx)
+ let receiver = Utils.ExtractOption receiverOpt
+ match Resolve (env,ctx) o with
+ | NewObj(_,tOpt) | ThisConst(_,tOpt) ->
+ let t = Utils.ExtractOptionMsg "Type missing for heap object" tOpt
+ let objComp = FindComponent prog (GetTypeShortName t) |> Utils.ExtractOption
+ let objInvs = GetInvariantsAsList objComp
+ let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)
+ objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc
+ | _ -> failwith "not supposed to happen"
+ ) prepostExpr
+ expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "")
+ // now evaluate and see what's left
+ let c = Eval (heap2,env2,ctx2) false expr
+ Some(heap2,env2,ctx2)
+
+// ============================================================================
/// Attempts to synthesize the initialization code for the given constructor "m"
///
-/// Returns a (heap,env,ctx) tuple -// ============================================================================ -let AnalyzeConstructor prog comp m = - let methodName = GetMethodName m - // generate Dafny code for analysis first - let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral) +/// Returns a (heap,env,ctx) tuple
+// ============================================================================
+let AnalyzeConstructor prog comp m =
+ let methodName = GetMethodName m
+ // generate Dafny code for analysis first
+ let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral)
Logger.InfoLine (" [*] analyzing constructor " + methodName + (PrintSig (GetMethodSig m)))
- Logger.Info " - searching for a solution ..." - let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m)) - if models.Count = 0 then - // no models means that the "assert false" was verified, which means that the spec is inconsistent - Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!" - None - else - if models.Count > 1 then - Logger.WarnLine " FAILED " - failwith "internal error (more than one model for a single constructor analysis)" - Logger.InfoLine " OK " - let model = models.[0] - let heap,env,ctx = ReadFieldValuesFromModel model prog comp m - |> GeneralizeSolution prog comp m - if _opt_verifySolutions then - Logger.InfoLine " - verifying synthesized solution ... " - let verified = VerifySolution prog comp m (heap,env,ctx) - Logger.Info " " - if verified then - Logger.InfoLine "~~~ VERIFIED ~~~" - Some(heap,env,ctx) - else - Logger.InfoLine "!!! NOT VERIFIED !!!" - Some(heap,env,ctx) - else - Some(heap,env,ctx) - - -// ============================================================================ -/// Goes through a given list of methods of the given program and attempts to -/// synthesize code for each one of them. -/// -/// Returns a map from (component * method) |--> (heap,env,ctx) -// ============================================================================ -let rec AnalyzeMethods prog members = - match members with - | (comp,m) :: rest -> - match m with - | Method(_,_,_,_,true) -> - let solOpt = AnalyzeConstructor prog comp m - Logger.InfoLine "" - match solOpt with - | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx) - | None -> AnalyzeMethods prog rest - | _ -> AnalyzeMethods prog rest - | [] -> Map.empty - -let Analyze prog filename = - let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) - let progName = System.IO.Path.GetFileNameWithoutExtension(filename) - use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName)) - file.AutoFlush <- true - Logger.InfoLine "Printing synthesized code" - let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze - fprintfn file "%s" synthCode - () - -//let AnalyzeComponent_rustan c = -// match c with -// | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) -> -// let aVars = Fields members -// let aVars0 = Rename "0" aVars -// let aVars1 = Rename "1" aVars -// let allVars = List.concat [aVars; List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars] -// let inv0 = Substitute (Map.ofList aVars0) inv -// let inv1 = Substitute (Map.ofList aVars1) inv -// // Now print it as a Dafny program -// printf "class %s" name -// match typeParams with -// | [] -> () -// | _ -> printf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp)) -// printfn " {" -// // the fields: original abstract fields plus two more copies thereof, plus and concrete fields -// allVars |> List.iter (function Var(nm,None) -> printfn " var %s;" nm | Var(nm,Some(tp)) -> printfn " var %s: %s;" nm (PrintType tp)) -// // the method -// printfn " method %s_checkInjective() {" name -// printf " assume " ; (VarsAreDifferent aVars0 aVars1) ; printfn ";" -// printfn " assume %s;" (PrintExpr 0 inv0) -// printfn " assume %s;" (PrintExpr 0 inv1) -// printfn " assert false;" // {:msg "Two abstract states map to the same concrete state"} -// printfn " }" -// // generate code -// members |> List.iter (function -// | Constructor(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv false) -// | Method(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv true) -// | _ -> ()) -// // the end of the class -// printfn "}" + Logger.Info " - searching for an instance ..."
+ let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))
+ if models.Count = 0 then
+ // no models means that the "assert false" was verified, which means that the spec is inconsistent
+ Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!"
+ None
+ else
+ if models.Count > 1 then
+ Logger.WarnLine " FAILED "
+ failwith "internal error (more than one model for a single constructor analysis)"
+ Logger.InfoLine " OK "
+ let model = models.[0]
+ let heap,env,ctx = ReadFieldValuesFromModel model prog comp m
+ let unifs = GetUnificationsForMethod comp m (heap,env,ctx) |> Map.toList
+ let heap,env,ctx = ApplyUnifications prog comp m unifs (heap,env,ctx) true
+ if Options.CONFIG.verifySolutions then
+ Logger.InfoLine " - verifying synthesized solution ... "
+ let verified = VerifySolution prog comp m (heap,env,ctx)
+ Logger.Info " "
+ if verified then
+ Logger.InfoLine "~~~ VERIFIED ~~~"
+ Some(heap,env,ctx)
+ else
+ Logger.InfoLine "!!! NOT VERIFIED !!!"
+ Logger.InfoLine "Trying to infer conditionals"
+ TryInferConditionals prog comp m unifs (heap,env,ctx)
+ else
+ Some(heap,env,ctx)
+
+let GetMethodsToAnalyze prog =
+ let mOpt = Options.CONFIG.methodToSynth;
+ if mOpt = "*" then
+ (* all *)
+ FilterMembers prog FilterConstructorMembers
+ elif mOpt = "paramsOnly" then
+ (* only with parameters *)
+ FilterMembers prog FilterConstructorMembersWithParams
+ else
+ let allMethods,neg =
+ if mOpt.StartsWith("~") then
+ mOpt.Substring(1), true
+ else
+ mOpt, false
+ (* exactly one *)
+ let methods = allMethods.Split([|','|])
+ let lst = methods |> Array.fold (fun acc m ->
+ let compName = m.Substring(0, m.LastIndexOf("."))
+ let methName = m.Substring(m.LastIndexOf(".") + 1)
+ let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName)
+ let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName)
+ (c,mthd) :: acc
+ ) []
+ if neg then
+ FilterMembers prog FilterConstructorMembers |> List.filter (fun e -> not (Utils.ListContains e lst))
+ else
+ lst
+
+
+// ============================================================================
+/// Goes through a given list of methods of the given program and attempts to
+/// synthesize code for each one of them.
+///
+/// Returns a map from (component * method) |--> (heap,env,ctx)
+// ============================================================================
+let rec AnalyzeMethods prog members =
+ match members with
+ | (comp,m) :: rest ->
+ match m with
+ | Method(_,_,_,_,true) ->
+ let solOpt = AnalyzeConstructor prog comp m
+ Logger.InfoLine ""
+ match solOpt with
+ | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)
+ | None -> AnalyzeMethods prog rest
+ | _ -> AnalyzeMethods prog rest
+ | [] -> Map.empty
+
+let Analyze prog filename =
+ let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)
+ let progName = System.IO.Path.GetFileNameWithoutExtension(filename)
+ use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName))
+ file.AutoFlush <- true
+ Logger.InfoLine "Printing synthesized code"
+ let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze
+ fprintfn file "%s" synthCode
+ ()
+
+//let AnalyzeComponent_rustan c =
+// match c with
+// | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
+// let aVars = Fields members
+// let aVars0 = Rename "0" aVars
+// let aVars1 = Rename "1" aVars
+// let allVars = List.concat [aVars; List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars]
+// let inv0 = Substitute (Map.ofList aVars0) inv
+// let inv1 = Substitute (Map.ofList aVars1) inv
+// // Now print it as a Dafny program
+// printf "class %s" name
+// match typeParams with
+// | [] -> ()
+// | _ -> printf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp))
+// printfn " {"
+// // the fields: original abstract fields plus two more copies thereof, plus and concrete fields
+// allVars |> List.iter (function Var(nm,None) -> printfn " var %s;" nm | Var(nm,Some(tp)) -> printfn " var %s: %s;" nm (PrintType tp))
+// // the method
+// printfn " method %s_checkInjective() {" name
+// printf " assume " ; (VarsAreDifferent aVars0 aVars1) ; printfn ";"
+// printfn " assume %s;" (PrintExpr 0 inv0)
+// printfn " assume %s;" (PrintExpr 0 inv1)
+// printfn " assert false;" // {:msg "Two abstract states map to the same concrete state"}
+// printfn " }"
+// // generate code
+// members |> List.iter (function
+// | Constructor(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv false)
+// | Method(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv true)
+// | _ -> ())
+// // the end of the class
+// printfn "}"
// | _ -> assert false // unexpected case
\ No newline at end of file diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs index 5c42dbec..7af1b6f6 100644 --- a/Jennisys/Jennisys/Ast.fs +++ b/Jennisys/Jennisys/Ast.fs @@ -1,7 +1,9 @@ -/// The AST of a Jennisy program
+// ####################################################################
+/// The AST of a Jennisy program
///
-/// author: Rustan Leino (leino@microsoft.com)
-/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+/// author: Rustan Leino (leino@microsoft.com)
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+// ####################################################################
namespace Ast
@@ -19,17 +21,25 @@ type Type = type VarDecl =
| Var of string * Type option
+(*
+ the difference between IdLiteral and VarLiteral is that the VarLiteral is more specific,
+ it always referes to a local variable (either method parameter or quantification variable)
+ *)
type Expr =
| IntLiteral of int
- | IdLiteral of string
+ | BoolLiteral of bool
+ | VarLiteral of string
+ | IdLiteral of string
| Star
| Dot of Expr * string
| UnaryExpr of string * Expr
| BinaryExpr of int * string * Expr * Expr
+ | IteExpr of (* cond *) Expr * (* thenExpr *) Expr * (* elseExpr *) Expr
| SelectExpr of Expr * Expr
| UpdateExpr of Expr * Expr * Expr
| SequenceExpr of Expr list
| SeqLength of Expr
+ | SetExpr of Expr list //TODO: maybe this should really be a set instead of a list
| ForallExpr of VarDecl list * Expr
type Stmt =
@@ -68,5 +78,4 @@ type Const = | ThisConst of (* loc id *) string * Type option
| NewObj of (* loc id *) string * Type option
| ExprConst of Expr
- | VarConst of (* varName *) string
| Unresolved of (* loc id *) string
\ No newline at end of file diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs index af80fb65..72bd189e 100644 --- a/Jennisys/Jennisys/AstUtils.fs +++ b/Jennisys/Jennisys/AstUtils.fs @@ -1,6 +1,8 @@ -/// Utility functions for manipulating AST elements
+// ####################################################################
+/// Utility functions for manipulating AST elements
///
-/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+// ####################################################################
module AstUtils
@@ -12,208 +14,226 @@ open Utils let rec VisitExpr visitorFunc expr acc =
match expr with
| IntLiteral(_)
- | IdLiteral(_)
- | Star -> acc |> visitorFunc expr
- | Dot(e, _) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
- | SelectExpr(e1, e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
- | UpdateExpr(e1, e2, e3) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3
- | SequenceExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)
- | SeqLength(e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
- | ForallExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
- | UnaryExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
- | BinaryExpr(_,_,e1,e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
+ | BoolLiteral(_)
+ | VarLiteral(_)
+ | IdLiteral(_)
+ | Star -> acc |> visitorFunc expr
+ | Dot(e, _)
+ | ForallExpr(_,e)
+ | UnaryExpr(_,e)
+ | SeqLength(e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+ | SelectExpr(e1, e2)
+ | BinaryExpr(_,_,e1,e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
+ | IteExpr(e1,e2,e3)
+ | UpdateExpr(e1,e2,e3) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3
+ | SequenceExpr(exs) | SetExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)
+
// ------------------------------- End Visitor Stuff -------------------------------------------
exception EvalFailed
-let rec EvalSym expr =
- match expr with
- | IntLiteral(n) -> IntConst(n)
- | IdLiteral(id) -> VarConst(id)
- | Dot(e, str) ->
- match EvalSym e with
- | VarConst(lhsName) -> VarConst(lhsName + "." + str)
- | _ -> ExprConst(expr)
- | SeqLength(e) ->
- match EvalSym e with
- | SeqConst(clist) -> IntConst(List.length clist)
- | _ -> ExprConst(expr)
- | SequenceExpr(elist) ->
- let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev
- SeqConst(clist)
- | SelectExpr(lst, idx) ->
- match EvalSym lst, EvalSym idx with
- | SeqConst(clist), IntConst(n) -> clist.[n]
- | _ -> ExprConst(expr)
- | UpdateExpr(lst,idx,v) ->
- match EvalSym lst, EvalSym idx, EvalSym v with
- | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist)
- | _ -> ExprConst(expr)
- | BinaryExpr(_,op,e1,e2) ->
- match op with
- | Exact "=" _ ->
- match EvalSym e1, EvalSym e2 with
- | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2)
- | VarConst(v1), VarConst(v2) -> BoolConst(v1 = v2)
- | _ -> ExprConst(expr)
- | Exact "!=" _ ->
- match EvalSym e1, EvalSym e2 with
- | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2))
- | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2))
- | VarConst(v1), VarConst(v2) -> BoolConst(not (v1 = v2))
- | _ -> ExprConst(expr)
- | Exact "<" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2)
- | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2))
- | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2))
- | _ -> ExprConst(expr)
- | Exact "<=" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2)
- | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2))
- | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2))
- | _ -> ExprConst(expr)
- | Exact ">" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2)
- | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2))
- | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2))
- | _ -> ExprConst(expr)
- | Exact ">=" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2)
- | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2))
- | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2))
- | _ -> ExprConst(expr)
- | Exact "in" _ ->
- match EvalSym e1, EvalSym e2 with
- | _ as c, SetConst(s) -> BoolConst(Set.contains c s)
- | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains c s)
- | _ -> ExprConst(expr)
- | Exact "!in" _ ->
- match EvalSym e1, EvalSym e2 with
- | _ as c, SetConst(s) -> BoolConst(not (Set.contains c s))
- | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains c s))
- | _ -> ExprConst(expr)
- | Exact "+" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
- | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)
- | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)
- | _ -> ExprConst(expr)
- | Exact "-" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
- | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2)
- | _ -> ExprConst(expr)
- | Exact "*" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2)
- | _ -> ExprConst(expr)
- | Exact "div" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2)
- | _ -> ExprConst(expr)
- | Exact "mod" _ ->
- match EvalSym e1, EvalSym e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2)
- | _ -> ExprConst(expr)
- | _ -> ExprConst(expr)
- | UnaryExpr(op, e) ->
- match op with
- | Exact "!" _ ->
- match EvalSym e with
- | BoolConst(b) -> BoolConst(not b)
- | _ -> ExprConst(expr)
- | Exact "-" _ ->
- match EvalSym e with
- | IntConst(n) -> IntConst(-n)
- | _ -> ExprConst(expr)
- | _ -> ExprConst(expr)
- | _ -> ExprConst(expr)
-
-//TODO: stuff might be missing
-let rec EvalToConst expr =
- match expr with
- | IntLiteral(n) -> IntConst(n)
- | IdLiteral(id) -> raise EvalFailed //VarConst(id)
- | Dot(e, str) -> raise EvalFailed
- | SeqLength(e) ->
- match EvalToConst e with
- | SeqConst(clist) -> IntConst(List.length clist)
- | _ -> raise EvalFailed
- | SequenceExpr(elist) ->
- let clist = elist |> List.fold (fun acc e -> EvalToConst e :: acc) [] |> List.rev
- SeqConst(clist)
- | SelectExpr(lst, idx) ->
- match EvalToConst lst, EvalToConst idx with
- | SeqConst(clist), IntConst(n) -> clist.[n]
- | _ -> raise EvalFailed
- | UpdateExpr(lst,idx,v) ->
- match EvalToConst lst, EvalToConst idx, EvalToConst v with
- | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n c clist)
- | _ -> raise EvalFailed
- | BinaryExpr(_,op,e1,e2) ->
- match op with
- | Exact "=" _ ->
- try
- BoolConst(EvalToBool(e1) = EvalToBool(e2))
- with
- | EvalFailed -> BoolConst(EvalToInt(e1) = EvalToInt(e2))
- | Exact "!=" _ ->
- try
- BoolConst(not(EvalToBool(e1) = EvalToBool(e2)))
- with
- | EvalFailed -> BoolConst(not(EvalToInt e1 = EvalToInt e2))
- | Exact "<" _ -> BoolConst(EvalToInt e1 < EvalToInt e2) //TODO sets, seqs
- | Exact "<=" _ -> BoolConst(EvalToInt e1 <= EvalToInt e2) //TODO sets, seqs
- | Exact ">" _ -> BoolConst(EvalToInt e1 > EvalToInt e2) //TODO sets, seqs
- | Exact ">=" _ -> BoolConst(EvalToInt e1 >= EvalToInt e2) //TODO sets, seqs
- | Exact "in" _ -> raise EvalFailed //TODO
- | Exact "!in" _ -> raise EvalFailed //TODO
- | Exact "+" _ ->
- match EvalToConst e1, EvalToConst e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
- | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)
- | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)
- | _ -> raise EvalFailed
- | Exact "-" _ -> IntConst(EvalToInt e1 - EvalToInt e2)
- | Exact "*" _ -> IntConst(EvalToInt e1 * EvalToInt e2)
- | Exact "div" _ -> IntConst(EvalToInt e1 / EvalToInt e2)
- | Exact "mod" _ -> IntConst(EvalToInt e1 % EvalToInt e2)
- | _ -> raise EvalFailed
- | UnaryExpr(op, e) ->
- match op with
- | Exact "!" _ -> BoolConst(not (EvalToBool e))
- | Exact "-" _ -> IntConst(-(EvalToInt e))
- | _ -> raise EvalFailed
- | _ -> raise EvalFailed
-and EvalToBool e =
- let c = EvalToConst e
- match c with
- | BoolConst(b) -> b
- | _ -> raise EvalFailed
-and EvalToInt e =
- let c = EvalToConst e
- match c with
- | IntConst(n) -> n
- | _ -> raise EvalFailed
-
+let DefaultResolver e = e
+
+let DefaultFallbackResolver resolverFunc e =
+ match resolverFunc e with
+ | Some(e') -> e'
+ | None -> e
+
+let EvalSym resolverFunc expr =
+ let rec __EvalSym ctx expr =
+ match expr with
+ | IntLiteral(_) -> expr
+ | BoolLiteral(_) -> expr
+ | Star -> expr //TODO: can we do better?
+ | VarLiteral(_) -> resolverFunc expr
+ | IdLiteral(_) -> resolverFunc expr
+ | Dot(_) -> resolverFunc expr
+ | SeqLength(e) ->
+ let e' = __EvalSym ctx e
+ match e' with
+ | SequenceExpr(elist) -> IntLiteral(List.length elist)
+ | _ -> SeqLength(e')
+ | SequenceExpr(elist) ->
+ let elist' = elist |> List.fold (fun acc e -> __EvalSym ctx e :: acc) [] |> List.rev
+ SequenceExpr(elist')
+ | SetExpr(elist) ->
+ let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym ctx e) acc) Set.empty
+ SetExpr(Set.toList eset')
+ | SelectExpr(lst, idx) ->
+ let lst', idx' = __EvalSym ctx lst, __EvalSym ctx idx
+ match lst', idx' with
+ | SequenceExpr(elist), IntLiteral(n) -> elist.[n]
+ | _ -> SelectExpr(lst', idx')
+ | UpdateExpr(lst,idx,v) ->
+ let lst', idx', v' = __EvalSym ctx lst, __EvalSym ctx idx, __EvalSym ctx v
+ match lst', idx', v' with
+ | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist)
+ | _ -> UpdateExpr(lst', idx', v')
+ | IteExpr(c, e1, e2) ->
+ let c', e1', e2' = __EvalSym ctx c, __EvalSym ctx e1, __EvalSym ctx e2
+ match c' with
+ | BoolLiteral(b) -> if b then e1' else e2'
+ | _ -> IteExpr(c', e1', e2')
+ | BinaryExpr(p,op,e1,e2) ->
+ let e1' = __EvalSym ctx e1
+ let e2' = __EvalSym ctx e2
+ let recomposed = BinaryExpr(p,op,e1',e2')
+ match op with
+ | "=" ->
+ match e1', e2' with
+ | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)
+ | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 = n2)
+ | _ when e1' = e2' -> BoolLiteral(true)
+ | _ -> recomposed
+ | "!=" ->
+ match e1', e2' with
+ | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(not (b1 = b2))
+ | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(not (n1 = n2))
+ | _ when e1' = e2' -> BoolLiteral(false)
+ | _ -> resolverFunc expr
+ | "<" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 < n2)
+ | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2))
+ | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2))
+ | _ -> recomposed
+ | "<=" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 <= n2)
+ | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))
+ | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))
+ | _ -> recomposed
+ | ">" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 > n2)
+ | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2))
+ | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2))
+ | _ -> recomposed
+ | ">=" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 >= n2)
+ | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))
+ | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))
+ | _ -> recomposed
+ | "in" ->
+ match e1', e2' with
+ | _, SetExpr(s)
+ | _, SequenceExpr(s) -> BoolLiteral(Utils.ListContains e1' s)
+ | _ -> recomposed
+ | "!in" ->
+ match e1', e2' with
+ | _, SetExpr(s)
+ | _, SequenceExpr(s) -> BoolLiteral(not (Utils.ListContains e1' s))
+ | _ -> recomposed
+ | "+" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2)
+ | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2)
+ | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList)
+ | _ -> recomposed
+ | "-" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2)
+ | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList)
+ | _ -> recomposed
+ | "*" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2)
+ | _ -> recomposed
+ | "div" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2)
+ | _ -> recomposed
+ | "mod" ->
+ match e1', e2' with
+ | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2)
+ | _ -> recomposed
+ | "&&" ->
+ match e1', e2' with
+ | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2)
+ | _ -> recomposed
+ | "||" ->
+ match e1', e2' with
+ | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2)
+ | _ -> recomposed
+ | "==>" ->
+ match e1', e2' with
+ | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral((not b1) || b2)
+ | _ -> recomposed
+ | "<==>" ->
+ match e1', e2' with
+ | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)
+ | _ -> recomposed
+ | _ -> recomposed
+ | UnaryExpr(op, e) ->
+ let e' = __EvalSym ctx e
+ let recomposed = UnaryExpr(op, e')
+ match op with
+ | "!" ->
+ match e' with
+ | BoolLiteral(b) -> BoolLiteral(not b)
+ | _ -> recomposed
+ | "-" ->
+ match e' with
+ | IntLiteral(n) -> IntLiteral(-n)
+ | _ -> recomposed
+ | _ -> recomposed
+ | ForallExpr(vars, e) ->
+ let rec PrintSep sep f list =
+ match list with
+ | [] -> ""
+ | [a] -> f a
+ | a :: more -> (f a) + sep + (PrintSep sep f more)
+ let rec PrintType ty =
+ match ty with
+ | IntType -> "int"
+ | BoolType -> "bool"
+ | NamedType(id, args) -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args)
+ | SeqType(t) -> sprintf "seq[%s]" (PrintType t)
+ | SetType(t) -> sprintf "set[%s]" (PrintType t)
+ | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args)
+ let PrintVarDecl vd =
+ match vd with
+ | Var(id,None) -> id
+ | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)
+ vars |> List.iter (fun v -> printfn "%s" (PrintVarDecl v))
+ resolverFunc expr //TODO
+ __EvalSym [] expr
+
+// =======================================
+/// Converts a given constant to expression
+// =======================================
let rec Const2Expr c =
match c with
| IntConst(n) -> IntLiteral(n)
- | BoolConst(b) -> if b then IntLiteral(1) else IntLiteral(0) //?? BoolLiteral(b)
+ | BoolConst(b) -> BoolLiteral(b)
| SeqConst(clist) ->
let expList = clist |> List.fold (fun acc c -> Const2Expr c :: acc) [] |> List.rev
SequenceExpr(expList)
| ThisConst(_) -> IdLiteral("this")
- | VarConst(v) -> IdLiteral(v)
+ | Unresolved(name) -> IdLiteral(name)
| NullConst -> IdLiteral("null")
| ExprConst(e) -> e
- | _ -> failwith "not implemented or not supported"
+ | _ -> failwithf "not implemented or not supported: %O" c
+
+let rec Expr2Const e =
+ match e with
+ | IntLiteral(n) -> IntConst(n)
+ | BoolLiteral(b) -> BoolConst(b)
+ | IdLiteral("this") -> ThisConst("this",None)
+ | IdLiteral("null") -> NullConst
+ | IdLiteral(id) -> Unresolved(id)
+ | VarLiteral(id) -> Unresolved(id)
+ | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const)
+ | SetExpr(elist) -> SetConst(elist |> List.map Expr2Const |> Set.ofList)
+ | _ -> failwithf "Not a constant: %O" e
+
+let TryExpr2Const e =
+ try
+ Some(Expr2Const e)
+ with
+ | ex -> None
// =======================================================================
/// Returns a binary AND of the two given expressions with short-circuiting
@@ -242,16 +262,18 @@ let BinaryOr (lhs: Expr) (rhs: Expr) = // ===================================================================================
let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)
-// =================================================
-/// Returns a binary NEQ of the two given expressions
-// =================================================
+// =======================================================
+/// Constructors for binary EQ/NEQ of two given expressions
+// =======================================================
let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)
-
-// =================================================
-/// Returns a binary EQ of the two given expressions
-// =================================================
let BinaryEq lhs rhs = BinaryExpr(40, "=", lhs, rhs)
+// =======================================================
+/// Constructors for binary IN/!IN of two given expressions
+// =======================================================
+let BinaryIn lhs rhs = BinaryExpr(40, "in", lhs, rhs)
+let BinaryNotIn lhs rhs = BinaryExpr(40, "!in", lhs, rhs)
+
// =====================
/// Returns TRUE literal
// =====================
@@ -368,6 +390,10 @@ let GetMethodPrePost mthd = // =========================================================
/// Returns all arguments of a method (both input and output)
// =========================================================
+let GetSigVars sign =
+ match sign with
+ | Sig(ins, outs) -> List.concat [ins; outs]
+
let GetMethodArgs mthd =
match mthd with
| Method(_,Sig(ins, outs),_,_,_) -> List.concat [ins; outs]
@@ -379,8 +405,7 @@ let rec GetTypeShortName ty = | BoolType -> "bool"
| SetType(_) -> "set"
| SeqType(_) -> "seq"
- | NamedType(n,_) -> n
- | InstantiatedType(n,_) -> n
+ | NamedType(n,_) | InstantiatedType(n,_) -> n
// ==============================================================
/// Returns all invariants of a component as a list of expressions
@@ -390,7 +415,14 @@ let GetInvariantsAsList comp = | Component(Class(_,_,members), Model(_,_,_,_,inv), _) ->
let clsInvs = members |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat
List.append (SplitIntoConjunts inv) clsInvs
- | _ -> failwith ("unexpected kinf of component: %s" + comp.ToString())
+ | _ -> failwithf "unexpected kind of component: %O" comp
+
+// ==================================
+/// Returns variable name
+// ==================================
+let GetVarName var =
+ match var with
+ | Var(name,_) -> name
// ==================================
/// Returns all members of a component
@@ -436,43 +468,101 @@ let FindVar (prog: Program) clsName fldName = let rec Desugar expr =
match expr with
| IntLiteral(_)
- | IdLiteral(_)
+ | BoolLiteral(_)
+ | IdLiteral(_)
+ | VarLiteral(_)
| Star
| Dot(_)
| SelectExpr(_)
- | SeqLength(_) -> expr
- | UpdateExpr(_) -> expr //TODO
- | SequenceExpr(exs) -> expr //TODO
+ | SeqLength(_)
+ | UpdateExpr(_)
+ | SetExpr(_)
+ | SequenceExpr(_) -> expr
| ForallExpr(v,e) -> ForallExpr(v, Desugar e)
| UnaryExpr(op,e) -> UnaryExpr(op, Desugar e)
+ | IteExpr(c,e1,e2) -> IteExpr(c, Desugar e1, Desugar e2)
| BinaryExpr(p,op,e1,e2) ->
let be = BinaryExpr(p, op, Desugar e1, Desugar e2)
try
match op with
- | Exact "=" _ ->
- match EvalSym e1, EvalSym e2 with
- | VarConst(v), SeqConst(clist)
- | SeqConst(clist), VarConst(v) ->
- let rec __fff lst cnt =
- match lst with
- | fs :: rest -> BinaryEq (SelectExpr(IdLiteral(v), IntLiteral(cnt))) (Const2Expr clist.[cnt]) :: __fff rest (cnt+1)
- | [] -> []
- __fff clist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
- | SeqConst(cl1), SeqConst(cl2) ->
+ | "=" ->
+ match EvalSym DefaultResolver e1, EvalSym DefaultResolver e2 with
+ | SequenceExpr(l1), SequenceExpr(l2) ->
let rec __fff lst1 lst2 cnt =
match lst1, lst2 with
- | fs1 :: rest1, fs2 :: rest2 -> BinaryEq (Const2Expr cl1.[cnt]) (Const2Expr cl2.[cnt]) :: __fff rest1 rest2 (cnt+1)
+ | fs1 :: rest1, fs2 :: rest2 -> BinaryEq l1.[cnt] l2.[cnt] :: __fff rest1 rest2 (cnt+1)
| [], [] -> []
| _ -> failwith "Lists are of different sizes"
- __fff cl1 cl2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
+ __fff l1 l2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
+ | e, SequenceExpr(elist)
+ | SequenceExpr(elist), e ->
+ let rec __fff lst cnt =
+ match lst with
+ | fs :: rest -> BinaryEq (SelectExpr(e, IntLiteral(cnt))) elist.[cnt] :: __fff rest (cnt+1)
+ | [] -> []
+ __fff elist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
| _ -> be
| _ -> be
with
- | EvalFailed as ex -> (* printfn "%s" (ex.StackTrace.ToString()); *) be
-
+ | EvalFailed as ex -> (* printfn "%O" (ex.StackTrace); *) be
let rec DesugarLst exprLst =
match exprLst with
| expr :: rest -> Desugar expr :: DesugarLst rest
| [] -> []
+let ChangeThisReceiver receiver expr =
+ let rec __ChangeThis locals expr =
+ match expr with
+ | IntLiteral(_)
+ | BoolLiteral(_)
+ | Star
+ | VarLiteral(_)
+ | IdLiteral("null") -> expr
+ | IdLiteral("this") -> receiver
+ | IdLiteral(id) -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(IdLiteral("this"), id))
+ | Dot(e, id) -> Dot(__ChangeThis locals e, id)
+ | ForallExpr(vars,e) -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals
+ ForallExpr(vars, __ChangeThis newLocals e)
+ | UnaryExpr(op,e) -> UnaryExpr(op, __ChangeThis locals e)
+ | SeqLength(e) -> SeqLength(__ChangeThis locals e)
+ | SelectExpr(e1, e2) -> SelectExpr(__ChangeThis locals e1, __ChangeThis locals e2)
+ | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, __ChangeThis locals e1, __ChangeThis locals e2)
+ | IteExpr(e1,e2,e3) -> IteExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3)
+ | UpdateExpr(e1,e2,e3) -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3)
+ | SequenceExpr(exs) -> SequenceExpr(exs |> List.map (__ChangeThis locals))
+ | SetExpr(exs) -> SetExpr(exs |> List.map (__ChangeThis locals))
+ (* function body starts here *)
+ __ChangeThis Set.empty expr
+
+let rec Rewrite rewriterFunc expr =
+ let __RewriteOrRecurse e =
+ match rewriterFunc e with
+ | Some(ee) -> ee
+ | None -> Rewrite rewriterFunc e
+ match expr with
+ | IntLiteral(_)
+ | BoolLiteral(_)
+ | Star
+ | VarLiteral(_)
+ | IdLiteral(_) -> match rewriterFunc expr with
+ | Some(e) -> e
+ | None -> expr
+ | Dot(e, id) -> Dot(__RewriteOrRecurse e, id)
+ | ForallExpr(vars,e) -> ForallExpr(vars, __RewriteOrRecurse e)
+ | UnaryExpr(op,e) -> UnaryExpr(op, __RewriteOrRecurse e)
+ | SeqLength(e) -> SeqLength(__RewriteOrRecurse e)
+ | SelectExpr(e1, e2) -> SelectExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2)
+ | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, __RewriteOrRecurse e1, __RewriteOrRecurse e2)
+ | IteExpr(e1,e2,e3) -> IteExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3)
+ | UpdateExpr(e1,e2,e3) -> UpdateExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3)
+ | SequenceExpr(exs) -> SequenceExpr(exs |> List.map __RewriteOrRecurse)
+ | SetExpr(exs) -> SetExpr(exs |> List.map __RewriteOrRecurse)
+
+let RewriteVars vars expr =
+ let __IdIsArg id = vars |> List.exists (function Var(name,_) -> name = id)
+ Rewrite (fun e ->
+ match e with
+ | IdLiteral(id) when __IdIsArg id -> Some(VarLiteral(id))
+ | _ -> None) expr
+
\ No newline at end of file diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs index 3c97b94f..f0e59d3b 100644 --- a/Jennisys/Jennisys/CodeGen.fs +++ b/Jennisys/Jennisys/CodeGen.fs @@ -97,21 +97,26 @@ let PrintAllocNewObjects (heap,env,ctx) indent = |> Set.fold (fun acc newObjConst ->
match newObjConst with
| NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline)
- | _ -> failwith ("NewObj doesn't have a type: " + newObjConst.ToString())
+ | _ -> failwithf "NewObj doesn't have a type: %O" newObjConst
) ""
let PrintObjRefName o (env,ctx) =
- match Resolve o (env,ctx) with
+ match Resolve (env,ctx) o with
| ThisConst(_,_) -> "this";
| NewObj(name, _) -> PrintGenSym name
| _ -> failwith ("unresolved object ref: " + o.ToString())
+let CheckUnresolved c =
+ match c with
+ | Unresolved(_) -> Logger.WarnLine "!!! There are some unresolved constants in the output file !!!"; c
+ | _ -> c
+
let PrintVarAssignments (heap,env,ctx) indent =
let idt = Indent indent
heap |> Map.fold (fun acc (o,f) l ->
let objRef = PrintObjRefName o (env,ctx)
let fldName = PrintVarName f
- let value = Resolve l (env,ctx) |> PrintConst
+ let value = TryResolve (env,ctx) l |> CheckUnresolved |> PrintConst
acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline
) ""
@@ -135,17 +140,6 @@ let GenConstructorCode mthd body = " }" + newline
| _ -> ""
-// NOTE: insert here coto to say which methods to analyze
-let GetMethodsToAnalyze prog =
- (* exactly one *)
-// let c = FindComponent prog "List" |> Utils.ExtractOption
-// let m = FindMethod c "Double" |> Utils.ExtractOption
-// [c, m]
- (* all *)
- FilterMembers prog FilterConstructorMembers
- (* only with parameters *)
-// FilterMembers prog FilterConstructorMembersWithParams
-
// solutions: (comp, constructor) |--> (heap, env, ctx)
let PrintImplCode prog solutions methodsToPrintFunc =
let methods = methodsToPrintFunc prog
@@ -156,5 +150,4 @@ let PrintImplCode prog solutions methodsToPrintFunc = | _ -> " //unable to synthesize" + newline
(GenConstructorCode mthd mthdBody) + newline
else
- ""
- )
\ No newline at end of file + "")
\ No newline at end of file diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs index 597ac7c9..4b9b0c60 100644 --- a/Jennisys/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/Jennisys/DafnyModelUtils.fs @@ -1,4 +1,10 @@ -module DafnyModelUtils
+// #########################################################################
+/// Utilities for reading/building models from Boogie Visual Debugger files
+///
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+// #########################################################################
+
+module DafnyModelUtils
(*
The heap maps objects and fields to locations.
@@ -18,10 +24,7 @@ open AstUtils open Utils
open Microsoft.Boogie
-
-/// special object ref constant that will hold method argument values
-let argsObjRefConst = Unresolved("*0")
-
+
let GetElemFullName (elem: Model.Element) =
elem.Names |> Seq.filter (fun ft -> ft.Func.Arity = 0)
|> Seq.choose (fun ft -> Some(ft.Func.Name))
@@ -64,7 +67,7 @@ let GetType (e: Model.Element) prog = let fNameOpt = GetElemFullName e
match fNameOpt with
| Some(fname) -> match fname with
- | Exact "intType" _ -> Some(IntType)
+ | "intType" -> Some(IntType)
| Prefix "class." clsName ->
match FindComponent prog clsName with
| Some(comp) -> Some(GetClassType comp)
@@ -75,10 +78,16 @@ let GetType (e: Model.Element) prog = let GetLoc (e: Model.Element) =
Unresolved(GetRefName e)
-let GetSeqFromEnv env key =
+let FindSeqInEnv env key =
match Map.find key env with
| SeqConst(lst) -> lst
| _ as x-> failwith ("not a SeqConst but: " + x.ToString())
+
+let TryFindSetInEnv env key =
+ match Map.tryFind key env with
+ | Some(SetConst(s)) -> Some(s)
+ | Some(x) -> failwith ("not a SetConst but: " + x.ToString())
+ | None -> None
let AddConstr c1 c2 ctx =
if c1 = c2 then
@@ -141,87 +150,204 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog = | None -> acc
) Map.empty
+// ====================================================================
+/// Reads values that were assigned to given arguments. Those values
+/// can be in functions with the same name as the argument name appended
+/// with an "#" and some number after it.
+// ====================================================================
let rec ReadArgValues (model: Microsoft.Boogie.Model) args =
match args with
| Var(name,_) as v :: rest ->
let farg = model.Functions |> Seq.filter (fun f -> f.Arity = 0 && f.Name.StartsWith(name + "#")) |> Utils.SeqToOption
match farg with
| Some(func) ->
- let refObj = argsObjRefConst
let fldVar = v
assert (Seq.length func.Apps = 1)
let ft = Seq.head func.Apps
let fldVal = ConvertValue model (ft.Result)
- ReadArgValues model rest |> Map.add (VarConst(name)) fldVal
+ ReadArgValues model rest |> Map.add (Unresolved(name)) fldVal
| None -> failwith ("cannot find corresponding function for parameter " + name)
| [] -> Map.empty
-let rec ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple list) (envMap,ctx) =
- match len_tuples with
- | ft :: rest ->
- let len = GetInt ft.Result
- let emptyList = Utils.GenList len NoneConst
- let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList))
- ReadSeqLen model rest (newMap,ctx)
- | _ -> (envMap,ctx)
-
-let rec ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTuple list) (envMap,ctx) =
- match idx_tuples with
- | ft :: rest ->
- let srcLstKey = GetLoc ft.Args.[0]
- let oldLst = GetSeqFromEnv envMap srcLstKey
- let idx = GetInt ft.Args.[1]
- let lstElem = UnboxIfNeeded model ft.Result
- let newLst = Utils.ListSet idx lstElem oldLst
- let newCtx = UpdateContext oldLst newLst ctx
- let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst))
- ReadSeqIndex model rest (newEnv,newCtx)
- | _ -> (envMap,ctx)
-
-let rec ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) =
- match bld_tuples with
- | ft :: rest ->
- let srcLstLoc = GetLoc ft.Args.[0]
- let dstLstLoc = GetLoc ft.Result
- let oldLst = GetSeqFromEnv envMap srcLstLoc
- let idx = GetInt ft.Args.[1]
- let lstElemVal = UnboxIfNeeded model ft.Args.[2]
- let dstLst = GetSeqFromEnv envMap dstLstLoc
- let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst
- let newCtx = UpdateContext dstLst newLst ctx
- let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))
- ReadSeqBuild model rest (newEnv,newCtx)
- | _ -> (envMap,ctx)
-
-let rec ReadSeqAppend (model: Microsoft.Boogie.Model) (app_tuples: Model.FuncTuple list) (envMap,ctx) =
- match app_tuples with
- | ft :: rest ->
- let srcLst1Loc = GetLoc ft.Args.[0]
- let srcLst2Loc = GetLoc ft.Args.[1]
- let dstLstLoc = GetLoc ft.Result
- let oldLst1 = GetSeqFromEnv envMap srcLst1Loc
- let oldLst2 = GetSeqFromEnv envMap srcLst2Loc
- let dstLst = GetSeqFromEnv envMap dstLstLoc
- let newLst = List.append oldLst1 oldLst2
- let newCtx = UpdateContext dstLst newLst ctx
- let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))
- ReadSeqAppend model rest (newEnv,newCtx)
- | _ -> (envMap,ctx)
-
+// ==============================================================
+/// Reads stuff about sequences from a given model and ads it to
+/// the given "envMap" map and a "ctx" set. The relevant stuff is
+/// fetched from the following functions:
+/// Seq#Length, Seq#Index, Seq#Build, Seq#Append
+// ==============================================================
let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
+ // reads stuff from Seq#Length
+ let rec __ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match len_tuples with
+ | ft :: rest ->
+ let len = GetInt ft.Result
+ let emptyList = Utils.GenList len NoneConst
+ let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList))
+ __ReadSeqLen model rest (newMap,ctx)
+ | _ -> (envMap,ctx)
+
+ // reads stuff from Seq#Index
+ let rec __ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match idx_tuples with
+ | ft :: rest ->
+ let srcLstKey = GetLoc ft.Args.[0]
+ let oldLst = FindSeqInEnv envMap srcLstKey
+ let idx = GetInt ft.Args.[1]
+ let lstElem = UnboxIfNeeded model ft.Result
+ let newLst = Utils.ListSet idx lstElem oldLst
+ let newCtx = UpdateContext oldLst newLst ctx
+ let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst))
+ __ReadSeqIndex model rest (newEnv,newCtx)
+ | _ -> (envMap,ctx)
+
+ // reads stuff from Seq#Build
+ let rec __ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match bld_tuples with
+ | ft :: rest ->
+ let srcLstLoc = GetLoc ft.Args.[0]
+ let dstLstLoc = GetLoc ft.Result
+ let oldLst = FindSeqInEnv envMap srcLstLoc
+ let idx = GetInt ft.Args.[1]
+ let lstElemVal = UnboxIfNeeded model ft.Args.[2]
+ let dstLst = FindSeqInEnv envMap dstLstLoc
+ let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst
+ let newCtx = UpdateContext dstLst newLst ctx
+ let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))
+ __ReadSeqBuild model rest (newEnv,newCtx)
+ | _ -> (envMap,ctx)
+
+ // reads stuff from Seq#Append
+ let rec __ReadSeqAppend (model: Microsoft.Boogie.Model) (app_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match app_tuples with
+ | ft :: rest ->
+ let srcLst1Loc = GetLoc ft.Args.[0]
+ let srcLst2Loc = GetLoc ft.Args.[1]
+ let dstLstLoc = GetLoc ft.Result
+ let oldLst1 = FindSeqInEnv envMap srcLst1Loc
+ let oldLst2 = FindSeqInEnv envMap srcLst2Loc
+ let dstLst = FindSeqInEnv envMap dstLstLoc
+ let newLst = List.append oldLst1 oldLst2
+ let newCtx = UpdateContext dstLst newLst ctx
+ let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))
+ __ReadSeqAppend model rest (newEnv,newCtx)
+ | _ -> (envMap,ctx)
+
let f_seq_len = model.MkFunc("Seq#Length", 1)
let f_seq_idx = model.MkFunc("Seq#Index", 2)
let f_seq_bld = model.MkFunc("Seq#Build", 4)
let f_seq_app = model.MkFunc("Seq#Append", 2)
- (envMap,ctx) |> ReadSeqLen model (List.ofSeq f_seq_len.Apps)
- |> ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)
- |> ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)
- |> ReadSeqAppend model (List.ofSeq f_seq_app.Apps)
+ (envMap,ctx) |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps)
+ |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)
+ |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)
+ |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)
+// =====================================================
+/// Reads stuff about sets from a given model and adds it
+/// to the given "envMap" map and "ctx" set.
+// =====================================================
let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =
- (envMap,ctx)
+ // reads stuff from Set#Empty
+ let rec __ReadSetEmpty (empty_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match empty_tuples with
+ | ft :: rest ->
+ let newMap = envMap |> Map.add (GetLoc ft.Result) (SetConst(Set.empty))
+ __ReadSetEmpty rest (newMap,ctx)
+ | [] -> (envMap,ctx)
+
+ // reads stuff from [2]
+ let rec __ReadSetMembership (set_tuples: Model.FuncTuple list) (env,ctx) =
+ match set_tuples with
+ | ft :: rest ->
+ if GetBool ft.Result then
+ let srcSetKey = GetLoc ft.Args.[0]
+ let srcSet = match TryFindSetInEnv env srcSetKey with
+ | Some(s) -> s
+ | None -> Set.empty
+ let elem = UnboxIfNeeded model ft.Args.[1]
+ let newEnv = env |> Map.add srcSetKey (SetConst(Set.add elem srcSet))
+ __ReadSetMembership rest (newEnv,ctx)
+ else
+ __ReadSetMembership rest (env,ctx)
+ | [] -> (env,ctx)
+
+ let t_set_empty = Seq.toList (model.MkFunc("Set#Empty", 1).Apps)
+ let t_set = Seq.toList (model.MkFunc("[2]", 2).Apps)
+ (envMap,ctx) |> __ReadSetEmpty t_set_empty
+ |> __ReadSetMembership t_set
+
+(* More complicated way which now doesn't seem to be necessary *)
+//let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =
+// // reads stuff from Set#Empty
+// let rec __ReadSetEmpty (empty_tuples: Model.FuncTuple list) (envMap,ctx) =
+// match empty_tuples with
+// | ft :: rest ->
+// let newMap = envMap |> Map.add (GetLoc ft.Result) (SetConst(Set.empty))
+// __ReadSetEmpty rest (newMap,ctx)
+// | [] -> (envMap,ctx)
+//
+// // reads stuff from Set#UnionOne and Set#Union
+// let rec __ReadSetUnions (envMap,ctx) =
+// // this one goes through a given list of "UnionOne" tuples, updates
+// // the env for those set that it was able to resolve, and returns a
+// // list of tuples for which it wasn't able to resolve sets
+// let rec ___RSU1 (tuples: Model.FuncTuple list) env unprocessed =
+// match tuples with
+// | ft :: rest ->
+// let srcSetKey = GetLoc ft.Args.[0]
+// match TryFindSetInEnv env srcSetKey with
+// | Some(oldSet) ->
+// let elem = UnboxIfNeeded model ft.Args.[1]
+// let newSet = Set.add elem oldSet
+// // update contex?
+// let newEnv = env |> Map.add (GetLoc ft.Result) (SetConst(newSet))
+// ___RSU1 rest newEnv unprocessed
+// | None -> ___RSU1 rest env (ft :: unprocessed)
+// | [] -> (env,unprocessed)
+// // this one goes through a given list of "Union" tuples, updates
+// // the env for those set that it was able to resolve, and returns a
+// // list of tuples for which it wasn't able to resolve sets
+// let rec ___RSU (tuples: Model.FuncTuple list) env unprocessed =
+// match tuples with
+// | ft :: rest ->
+// let set1Key = GetLoc ft.Args.[0]
+// let set2Key = GetLoc ft.Args.[1]
+// match TryFindSetInEnv env set1Key, TryFindSetInEnv env set2Key with
+// | Some(oldSet1), Some(oldSet2) ->
+// let newSet = Set.union oldSet1 oldSet2
+// // update contex?
+// let newEnv = env |> Map.add (GetLoc ft.Result) (SetConst(newSet))
+// ___RSU rest newEnv unprocessed
+// | _ -> ___RSU rest env (ft :: unprocessed)
+// | [] -> (env,unprocessed)
+// // this one keeps looping as loong as the list of unprocessed tuples
+// // is decreasing, it ends when if falls down to 0, or fails if
+// // the list stops decreasing
+// let rec ___RSU_until_fixpoint u1tuples utuples env =
+// let newEnv1,unprocessed1 = ___RSU1 u1tuples env []
+// let newEnv2,unprocessed2 = ___RSU utuples newEnv1 []
+// let oldLen = (List.length u1tuples) + (List.length utuples)
+// let totalUnprocLen = (List.length unprocessed1) + (List.length unprocessed2)
+// if totalUnprocLen = 0 then
+// newEnv2
+// elif totalUnprocLen < oldLen then
+// ___RSU_until_fixpoint unprocessed1 unprocessed2 newEnv2
+// else
+// failwith "cannot resolve all sets in Set#UnionOne/Set#Union"
+// // finally, just invoke the fixpoint function for UnionOne and Union tuples
+// let t_union_one = Seq.toList (model.MkFunc("Set#UnionOne", 2).Apps)
+// let t_union = Seq.toList (model.MkFunc("Set#Union", 2).Apps)
+// let newEnv = ___RSU_until_fixpoint t_union_one t_union envMap
+// (newEnv,ctx)
+//
+// let f_set_empty = model.MkFunc("Set#Empty", 1)
+// (envMap,ctx) |> __ReadSetEmpty (List.ofSeq f_set_empty.Apps)
+// |> __ReadSetUnions
+// ======================================================
+/// Reads staff about the null constant from a given model
+/// and adds it to the given "envMap" map and "ctx" set.
+// ======================================================
let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) =
let f_null = model.MkFunc("null", 0)
assert (f_null.AppCount = 1)
@@ -229,6 +355,12 @@ let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) = let newEnv = envMap |> Map.add (GetLoc e) NullConst
(newEnv,ctx)
+// ============================================================================================
+/// Reads the evinronment map and the context set.
+///
+/// It starts by reading the model for the "dtype" function to discover all objects on the heap,
+/// and then proceeds by reading stuff about the null constant, about sequences, and about sets.
+// ============================================================================================
let ReadEnv (model: Microsoft.Boogie.Model) prog =
let f_dtype = model.MkFunc("dtype", 1)
let refs = f_dtype.Apps |> Seq.choose (fun ft -> Some(ft.Args.[0]))
diff --git a/Jennisys/Jennisys/DafnyPrinter.fs b/Jennisys/Jennisys/DafnyPrinter.fs index fb9f3bf7..05f333d1 100644 --- a/Jennisys/Jennisys/DafnyPrinter.fs +++ b/Jennisys/Jennisys/DafnyPrinter.fs @@ -14,7 +14,9 @@ let rec PrintType ty = let rec PrintExpr ctx expr = match expr with - | IntLiteral(n) -> sprintf "%O" n + | IntLiteral(n) -> sprintf "%d" n + | BoolLiteral(b) -> sprintf "%b" b + | VarLiteral(id) | IdLiteral(id) -> id | Star -> assert false; "" // I hope this won't happen | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id @@ -30,10 +32,12 @@ let rec PrintExpr ctx expr = let openParen = if needParens then "(" else "" let closeParen = if needParens then ")" else "" sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen + | IteExpr(c,e1,e2) -> sprintf "(if %s then %s else %s)" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2) | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v) | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0)) | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e) + | SetExpr(ee) -> sprintf "{%s}" (ee |> PrintSep ", " (PrintExpr 0)) | ForallExpr(vv,e) -> let needParens = true let openParen = if needParens then "(" else "" diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs index 32827f39..ca1ab1ad 100644 --- a/Jennisys/Jennisys/Jennisys.fs +++ b/Jennisys/Jennisys/Jennisys.fs @@ -10,60 +10,42 @@ open Microsoft.FSharp.Text.Lexing open Ast open Lexer +open Options open Parser open Printer open TypeChecker open Analyzer -let readAndProcess tracing analyzing (filename: string) = +let readAndProcess (filename: string) = + try + printfn "// Jennisys, Copyright (c) 2011, Microsoft." + // lex + let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader + let lexbuf = LexBuffer<char>.FromTextReader(f) + lexbuf.EndPos <- { pos_bol = 0; + pos_fname=if filename = null then "stdin" else filename; + pos_cnum=0; + pos_lnum=1 } try - printfn "// Jennisys, Copyright (c) 2011, Microsoft." - // lex - let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader - let lexbuf = LexBuffer<char>.FromTextReader(f) - lexbuf.EndPos <- { pos_bol = 0; - pos_fname=if filename = null then "stdin" else filename; - pos_cnum=0; - pos_lnum=1 } - try - // parse - let sprog = Parser.start Lexer.tokenize lexbuf - // print the given Jennisys program - if tracing then - printfn "---------- Given Jennisys program ----------" - printfn "%s" (Print sprog) - else () - match TypeCheck sprog with - | None -> () // errors have already been reported - | Some(prog) -> - if analyzing then - // output a Dafny program with the constraints to be solved - Analyze prog filename - else () - // that's it - if tracing then printfn "----------" else () - with - | ex -> - let pos = lexbuf.EndPos - printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message - printfn "%s" (ex.StackTrace.ToString()) - + // parse + let sprog = Parser.start Lexer.tokenize lexbuf + match TypeCheck sprog with + | None -> () // errors have already been reported + | Some(prog) -> + Analyze prog filename with - | ex -> + | ex -> + let pos = lexbuf.EndPos + printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message + printfn "%s" (ex.StackTrace.ToString()) + with + | ex -> printfn "Unhandled Exception: %s" ex.Message printfn "%s" (ex.StackTrace.ToString()) -let rec start n (args: string []) tracing analyzing filename = - if n < args.Length then - let arg = args.[n] - if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else () - let filename = if arg.StartsWith "/" then filename else arg - start (n+1) args (tracing || arg = "/trace") (analyzing && arg <> "/noAnalysis") filename - else - readAndProcess tracing analyzing filename - -let args = Environment.GetCommandLineArgs() try - start 1 args false true null -with - | Failure(msg) as e -> printfn "WHYYYYYYYYYYYYYYY: %s" msg; printfn "%s" e.StackTrace
\ No newline at end of file + let args = Environment.GetCommandLineArgs() + ParseCmdLineArgs (List.ofArray args) + readAndProcess CONFIG.inputFilename +with + | InvalidCmdLineOption(msg) as ex -> printfn "%s" msg; printfn "%s" ex.StackTrace
\ No newline at end of file diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj index bbb15dc4..832176fd 100644 --- a/Jennisys/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ <WarningLevel>3</WarningLevel>
<PlatformTarget>x86</PlatformTarget>
<DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
- <StartArguments>C:\boogie\Jennisys\Jennisys\examples\List.jen</StartArguments>
+ <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Double /noCheckUnifs</StartArguments>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
<DebugType>pdbonly</DebugType>
@@ -42,8 +42,8 @@ <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>
</PropertyGroup>
<ItemGroup>
- <Compile Include="Options.fs" />
<Compile Include="Utils.fs" />
+ <Compile Include="Options.fs" />
<Compile Include="PipelineUtils.fs" />
<Compile Include="Ast.fs" />
<Compile Include="AstUtils.fs" />
@@ -64,8 +64,8 @@ <OtherFlags>--unicode</OtherFlags>
</FsLex>
<Compile Include="Printer.fs" />
- <Compile Include="Logger.fs" />
<Compile Include="DafnyPrinter.fs" />
+ <Compile Include="Logger.fs" />
<Compile Include="TypeChecker.fs" />
<Compile Include="Resolver.fs" />
<Compile Include="CodeGen.fs" />
diff --git a/Jennisys/Jennisys/Lexer.fsl b/Jennisys/Jennisys/Lexer.fsl index 91c3239c..9eaf7421 100644 --- a/Jennisys/Jennisys/Lexer.fsl +++ b/Jennisys/Jennisys/Lexer.fsl @@ -69,6 +69,7 @@ rule tokenize = parse | ":" { COLON }
| "::" { COLONCOLON }
| "," { COMMA }
+| "?" { QMARK }
// Numberic constants
| digit+ { INTEGER (System.Convert.ToInt32(lexeme lexbuf)) }
// identifiers
diff --git a/Jennisys/Jennisys/Logger.fs b/Jennisys/Jennisys/Logger.fs index bb784ba2..2801354d 100644 --- a/Jennisys/Jennisys/Logger.fs +++ b/Jennisys/Jennisys/Logger.fs @@ -1,6 +1,8 @@ -/// Simple logging facility
+// #######################################################
+/// Simple logging facility
///
-/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+// #######################################################
module Logger
diff --git a/Jennisys/Jennisys/Options.fs b/Jennisys/Jennisys/Options.fs index 34a0422b..4a1487ce 100644 --- a/Jennisys/Jennisys/Options.fs +++ b/Jennisys/Jennisys/Options.fs @@ -1,8 +1,113 @@ -/// This module is intended to store and handle configuration options
+// ####################################################################
+/// This module is intended to store and handle configuration options
///
-/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+// ####################################################################
module Options
-/// attempt to verify synthesized code
-let _opt_verifySolutions = true
\ No newline at end of file +open Utils
+
+type Config = {
+ inputFilename: string;
+ methodToSynth: string;
+ verifySolutions: bool;
+ checkUnifications: bool;
+ timeout: int;
+}
+
+let defaultConfig: Config = {
+ inputFilename = "";
+ methodToSynth = "*";
+ verifySolutions = true;
+ checkUnifications = true;
+ timeout = 0;
+}
+
+let mutable CONFIG = defaultConfig
+
+exception InvalidCmdLineArg of string
+exception InvalidCmdLineOption of string
+
+let ParseCmdLineArgs args =
+ let __StripSwitches str =
+ match str with
+ | Prefix "--" x
+ | Prefix "-" x
+ | Prefix "/" x -> x
+ | _ -> str
+
+ let __Split (str: string) =
+ let stripped = __StripSwitches str
+ if stripped = str then
+ ("",str)
+ else
+ let splits = stripped.Split([| ':' |])
+ if splits.Length > 2 then raise (InvalidCmdLineOption("more than 2 colons in " + str))
+ if splits.Length = 2 then
+ let opt = splits.[0]
+ let value = splits.[1]
+ (opt,value)
+ else
+ let x = __StripSwitches splits.[0]
+ (x, "")
+
+ let __CheckNonEmpty value optName =
+ if value = "" then raise (InvalidCmdLineArg("A value for option " + optName + " must not be empty"))
+
+ let __CheckInt value optName =
+ try
+ System.Int32.Parse value
+ with
+ | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be a boolean"))
+
+ let __CheckBool value optName =
+ if value = "" then
+ true
+ else
+ try
+ System.Boolean.Parse value
+ with
+ | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be an integer"))
+
+ let rec __Parse args cfg =
+ match args with
+ | fs :: rest ->
+ let opt,value = __Split fs
+ match opt with
+ | "method" ->
+ __CheckNonEmpty value opt
+ __Parse rest { cfg with methodToSynth = value }
+ | "verifySol" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with verifySolutions = b }
+ | "noVerifySol" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with verifySolutions = not b }
+ | "checkUnifs" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with checkUnifications = b }
+ | "noCheckUnifs" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with checkUnifications = not b }
+ | "timeout" ->
+ let t = __CheckInt value opt
+ __Parse rest { cfg with timeout = t }
+ | "" ->
+ __Parse rest { cfg with inputFilename = value }
+ | _ ->
+ raise (InvalidCmdLineOption("Unknown option: " + opt))
+ | [] -> cfg
+
+ let __CheckBool value optName =
+ if value = "" then
+ true
+ else
+ try
+ System.Boolean.Parse value
+ with
+ | ex -> raise (InvalidCmdLineArg("Option " + optName " must be boolean"))
+
+ (* --- function body starts here --- *)
+ CONFIG <- __Parse args defaultConfig
+
diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy index 5053bd18..15b27ddb 100644 --- a/Jennisys/Jennisys/Parser.fsy +++ b/Jennisys/Jennisys/Parser.fsy @@ -26,7 +26,7 @@ let rec MyFold ee acc = %token IMPLIES
%token IFF
%token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR
-%token GETS COLON COLONCOLON COMMA
+%token GETS COLON COLONCOLON COMMA QMARK
%token CLASS MODEL CODE
%token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL
%token INTTYPE BOOLTYPE SEQTYPE SETTYPE
@@ -89,7 +89,7 @@ BlockStmt: Member:
| VAR VarDecl { Field($2) }
- | CONSTRUCTOR ID Signature Pre Post { Method($2, $3, $4, $5, true) }
+ | CONSTRUCTOR ID Signature Pre Post { Method($2, $3, RewriteVars (GetSigVars $3) $4, RewriteVars (GetSigVars $3) $5, true) }
| METHOD ID Signature Pre Post { Method($2, $3, $4, $5, false) }
| INVARIANT ExprList { Invariant($2) }
@@ -134,9 +134,12 @@ Expr10: | Expr10 IFF Expr20 { BinaryExpr(10,"<==>",$1,$3) }
Expr20:
- | Expr30 { $1 }
- | Expr30 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) }
+ | Expr25 { $1 }
+ | Expr25 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) }
+Expr25:
+ | Expr30 { $1 }
+ | Expr30 QMARK Expr25 COLON Expr25 { IteExpr($1,$3,$5) }
Expr30:
| Expr40 { $1 }
| Expr40 AND Expr30and { BinaryAnd $1 $3 }
@@ -183,8 +186,9 @@ Expr100: | Expr100 LBRACKET Expr GETS Expr RBRACKET { UpdateExpr($1, $3, $5) }
| LPAREN Expr RPAREN { $2 }
| LBRACKET ExprList RBRACKET { SequenceExpr($2) }
+ | LCURLY ExprList RCURLY { SetExpr($2) }
| VERTBAR Expr VERTBAR { SeqLength($2) }
- | FORALL VarDeclList COLONCOLON Expr { ForallExpr($2, $4) }
+ | FORALL VarDeclList COLONCOLON Expr { ForallExpr($2, RewriteVars $2 $4) }
StarExpr:
| STAR { Star }
diff --git a/Jennisys/Jennisys/PipelineUtils.fs b/Jennisys/Jennisys/PipelineUtils.fs index c17ebfa7..1439018a 100644 --- a/Jennisys/Jennisys/PipelineUtils.fs +++ b/Jennisys/Jennisys/PipelineUtils.fs @@ -1,7 +1,9 @@ -/// Utility functions for executing shell commands and
-/// running Dafny in particular
+// ####################################################################
+/// Utility functions for executing shell commands and
+/// running Dafny in particular
///
-/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+// ####################################################################
module PipelineUtils
@@ -10,6 +12,8 @@ let dafnyVerifySuffix = "verify" let dafnyUnifSuffix = "unif"
let dafnySynthFileNameTemplate = @"c:\tmp\jennisys-synth_###.dfy"
+let mutable lastDafnyExitCode = 0 //TODO: how to avoid this muttable state?
+
let CreateEmptyModelFile modelFile =
use mfile = System.IO.File.CreateText(modelFile)
fprintf mfile ""
@@ -23,10 +27,11 @@ let RunDafny inputFile modelFile = async {
use proc = new System.Diagnostics.Process()
proc.StartInfo.FileName <- @"c:\tmp\StartDafny-jen.bat"
- proc.StartInfo.Arguments <- "/mv:" + modelFile + " " + inputFile
+ proc.StartInfo.Arguments <- (sprintf "/mv:%s /timeLimit:%d %s" modelFile Options.CONFIG.timeout inputFile)
proc.StartInfo.WindowStyle <- System.Diagnostics.ProcessWindowStyle.Hidden
assert proc.Start()
proc.WaitForExit()
+ lastDafnyExitCode <- proc.ExitCode
} |> Async.RunSynchronously
// =======================================================
@@ -49,7 +54,6 @@ let RunDafnyProgram dafnyProgram suffix = /// Checks whether the given dafny program verifies
// =======================================================
let CheckDafnyProgram dafnyProgram suffix =
- // TODO: also check whether Dafny produced any other errors (e.g. compilation errors, etc.)
let models = RunDafnyProgram dafnyProgram suffix
// if there are no models, verification was successful
- models.Count = 0
+ lastDafnyExitCode = 0 && models.Count = 0
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs index e4f6e0a0..54d0dc43 100644 --- a/Jennisys/Jennisys/Printer.fs +++ b/Jennisys/Jennisys/Printer.fs @@ -34,7 +34,9 @@ let PrintVarName vd = let rec PrintExpr ctx expr = match expr with - | IntLiteral(n) -> sprintf "%O" n + | IntLiteral(n) -> sprintf "%d" n + | BoolLiteral(b) -> sprintf "%b" b + | VarLiteral(id) | IdLiteral(id) -> id | Star -> "*" | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id @@ -44,10 +46,12 @@ let rec PrintExpr ctx expr = let openParen = if needParens then "(" else "" let closeParen = if needParens then ")" else "" sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen + | IteExpr(c,e1,e2) -> sprintf "%s ? %s : %s" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2) | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v) - | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0)) + | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep " " (PrintExpr 0)) | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e) + | SetExpr(ee) -> sprintf "{%s}" (ee |> PrintSep " " (PrintExpr 0)) | ForallExpr(vv,e) -> let needParens = ctx <> 0 let openParen = if needParens then "(" else "" @@ -119,7 +123,7 @@ let rec PrintConst cst = match cst with | IntConst(v) -> sprintf "%d" v | BoolConst(b) -> sprintf "%b" b - | SetConst(cset) -> cset.ToString() //TODO: this won't work + | SetConst(cset) -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset)) | SeqConst(cseq) -> let seqCont = cseq |> List.fold (fun acc c -> let sep = if acc = "" then "" else ", " @@ -131,5 +135,4 @@ let rec PrintConst cst = | ThisConst(_,_) -> "this" | NewObj(name,_) -> PrintGenSym name | ExprConst(e) -> PrintExpr 0 e - | VarConst(name) -> name | Unresolved(name) -> sprintf "Unresolved(%s)" name
\ No newline at end of file diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs index c6bb1991..f87ce5bd 100644 --- a/Jennisys/Jennisys/Resolver.fs +++ b/Jennisys/Jennisys/Resolver.fs @@ -1,19 +1,33 @@ -module Resolver
+// ####################################################################
+/// Utilities for resolving the "Unresolved" constants with respect to
+/// a given context (heap/env/ctx)
+///
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+// ####################################################################
+
+module Resolver
open Ast
+open AstUtils
open Printer
open EnvUtils
// resolving values
exception ConstResolveFailed of string
-let rec ResolveCont cst (env,ctx) failResolver =
+// ================================================================
+/// Resolves a given Const (cst) with respect to a given env/ctx.
+///
+/// If unable to resolve, it just delegates the task to the
+/// failResolver function
+// ================================================================
+let rec ResolveCont (env,ctx) failResolver cst =
match cst with
| Unresolved(_) as u ->
// see if it is in the env map first
let envVal = Map.tryFind cst env
match envVal with
- | Some(c) -> ResolveCont c (env,ctx) failResolver
+ | Some(c) -> ResolveCont (env,ctx) failResolver c
| None ->
// not found in the env map --> check the equality sets
let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)
@@ -27,53 +41,60 @@ let rec ResolveCont cst (env,ctx) failResolver = | _ -> failResolver cst (env,ctx)
| _ -> failResolver cst (env,ctx)
| SeqConst(cseq) ->
- let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont c (env,ctx) failResolver :: acc) []
+ let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont (env,ctx) failResolver c :: acc) []
SeqConst(resolvedLst)
| SetConst(cset) ->
- let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont c (env,ctx) failResolver)) Set.empty
+ let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont (env,ctx) failResolver c)) Set.empty
SetConst(resolvedSet)
| _ -> cst
-let TryResolve cst (env,ctx) =
- ResolveCont cst (env,ctx) (fun c (e,x) -> c)
-
-let Resolve cst (env,ctx) =
- ResolveCont cst (env,ctx) (fun c (e,x) -> raise (ConstResolveFailed("failed to resolve " + c.ToString())))
-
-
+// =====================================================================
+/// Tries to resolve a given Const (cst) with respect to a given env/ctx.
+///
+/// If unable to resolve, just returns the original Unresolved const.
+// =====================================================================
+let TryResolve (env,ctx) cst =
+ ResolveCont (env,ctx) (fun c (e,x) -> c) cst
-let rec EvalUnresolved expr (heap,env,ctx) =
- match expr with - | IntLiteral(n) -> IntConst(n) - | IdLiteral(id) when id = "this" -> GetThisLoc env - | IdLiteral(id) -> EvalUnresolved (Dot(IdLiteral("this"), id)) (heap,env,ctx) - | Dot(e, str) -> - let discr = EvalUnresolved e (heap,env,ctx) - let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList - match h2 with - | ((_,_),x) :: [] -> x - | _ :: _ -> failwithf "can't evaluate expression deterministically: %s.%s resolves to multiple locations." (PrintConst discr) str - | [] -> failwithf "can't find value for %s.%s" (PrintConst discr) str - | SelectExpr(lst, idx) -> - let lstC = Resolve (EvalUnresolved lst (heap,env,ctx)) (env,ctx) - let idxC = EvalUnresolved idx (heap,env,ctx) - match lstC, idxC with - | SeqConst(clist), IntConst(n) -> clist.[n] - | _ -> failwith "can't eval SelectExpr" - | _ -> failwith "NOT IMPLEMENTED YET" //TODO finish this! -// | Star -// | SelectExpr(_) -// | UpdateExpr(_) -// | SequenceExpr(_) -// | SeqLength(_) -// | ForallExpr(_) -// | UnaryExpr(_) -// | BinaryExpr(_) - -// TODO: can this be implemented on top of the existing AstUtils.EvalSym?? We must! -let Eval expr (heap,env,ctx) =
- try
- let unresolvedConst = EvalUnresolved expr (heap,env,ctx)
- Some(TryResolve unresolvedConst (env,ctx))
- with
- ex -> None
\ No newline at end of file +// ==============================================================
+/// Resolves a given Const (cst) with respect to a given env/ctx.
+///
+/// If unable to resolve, raises a ConstResolveFailed exception
+// ==============================================================
+let Resolve (env,ctx) cst =
+ ResolveCont (env,ctx) (fun c (e,x) -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) cst
+
+// =================================================================
+/// Evaluates a given expression with respect to a given heap/env/ctx
+// =================================================================
+let Eval (heap,env,ctx) resolveVars expr =
+ let rec __EvalResolver expr =
+ match expr with
+ | VarLiteral(id) when not resolveVars -> ExprConst(expr)
+ | IdLiteral("this") -> GetThisLoc env
+ | VarLiteral(id)
+ | IdLiteral(id) ->
+ match TryResolve (env,ctx) (Unresolved(id)) with
+ | Unresolved(_) -> __EvalResolver (Dot(IdLiteral("this"), id))
+ | _ as c -> c
+ | Dot(e, str) ->
+ let discr = __EvalResolver e
+ let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList
+ match h2 with
+ | ((_,_),x) :: [] -> x
+ | _ :: _ -> failwithf "can't evaluate expression deterministically: %s.%s resolves to multiple locations." (PrintConst discr) str
+ | [] -> failwithf "can't find value for %s.%s" (PrintConst discr) str
+ | _ -> failwith "NOT IMPLEMENTED YET"
+// try
+ EvalSym (fun e -> __EvalResolver e |> Resolve (env,ctx) |> Const2Expr) expr
+// ccc |> Const2Expr
+// match ccc with
+// | ExprConst(eee) -> match Eval (heap,env,ctx) eee with
+// | Some(c) -> c
+// | None -> ccc
+// | _ -> ccc
+// ) expr
+
+ //Some(TryResolve (env,ctx) unresolvedConst)
+// with
+// ex -> None
\ No newline at end of file diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs index 6540173c..b7db5706 100644 --- a/Jennisys/Jennisys/Utils.fs +++ b/Jennisys/Jennisys/Utils.fs @@ -1,6 +1,8 @@ -/// Various utility functions
+// ####################################################################
+/// Various utility functions
///
-/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+// ####################################################################
module Utils
@@ -9,6 +11,28 @@ module Utils // -------------------------------------------
// =====================================
+/// ensures: ret = b ? Some(b) : None
+// =====================================
+let BoolToOption b =
+ if b then
+ Some(b)
+ else
+ None
+
+// =====================================
+/// ensures: ret = (opt == Some(_))
+// =====================================
+let IsSomeOption opt =
+ match opt with
+ | Some(_) -> true
+ | None -> false
+
+// =====================================
+/// ensures: ret = (opt == None)
+// =====================================
+let IsNoneOption opt = IsSomeOption opt |> not
+
+// =====================================
/// requres: x = Some(a) or failswith msg
/// ensures: ret = a
// =====================================
@@ -24,21 +48,23 @@ let ExtractOptionMsg msg x = let ExtractOption x =
ExtractOptionMsg "can't extract anything from a None" x
-// =============================
-/// requres: List.length lst <= 1
+// ==========================================================
+/// requres: List.length lst <= 1, otherwise fails with errMsg
/// ensures: if |lst| = 0 then
/// ret = None
/// else
/// ret = Some(lst[0])
-// =============================
-let ListToOption lst =
+// ==========================================================
+let ListToOptionMsg lst errMsg =
if List.length lst > 1 then
- failwith "given list contains more than one element"
+ failwith errMsg
if List.isEmpty lst then
None
else
Some(lst.[0])
+let ListToOption lst = ListToOptionMsg lst "given list contains more than one element"
+
// =============================================================
/// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i])
// =============================================================
@@ -47,36 +73,40 @@ let rec ConvertToOptionList lst = | fs :: rest -> Some(fs) :: ConvertToOptionList rest
| [] -> []
-// =============================
-/// requres: Seq.length seq <= 1
+// =========================================================
+/// requres: Seq.length seq <= 1, otherwise fails with errMsg
/// ensures: if |seq| = 0 then
/// ret = None
/// else
/// ret = Some(seq[0])
-// =============================
-let SeqToOption seq =
+// =========================================================
+let SeqToOptionMsg seq errMsg =
if Seq.length seq > 1 then
- failwith "given seq contains more than one element"
+ failwith errMsg
if Seq.isEmpty seq then
None
else
Some(Seq.nth 0 seq)
-// =============================
-/// requires: Set.count set <= 1
+let SeqToOption seq = SeqToOptionMsg seq "given seq contains more than one element"
+
+// =========================================================
+/// requires: Set.count set <= 1, otherwise fails with errMsg
/// ensures: if |set| = 0 then
/// ret = None
/// else
/// ret = Some(set[0])
-// =============================
-let SetToOption set =
+// =========================================================
+let SetToOptionMsg set errMsg =
if Set.count set > 1 then
- failwith "give set contains more than one value"
+ failwith errMsg
if (Set.isEmpty set) then
None
else
Some(set |> Set.toList |> List.head)
+let SetToOption set = SetToOptionMsg set "give set contains more than one value"
+
// ============================================================
/// requires: n >= 0
/// ensures: |ret| = n && forall i :: 0 <= i < n ==> ret[i] = e
@@ -164,15 +194,9 @@ let (|Prefix|_|) (p:string) (s:string) = Some(s.Substring(p.Length))
else
None
-
-let (|Exact|_|) (p:string) (s:string) =
- if s = p then
- Some(s)
- else
- None
-
+
// -------------------------------------------
-// ----------------- random ------------------
+// --------------- workflow ------------------
// -------------------------------------------
let IfDo1 cond func1 a =
@@ -187,3 +211,15 @@ let IfDo2 cond func2 (a1,a2) = else
a1,a2
+type CascadingBuilder<'a>(failVal: 'a) =
+ member this.Bind(v, f) =
+ match v with
+ | Some(x) -> f x
+ | None -> failVal
+ member this.Return(v) = v
+
+// -------------------------------------------
+// --------------- random --------------------
+// -------------------------------------------
+
+let Iden x = x
\ No newline at end of file diff --git a/Jennisys/Jennisys/examples/Set.jen b/Jennisys/Jennisys/examples/Set.jen new file mode 100644 index 00000000..6404bfd6 --- /dev/null +++ b/Jennisys/Jennisys/examples/Set.jen @@ -0,0 +1,52 @@ +class Set { + var elems: set[int] + + constructor Empty() + ensures elems = {} + + constructor Singleton(t: int) + ensures elems = {t} + + constructor Sum(p: int, q: int) + ensures elems = {p + q} + + constructor Double(p: int, q: int) + requires p != q + ensures elems = {p q} +} + +model Set { + var root: SetNode + + frame + root * root.elems[*] + + invariant + root = null ==> elems = {} + root != null ==> elems = root.elems +} + +class SetNode { + var elems: set[int] + + constructor Init(t: int) + ensures elems = {t} + + constructor Double(p: int, q: int) + requires p != q + ensures elems = {p q} +} + +model SetNode { + var data: int + var left: SetNode + var right: SetNode + + frame + data * left * right + + invariant + elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {}) + left != null ==> forall e :: e in left.elems ==> e < data + right != null ==> forall e :: e in right.elems ==> e > data +} diff --git a/Jennisys/Jennisys/scripts/StartDafny-jen.bat b/Jennisys/Jennisys/scripts/StartDafny-jen.bat index 79d39a38..6f44ec4c 100644 --- a/Jennisys/Jennisys/scripts/StartDafny-jen.bat +++ b/Jennisys/Jennisys/scripts/StartDafny-jen.bat @@ -1,3 +1,2 @@ @echo off
"c:/boogie/Binaries/Dafny.exe" -nologo -compile:0 /print:xxx.bpl -timeLimit:60 %* > c:\tmp\jen-doo.out
-exit 43
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 06af76d1..665cf33f 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -188,7 +188,7 @@ Dafny theModules.Add(module); .)
| ClassDecl<defaultModule, out c> (. defaultModule.TopLevelDecls.Add(c); .)
| DatatypeDecl<defaultModule, out dt> (. defaultModule.TopLevelDecls.Add(dt); .)
- | ClassMemberDecl<membersDefaultClass>
+ | ClassMemberDecl<membersDefaultClass, false>
}
(. if (defaultModuleCreatedHere) {
defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
@@ -225,7 +225,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c> [ "refines" Ident<out idRefined> (. optionalId = idRefined; .)
]
"{" (. bodyStart = t; .)
- { ClassMemberDecl<members>
+ { ClassMemberDecl<members, true>
}
"}"
(. if (optionalId == null)
@@ -237,7 +237,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c> .)
.
-ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm.>
+ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
= (. Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
@@ -248,8 +248,8 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm.> | "unlimited" (. mmod.IsUnlimited = true; .)
}
( FieldDecl<mmod, mm>
- | FunctionDecl<mmod, out f> (. mm.Add(f); .)
- | MethodDecl<mmod, out m> (. mm.Add(m); .)
+ | FunctionDecl<mmod, out f> (. mm.Add(f); .)
+ | MethodDecl<mmod, allowConstructors, out m> (. mm.Add(m); .)
| CouplingInvDecl<mmod, mm>
)
.
@@ -404,7 +404,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.> /*------------------------------------------------------------------------*/
-MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
+MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id;
Attributes attrs = null;
@@ -422,8 +422,13 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m> IToken bodyEnd = Token.NoToken;
.)
( "method"
- | "constructor" (. isConstructor = true; .)
- | "refines" (. isRefinement = true; .)
+ | "constructor" (. if (allowConstructor) {
+ isConstructor = true;
+ } else {
+ SemErr(t, "constructors are only allowed in classes");
+ }
+ .)
+ | "refines" (. isRefinement = true; .)
)
(. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
@@ -443,9 +448,9 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m> Formals<false, !mmod.IsGhost, outs>
]
- ( ";" { MethodSpec<req, mod, ens, dec> }
- | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb, out bodyStart, out bodyEnd> (. body = (BlockStmt)bb; .)
- )
+ { MethodSpec<req, mod, ens, dec> }
+ [ BlockStmt<out bb, out bodyStart, out bodyEnd> (. body = (BlockStmt)bb; .)
+ ]
(. if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -594,11 +599,9 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> Formals<true, isFunctionMethod, formals>
":"
Type<out returnType>
- ( ";"
- { FunctionSpec<reqs, reads, ens, decreases> }
- | { FunctionSpec<reqs, reads, ens, decreases> }
- FunctionBody<out bb, out bodyStart, out bodyEnd> (. body = bb; .)
- )
+ { FunctionSpec<reqs, reads, ens, decreases> }
+ [ FunctionBody<out bb, out bodyStart, out bodyEnd> (. body = bb; .)
+ ]
(. f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index f730ea75..15a3f65d 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -230,7 +230,7 @@ namespace Microsoft.Dafny { PrintFormals(f.Formals);
wr.Write(": ");
PrintType(f.ResultType);
- wr.WriteLine(f.Body == null ? ";" : "");
+ wr.WriteLine();
int ind = indent + IndentAmount;
PrintSpec("requires", f.Req, ind);
@@ -277,7 +277,7 @@ namespace Microsoft.Dafny { }
PrintFormals(method.Outs);
}
- wr.WriteLine(method.Body == null ? ";" : "");
+ wr.WriteLine();
int ind = indent + IndentAmount;
PrintSpec("requires", method.Req, ind);
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 73f7fc71..afd36aa8 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -34,23 +34,27 @@ namespace Microsoft.Boogie // ------------------------------------------------------------------------
// Main
- public static void Main (string[] args)
+ public static int Main (string[] args)
{Contract.Requires(cce.NonNullElements(args));
//assert forall{int i in (0:args.Length); args[i] != null};
+ ExitValue exitValue = ExitValue.VERIFIED;
CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
if (CommandLineOptions.Clo.Parse(args) != 1)
{
+ exitValue = ExitValue.PREPROCESSING_ERROR;
goto END;
}
if (CommandLineOptions.Clo.Files.Count == 0)
{
ErrorWriteLine("*** Error: No input files were specified.");
+ exitValue = ExitValue.PREPROCESSING_ERROR;
goto END;
}
if (CommandLineOptions.Clo.XmlSink != null) {
string errMsg = CommandLineOptions.Clo.XmlSink.Open();
if (errMsg != null) {
ErrorWriteLine("*** Error: " + errMsg);
+ exitValue = ExitValue.PREPROCESSING_ERROR;
goto END;
}
}
@@ -76,11 +80,12 @@ namespace Microsoft.Boogie {
ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy).", file,
extension == null ? "" : extension);
+ exitValue = ExitValue.PREPROCESSING_ERROR;
goto END;
}
}
CommandLineOptions.Clo.RunningBoogieOnSsc = false;
- ProcessFiles(CommandLineOptions.Clo.Files);
+ exitValue = ProcessFiles(CommandLineOptions.Clo.Files);
END:
if (CommandLineOptions.Clo.XmlSink != null) {
@@ -91,6 +96,7 @@ namespace Microsoft.Boogie Console.WriteLine("Press Enter to exit.");
Console.ReadLine();
}
+ return (int)exitValue;
}
public static void ErrorWriteLine(string s) {Contract.Requires(s != null);
@@ -136,14 +142,16 @@ namespace Microsoft.Boogie enum FileType { Unknown, Cil, Bpl, Dafny };
- static void ProcessFiles (List<string/*!*/>/*!*/ fileNames)
+ static ExitValue ProcessFiles (List<string/*!*/>/*!*/ fileNames)
{
Contract.Requires(cce.NonNullElements(fileNames));
+ ExitValue exitValue = ExitValue.VERIFIED;
using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {
Dafny.Program dafnyProgram;
string programName = fileNames.Count == 1 ? fileNames[0] : "the program";
string err = Dafny.Main.ParseCheck(fileNames, programName, out dafnyProgram);
if (err != null) {
+ exitValue = ExitValue.DAFNY_ERROR;
ErrorWriteLine(err);
} else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
Dafny.Translator translator = new Dafny.Translator();
@@ -164,10 +172,11 @@ namespace Microsoft.Boogie int errorCount, verified, inconclusives, timeOuts, outOfMemories;
PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
+ bool allOk = errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0;
switch (oc) {
case PipelineOutcome.VerificationCompleted:
WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
- if ((CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) || CommandLineOptions.Clo.ForceCompile)
+ if ((CommandLineOptions.Clo.Compile && allOk) || CommandLineOptions.Clo.ForceCompile)
CompileDafnyProgram(dafnyProgram);
break;
case PipelineOutcome.Done:
@@ -179,8 +188,10 @@ namespace Microsoft.Boogie // error has already been reported to user
break;
}
+ exitValue = allOk ? ExitValue.VERIFIED : ExitValue.NOT_VERIFIED;
}
}
+ return exitValue;
}
private static void CompileDafnyProgram(Dafny.Program dafnyProgram)
@@ -373,7 +384,8 @@ namespace Microsoft.Boogie enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }
-
+ enum ExitValue { VERIFIED = 0, PREPROCESSING_ERROR, DAFNY_ERROR, NOT_VERIFIED }
+
/// <summary>
/// Resolves and type checks the given Boogie program. Any errors are reported to the
/// console. Returns:
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 50a8f45c..06f680fa 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -776,6 +776,5 @@ namespace Microsoft.Boogie p.Run();
return p.resModels;
}
-
}
}
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 3de94555..7cf3de07 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -12,13 +12,13 @@ class Queue<T> {
var contents: seq<T>;
- method Init();
+ method Init()
modifies this;
ensures |contents| == 0;
- method Enqueue(x: T);
+ method Enqueue(x: T)
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: T);
+ method Dequeue() returns (x: T)
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
@@ -33,7 +33,7 @@ class Queue<T> { }
class Comparable {
- function AtMost(c: Comparable): bool;
+ function AtMost(c: Comparable): bool
reads this, c;
}
@@ -96,7 +96,6 @@ class Benchmark3 { }
-
method RemoveMin(q: Queue<int>) returns (m: int, k: int) //m is the min, k is m's index in q
requires q != null && |q.contents| != 0;
modifies q;
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index f34f5c00..d6759c5f 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -8,13 +8,13 @@ class Queue<T> {
var contents: seq<T>;
- method Init();
+ method Init()
modifies this;
ensures |contents| == 0;
- method Enqueue(x: T);
+ method Enqueue(x: T)
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: T);
+ method Dequeue() returns (x: T)
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
@@ -101,7 +101,7 @@ class Stream { class Client {
- method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>);
+ method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)
requires q != null;
modifies q;
ensures r != null && fresh(r);
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 0c9d1186..383bccfd 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -6,13 +6,13 @@ class Queue<T> {
var contents: seq<T>;
- method Init();
+ method Init()
modifies this;
ensures |contents| == 0;
- method Enqueue(x: T);
+ method Enqueue(x: T)
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: T);
+ method Dequeue() returns (x: T)
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
@@ -28,7 +28,7 @@ class Queue<T> { class Glossary {
- method Sort(q: Queue<Word>) returns (r: Queue<Word>, perm:seq<int>);
+ method Sort(q: Queue<Word>) returns (r: Queue<Word>, perm:seq<int>)
requires q != null;
modifies q;
ensures r != null && fresh(r);
@@ -149,29 +149,29 @@ class Glossary { class Word
{
- function AtMost(w:Word) :bool;
+ function AtMost(w: Word): bool
}
class ReaderStream {
- ghost var footprint:set<object>;
- var isOpen:bool;
+ ghost var footprint: set<object>;
+ var isOpen: bool;
- function Valid():bool
- reads this, footprint;
+ function Valid(): bool
+ reads this, footprint;
{
null !in footprint && this in footprint && isOpen
}
method Open() //reading
- modifies this;
- ensures Valid() && fresh(footprint -{this});
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
{
footprint := {this};
isOpen :=true;
}
- method GetWord()returns(x:Word)
- requires Valid() ;
+ method GetWord() returns (x: Word)
+ requires Valid();
modifies footprint;
ensures Valid() && fresh(footprint - old(footprint));
{
@@ -190,8 +190,8 @@ class WriterStream { var stream:seq<int>;
var isOpen:bool;
- function Valid():bool
- reads this, footprint;
+ function Valid(): bool
+ reads this, footprint;
{
null !in footprint && this in footprint && isOpen
}
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 8df1a7c5..2063eec4 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -44,17 +44,17 @@ class SoWellformed { c := true;
}
- method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);
+ method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
requires next != null;
modifies this;
ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null)
- method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+ method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
requires next != null;
modifies s;
ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null)
- method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+ method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
requires next != null && this !in s;
modifies s;
ensures next.xyz < 100; // fine
@@ -175,7 +175,7 @@ class StatementTwoShoes { }
function G(w: int): int { 5 }
- function method H(x: int): int;
+ function method H(x: int): int
method V(s: set<StatementTwoShoes>, a: int, b: int)
modifies s;
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 53d3bf03..e56b4122 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -42,7 +42,7 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) { r := t1;
}
-function method FenEric<T>(t0: T, t1: T): T;
+function method FenEric<T>(t0: T, t1: T): T
datatype Pair<T> = Pr(T, T);
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index d4d1dfcf..f31935af 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -87,7 +87,7 @@ class Termination { }
}
- method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);
+ method Traverse<T>(a: List<T>) returns (val: T, b: List<T>)
requires a != List.Nil;
ensures a == List.Cons(val, b);
}
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index 2bedd37d..710e9838 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -88,7 +88,7 @@ method N() returns (k: MyClass) k := new MyClass;
}
-function NF(): MyClass;
+function NF(): MyClass
function TakesADatatype(a: List): int { 12 }
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index a3698dc0..8f3f8b87 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -17,7 +17,7 @@ class C<U> { assert kz && (G() || !G());
}
- function G<Y>(): Y;
+ function G<Y>(): Y
}
class SetTest {
@@ -99,7 +99,7 @@ class CClient { // -------------------------
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool;
+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
requires c == c || c in people;
method FindCelebrity3(people: set<int>, ghost c: int)
@@ -110,7 +110,7 @@ method FindCelebrity3(people: set<int>, ghost c: int) b := F(c, people);
}
-static function F(c: int, people: set<int>): bool;
+static function F(c: int, people: set<int>): bool
requires IsCelebrity(c, people);
function RogerThat<G>(g: G): G
@@ -153,8 +153,8 @@ method LoopyRoger(n: int) class TyKn_C<T> {
var x: T;
- function G(): T;
- method M() returns (t: T);
+ function G(): T
+ method M() returns (t: T)
}
class TyKn_K {
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 74512e01..21b895aa 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -1,6 +1,6 @@ // Celebrity example, inspired by the Rodin tutorial
-static function method Knows<Person>(a: Person, b: Person): bool;
+static function method Knows<Person>(a: Person, b: Person): bool
requires a != b; // forbid asking about the reflexive case
static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index fdce6dc7..39e14ea5 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -163,7 +163,7 @@ function mapF(xs: List): List case Nil => Nil
case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))
}
-function HardcodedUninterpretedFunction(n: Nat): Nat;
+function HardcodedUninterpretedFunction(n: Nat): Nat
function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List
{
@@ -195,7 +195,7 @@ function filterP(xs: List): List then Cons(y, filterP(ys))
else filterP(ys)
}
-function HardcodedUninterpretedPredicate(n: Nat): Bool;
+function HardcodedUninterpretedPredicate(n: Nat): Bool
function insort(n: Nat, xs: List): List
{
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index 189ff2b5..c8419890 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -29,7 +29,7 @@ class UltraFilter<G> { }
// Dafny currently does not have a set comprehension expression, so this method stub will have to do
- method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>);
+ method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)
ensures (forall X :: X in h <==> M + X in f);
method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
|