diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 4c11e00f0..242f2acc4 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2671,8 +2671,8 @@ public override void Emit(TokenTextWriter stream, int level) { } public class Function : DeclWithFormals { public string Comment; - // the body is only set if the function is declared with {:inline} - public Expr Body; + public Expr Body; // Only set if the function is declared with {:inline} + public NAryExpr DefinitionBody; // Only set if the function is declared with {:define} public Axiom DefinitionAxiom; public IList otherDefinitionAxioms; @@ -2755,12 +2755,20 @@ public override void Emit(TokenTextWriter stream, int level) { stream.Write(this, level, "function "); EmitAttributes(stream); if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline")) { + Contract.Assert(DefinitionBody == null); // Boogie inlines any function whose .Body field is non-null. The parser populates the .Body field - // is the :inline attribute is present, but if someone creates the Boogie file directly as an AST, then + // if the :inline attribute is present, but if someone creates the Boogie file directly as an AST, then // the :inline attribute may not be there. We'll make sure it's printed, so one can see that this means // that the body will be inlined. stream.Write("{:inline} "); } + if (DefinitionBody != null && !QKeyValue.FindBoolAttribute(Attributes, "define")) { + // Boogie defines any function whose .DefinitionBody field is non-null. The parser populates the .DefinitionBody field + // if the :define attribute is present, but if someone creates the Boogie file directly as an AST, then + // the :define attribute may not be there. We'll make sure it's printed, so one can see that this means + // that the function will be defined. + stream.Write("{:define} "); + } if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { stream.Write("h{0}^^{1}", this.GetHashCode(), TokenTextWriter.SanitizeIdentifier(this.Name)); } else { @@ -2768,12 +2776,20 @@ public override void Emit(TokenTextWriter stream, int level) { } EmitSignature(stream, true); if (Body != null) { + Contract.Assert(DefinitionBody == null); stream.WriteLine(); stream.WriteLine("{"); stream.Write(level + 1, ""); Body.Emit(stream); stream.WriteLine(); stream.WriteLine("}"); + } else if (DefinitionBody != null) { + stream.WriteLine(); + stream.WriteLine("{"); + stream.Write(level + 1, ""); + DefinitionBody.Args[1].Emit(stream); + stream.WriteLine(); + stream.WriteLine("}"); } else { stream.WriteLine(";"); } @@ -2791,11 +2807,15 @@ public override void Resolve(ResolutionContext rc) { RegisterFormals(InParams, rc); RegisterFormals(OutParams, rc); ResolveAttributes(rc); - if (Body != null) - { - rc.StateMode = ResolutionContext.State.StateLess; - Body.Resolve(rc); - rc.StateMode = ResolutionContext.State.Single; + if (Body != null) { + Contract.Assert(DefinitionBody == null); + rc.StateMode = ResolutionContext.State.StateLess; + Body.Resolve(rc); + rc.StateMode = ResolutionContext.State.Single; + } else if (DefinitionBody != null) { + rc.StateMode = ResolutionContext.State.StateLess; + DefinitionBody.Resolve(rc); + rc.StateMode = ResolutionContext.State.Single; } rc.PopVarContext(); Type.CheckBoundVariableOccurrences(TypeParameters, @@ -2814,11 +2834,21 @@ public override void Typecheck(TypecheckingContext tc) { base.Typecheck(tc); // TypecheckAttributes(tc); if (Body != null) { + Contract.Assert(DefinitionBody == null); Body.Typecheck(tc); if (!cce.NonNull(Body.Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type)) tc.Error(Body, "function body with invalid type: {0} (expected: {1})", Body.Type, cce.NonNull(OutParams[0]).TypedIdent.Type); + } else if (DefinitionBody != null) { + DefinitionBody.Typecheck(tc); + + // We are matching the type of the function body with output param, and not the type + // of DefinitionBody, which is always going to be bool (since it is of the form func_call == func_body) + if (!cce.NonNull(DefinitionBody.Args[1].Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type)) + tc.Error(DefinitionBody.Args[1], + "function body with invalid type: {0} (expected: {1})", + DefinitionBody.Args[1].Type, cce.NonNull(OutParams[0]).TypedIdent.Type); } } @@ -2871,6 +2901,36 @@ public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null) { DefinitionAxiom = new Axiom(tok, def); return DefinitionAxiom; } + + // Generates function definition of the form func_call == func_body + // For example, for + // function {:define} foo(x:int) returns(int) { x + 1 } + // this will generate + // foo(x):int == x + 1 + // We need the left hand call part later on to be able to generate + // the appropriate SMTlib style function definition. Hence, it is + // important that it goes through the resolution and type checking passes, + // since otherwise it is hard to connect function parameters to the resolved + // variables in the function body. + public NAryExpr CreateFunctionDefinition(Expr body) { + Contract.Requires(body != null); + + List callArgs = new List(); + int i = 0; + foreach (Formal/*!*/ f in InParams) { + Contract.Assert(f != null); + string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i; + callArgs.Add(new IdentifierExpr(f.tok, nm)); + i++; + } + + Expr call = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, Name)), callArgs); + // specify the type of the function, because it might be that + // type parameters only occur in the output type + call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone()); + NAryExpr def = Expr.Binary(tok, BinaryOperator.Opcode.Eq, call, body); + return def; + } } public class Macro : Function { diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index bb00b50d5..e9821e733 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -593,7 +593,7 @@ public override int GetHashCode() { public class ForallExpr : QuantifierExpr { public ForallExpr(IToken/*!*/ tok, List/*!*/ typeParams, - List/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false) + List/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable = false) : base(tok, typeParams, dummies, kv, triggers, body, immutable) { Contract.Requires(tok != null); Contract.Requires(typeParams != null); @@ -601,21 +601,21 @@ public ForallExpr(IToken/*!*/ tok, List/*!*/ typeParams, Contract.Requires(body != null); Contract.Requires(dummies.Count + typeParams.Count > 0); } - public ForallExpr(IToken tok, List dummies, Trigger triggers, Expr body, bool immutable=false) + public ForallExpr(IToken tok, List dummies, Trigger triggers, Expr body, bool immutable = false) : base(tok, new List(), dummies, null, triggers, body, immutable) { Contract.Requires(body != null); Contract.Requires(dummies != null); Contract.Requires(tok != null); Contract.Requires(dummies.Count > 0); } - public ForallExpr(IToken tok, List dummies, Expr body, bool immutable=false) + public ForallExpr(IToken tok, List dummies, Expr body, bool immutable = false) : base(tok, new List(), dummies, null, null, body, immutable) { Contract.Requires(body != null); Contract.Requires(dummies != null); Contract.Requires(tok != null); Contract.Requires(dummies.Count > 0); } - public ForallExpr(IToken tok, List typeParams, List dummies, Expr body, bool immutable=false) + public ForallExpr(IToken tok, List typeParams, List dummies, Expr body, bool immutable = false) : base(tok, typeParams, dummies, null, null, body, immutable) { Contract.Requires(body != null); Contract.Requires(dummies != null); @@ -639,7 +639,7 @@ public override BinderKind Kind { public class ExistsExpr : QuantifierExpr { public ExistsExpr(IToken/*!*/ tok, List/*!*/ typeParams, List/*!*/ dummies, - QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false) + QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable = false) : base(tok, typeParams, dummies, kv, triggers, body, immutable) { Contract.Requires(tok != null); Contract.Requires(typeParams != null); @@ -647,14 +647,14 @@ public ExistsExpr(IToken/*!*/ tok, List/*!*/ typeParams, List 0); } - public ExistsExpr(IToken tok, List dummies, Trigger triggers, Expr body, bool immutable=false) + public ExistsExpr(IToken tok, List dummies, Trigger triggers, Expr body, bool immutable = false) : base(tok, new List(), dummies, null, triggers, body, immutable) { Contract.Requires(body != null); Contract.Requires(dummies != null); Contract.Requires(tok != null); Contract.Requires(dummies.Count > 0); } - public ExistsExpr(IToken tok, List dummies, Expr body, bool immutable=false) + public ExistsExpr(IToken tok, List dummies, Expr body, bool immutable = false) : base(tok, new List(), dummies, null, null, body, immutable) { Contract.Requires(body != null); Contract.Requires(dummies != null); @@ -898,7 +898,7 @@ public override int GetHashCode() { public class LambdaExpr : BinderExpr { public LambdaExpr(IToken/*!*/ tok, List/*!*/ typeParameters, - List/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false) + List/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable = false) : base(tok, typeParameters, dummies, kv, body, immutable) { Contract.Requires(tok != null); Contract.Requires(typeParameters != null); diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 6da1d2cbf..e43f2656e 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -520,7 +520,13 @@ Function<.out List/*!*/ ds.> if (definition != null) { // generate either an axiom or a function body if (QKeyValue.FindBoolAttribute(kv, "inline")) { + if (QKeyValue.FindBoolAttribute(kv, "define")) + SemErr("function cannot have both :inline and :define attributes"); func.Body = definition; + } else if (QKeyValue.FindBoolAttribute(kv, "define")) { + if (func.TypeParameters.Count > 0) + SemErr("function with :define attribute has to be monomorphic"); + func.DefinitionBody = func.CreateFunctionDefinition(definition); } else { ds.Add(func.CreateDefinitionAxiom(definition, kv)); } diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index f3b649063..5fdfaa969 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1621,9 +1621,17 @@ result caching (default: "":0""). {:bvbuiltin ""spec""} Rewrite the function to built-in prover function symbol 'fn'. + {:define} + {:define true} + Turn this function into a definition (using the define-fun construct) + when using the SMT-LIB backend. Can only be used with non-recursive + functions. Cannot be combined with :inline attribute. + Currently works only with monomorphic functions. + {:inline} {:inline true} Expand function according to its definition before going to the prover. + Cannot be combined with :define attribute. {:never_pattern true} Terms starting with this function symbol will never be diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index ee6c8818d..281652983 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -427,7 +427,13 @@ void Function(out List/*!*/ ds) { if (definition != null) { // generate either an axiom or a function body if (QKeyValue.FindBoolAttribute(kv, "inline")) { + if (QKeyValue.FindBoolAttribute(kv, "define")) + SemErr("function cannot have both :inline and :define attributes"); func.Body = definition; + } else if (QKeyValue.FindBoolAttribute(kv, "define")) { + if (func.TypeParameters.Count > 0) + SemErr("function with :define attribute has to be monomorphic"); + func.DefinitionBody = func.CreateFunctionDefinition(definition); } else { ds.Add(func.CreateDefinitionAxiom(definition, kv)); } @@ -2426,4 +2432,4 @@ public FatalError(string m): base(m) {} } -} \ No newline at end of file +} diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 052a320bc..1b8167840 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -325,8 +325,11 @@ public virtual Function VisitFunction(Function node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); node = (Function)this.VisitDeclWithFormals(node); - if (node.Body != null) + if (node.Body != null) { + Contract.Assert(node.DefinitionBody == null); node.Body = this.VisitExpr(node.Body); + } else if (node.DefinitionBody != null) + node.DefinitionBody = (NAryExpr)this.VisitExpr(node.DefinitionBody); return node; } public virtual GlobalVariable VisitGlobalVariable(GlobalVariable node) { @@ -892,8 +895,11 @@ public override Function VisitFunction(Function node) { Contract.Ensures(Contract.Result() == node); node = (Function)this.VisitDeclWithFormals(node); - if (node.Body != null) - this.VisitExpr(node.Body); + if (node.Body != null) { + Contract.Assert(node.DefinitionBody == null); + this.VisitExpr(node.Body); + } else if (node.DefinitionBody != null) + this.VisitExpr(node.DefinitionBody); return node; } public override GlobalVariable VisitGlobalVariable(GlobalVariable node) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 46219a855..a57a364c0 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -24,6 +24,29 @@ namespace Microsoft.Boogie.SMTLib { + public class FunctionDependencyCollector : BoundVarTraversingVCExprVisitor { + private List functionList; + + // not used but required by interface + protected override bool StandardResult(VCExpr node, bool arg) { + return true; + } + + public List Collect(VCExpr expr) { + functionList = new List(); + Traverse(expr, true); + return functionList; + } + + public override bool Visit(VCExprNAry node, bool arg) { + VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp; + if (op != null) { + functionList.Add(op.Func); + } + return base.Visit(node, arg); + } + } + public class SMTLibProcessTheoremProver : ProverInterface { private readonly SMTLibProverContext ctx; @@ -225,6 +248,153 @@ private void FindDependentTypes(Type type, List dependentTypes) } } + private void PrepareDataTypes() + { + if (ctx.KnownDatatypeConstructors.Count > 0) + { + GraphUtil.Graph dependencyGraph = new GraphUtil.Graph(); + foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) + { + dependencyGraph.AddSource(datatype); + // Check for user-specified dependency (using ":dependson" attribute). + string userDependency = datatype.GetTypeDependency(); + if (userDependency != null) + { + dependencyGraph.AddEdge(datatype, ctx.LookupDatatype(userDependency)); + } + + foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) + { + List dependentTypes = new List(); + foreach (Variable v in f.InParams) + { + FindDependentTypes(v.TypedIdent.Type, dependentTypes); + } + + foreach (CtorType result in dependentTypes) + { + dependencyGraph.AddEdge(datatype, result); + } + } + } + + GraphUtil.StronglyConnectedComponents sccs = + new GraphUtil.StronglyConnectedComponents(dependencyGraph.Nodes, dependencyGraph.Predecessors, + dependencyGraph.Successors); + sccs.Compute(); + foreach (GraphUtil.SCC scc in sccs) + { + string datatypesString = ""; + string datatypeConstructorsString = ""; + foreach (CtorType datatype in scc) + { + datatypesString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " 0)"; + string datatypeConstructorString = ""; + foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) + { + string quotedConstructorName = Namer.GetQuotedName(f, f.Name); + datatypeConstructorString += "(" + quotedConstructorName + " "; + foreach (Variable v in f.InParams) + { + string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name); + datatypeConstructorString += "(" + quotedSelectorName + " " + + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") "; + } + + datatypeConstructorString += ") "; + } + + datatypeConstructorsString += "(" + datatypeConstructorString + ") "; + } + + List decls = DeclCollector.GetNewDeclarations(); + foreach (string decl in decls) + { + SendCommon(decl); + } + + SendCommon("(declare-datatypes (" + datatypesString + ") (" + datatypeConstructorsString + "))"); + } + } + } + + private void PrepareFunctionDefinitions() + { + // Collect all function definitions to be processed + Stack functionDefs = new Stack(); + foreach (Function f in ctx.DefinedFunctions.Keys) + { + DeclCollector.AddKnownFunction(f); // add func to knows funcs so that it does not get declared later on + functionDefs.Push(f); + } + + // Process each definition, but also be sure to process dependencies first in case one + // definition calls another. + // Also check for definition cycles. + List generatedFuncDefs = new List(); + FunctionDependencyCollector collector = new FunctionDependencyCollector(); + HashSet definitionAdded = new HashSet(); // whether definition has been fully processed + HashSet dependenciesComputed = new HashSet(); // whether dependencies have already been computed + while (functionDefs.Count > 0) { + Function f = functionDefs.Peek(); + if (definitionAdded.Contains(f)) { + // This definition was already processed (as a dependency of another definition) + functionDefs.Pop(); + continue; + } + + // Grab the definition and then compute the dependencies. + Contract.Assert(ctx.DefinedFunctions.ContainsKey(f)); + VCExprNAry defBody = ctx.DefinedFunctions[f]; + List dependencies = collector.Collect(defBody[1]); + bool hasDependencies = false; + foreach (Function fdep in dependencies) { + if (ctx.DefinedFunctions.ContainsKey(fdep) && !definitionAdded.Contains(fdep)) { + if (!dependenciesComputed.Contains(fdep)) { + // Handle dependencies first + functionDefs.Push(fdep); + hasDependencies = true; + } else { + HandleProverError("Function definition cycle detected: " + f.ToString() + " depends on " + fdep.ToString()); + } + } + } + + if (!hasDependencies) { + // No dependencies: go ahead and process this definition. + string funcDef = "(define-fun "; + var funCall = defBody[0] as VCExprNAry; + Contract.Assert(funCall != null); + VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)funCall.Op; + Contract.Assert(op != null); + funcDef += Namer.GetQuotedName(op.Func, op.Func.Name); + + funcDef += " ("; + foreach (var v in funCall.UniformArguments) { + VCExprVar varExpr = v as VCExprVar; + Contract.Assert(varExpr != null); + DeclCollector.AddKnownVariable(varExpr); // add var to knows vars so that it does not get declared later on + string printedName = Namer.GetQuotedLocalName(varExpr, varExpr.Name); + Contract.Assert(printedName != null); + funcDef += "(" + printedName + " " + SMTLibExprLineariser.TypeToString(varExpr.Type) + ") "; + } + funcDef += ") "; + + funcDef += SMTLibExprLineariser.TypeToString(defBody[0].Type) + " "; + funcDef += VCExpr2String(defBody[1], -1); + funcDef += ")"; + generatedFuncDefs.Add(funcDef); + definitionAdded.Add(f); + functionDefs.Pop(); + } else { + dependenciesComputed.Add(f); + } + } + + FlushAxioms(); // Flush all dependencies before flushing function definitions + generatedFuncDefs.Iter(SendCommon); // Flush function definitions + } + private void PrepareCommon() { if (common.Length == 0) @@ -265,63 +435,13 @@ private void PrepareCommon() SendCommon("(declare-fun timeoutDiagnostics (Int) Bool)"); } - if (ctx.KnownDatatypeConstructors.Count > 0) - { - GraphUtil.Graph dependencyGraph = new GraphUtil.Graph(); - foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) - { - dependencyGraph.AddSource(datatype); - // Check for user-specified dependency (using ":dependson" attribute). - string userDependency = datatype.GetTypeDependency(); - if (userDependency != null) { - dependencyGraph.AddEdge(datatype, ctx.LookupDatatype(userDependency)); - } - foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) - { - List dependentTypes = new List(); - foreach (Variable v in f.InParams) - { - FindDependentTypes(v.TypedIdent.Type, dependentTypes); - } - foreach (CtorType result in dependentTypes) - { - dependencyGraph.AddEdge(datatype, result); - } - } - } - GraphUtil.StronglyConnectedComponents sccs = new GraphUtil.StronglyConnectedComponents(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors); - sccs.Compute(); - foreach (GraphUtil.SCC scc in sccs) - { - string datatypesString = ""; - string datatypeConstructorsString = ""; - foreach (CtorType datatype in scc) - { - datatypesString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " 0)"; - string datatypeConstructorString = ""; - foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) - { - string quotedConstructorName = Namer.GetQuotedName(f, f.Name); - datatypeConstructorString += "(" + quotedConstructorName + " "; - foreach (Variable v in f.InParams) - { - string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name); - datatypeConstructorString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") "; - } - datatypeConstructorString += ") "; - } - datatypeConstructorsString += "(" + datatypeConstructorString + ") "; - } - List decls = DeclCollector.GetNewDeclarations(); - foreach (string decl in decls) - { - SendCommon(decl); - } - SendCommon("(declare-datatypes (" + datatypesString + ") (" + datatypeConstructorsString + "))"); - } + PrepareDataTypes(); + + if (CommandLineOptions.Clo.ProverPreamble != null) { + SendCommon("(include \"" + CommandLineOptions.Clo.ProverPreamble + "\")"); } - if (CommandLineOptions.Clo.ProverPreamble != null) - SendCommon("(include \"" + CommandLineOptions.Clo.ProverPreamble + "\")"); + + PrepareFunctionDefinitions(); } if (!AxiomsAreSetup) @@ -503,7 +623,7 @@ public override void FullReset(VCExpressionGenerator gen) SendThisVC("; did a full reset"); } } - + private string StripCruft(string name){ @@ -2221,7 +2341,7 @@ public override List UnsatCore() } public override void DefineMacro(Macro f, VCExpr vc) { - DeclCollector.AddFunction(f); + DeclCollector.AddKnownFunction(f); string printedName = Namer.GetQuotedName(f, f.Name); var argTypes = f.InParams.Cast().MapConcat(p => DeclCollector.TypeToStringReg(p.TypedIdent.Type), " "); string decl = "(define-fun " + printedName + " (" + argTypes + ") " + DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VCExpr2String(vc, 1) + ")"; @@ -2755,6 +2875,7 @@ public class SMTLibProverContext : DeclFreeProverContext internal SMTLibProcessTheoremProver parent; public readonly Dictionary> KnownDatatypeConstructors = new Dictionary>(); + public readonly Dictionary DefinedFunctions = new Dictionary(); public SMTLibProverContext(VCExpressionGenerator gen, VCGenerationOptions genOptions) @@ -2787,6 +2908,8 @@ public override void DeclareFunction(Function f, string attributes) { if (!KnownDatatypeConstructors.ContainsKey(datatype)) KnownDatatypeConstructors[datatype] = new List(); KnownDatatypeConstructors[datatype].Add(f); + } else if (f.DefinitionBody != null) { + DefinedFunctions.Add(f, (VCExprNAry)translator.Translate(f.DefinitionBody)); } base.DeclareFunction(f, attributes); } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index ea039afc5..caeb74f8e 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -185,12 +185,22 @@ public string TypeToStringReg(Type t) return TypeToString(t); } - public void AddFunction(Function func) { + public void AddKnownFunction(Function func) + { if (KnownFunctions.Contains(func)) return; KnownFunctions.Add(func); - if(declHandler != null) - declHandler.FuncDecl(func); + if (declHandler != null) + declHandler.FuncDecl(func); + } + + public void AddKnownVariable(VCExprVar variable) + { + if (KnownVariables.Contains(variable)) + return; + KnownVariables.Add(variable); + if (declHandler != null) + declHandler.VarDecl(variable); } public void RegisterRelation(Function func) @@ -258,9 +268,10 @@ public override bool Visit(VCExprVar node, bool arg) { { AddDeclaration(decl); } + KnownVariables.Add(node); - if(declHandler != null) - declHandler.VarDecl(node); + if (declHandler != null) + declHandler.VarDecl(node); } return base.Visit(node, arg); diff --git a/Test/civl/verified-ft-define.bpl b/Test/civl/verified-ft-define.bpl new file mode 100644 index 000000000..339245623 --- /dev/null +++ b/Test/civl/verified-ft-define.bpl @@ -0,0 +1,1214 @@ +/* + +Copyright (c) 2017, Cormac Flanagan (University of California, Santa Cruz) + Stephen Freund (Williams College) + James Wilcox (University of Washington) + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the names of the University of California, Santa Cruz + and Williams College nor the names of its contributors may be + used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +*/ + +/* + * Proof of VerifiedFT correctness in CIVL. + */ + +// RUN: %boogie -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +/* + * Tid + */ +type Tid = int; // make int so you can iterate over Tids +const unique nil: Tid; + +function {:define} ValidTid(tid : Tid): bool { + tid != nil && tid >= 0 +} + +/* + * datatype Epoch = Tid*Clock + */ +type{:datatype} Epoch; +function{:constructor} epoch(tid:Tid, clock:int):Epoch; + +const unique SHARED: Epoch; + +function {:define} EpochInc(e : Epoch): Epoch { + epoch(tid#epoch(e),clock#epoch(e) + 1) +} + +function {:define} EpochIsShared(e : Epoch): bool { + e == SHARED +} + +function {:define} EpochLeq(e1 : Epoch, e2 : Epoch): bool { + tid#epoch(e1) == tid#epoch(e2) && clock#epoch(e1) <= clock#epoch(e2) +} + +function {:define} max(a : int, b : int) : int { + if (a < b) then b else a +} + +function {:define} EpochMax(e1 : Epoch, e2 : Epoch): Epoch { + epoch(tid#epoch(e1), max(clock#epoch(e1), clock#epoch(e2))) +} + +function {:define} EpochInit(tid: Tid): Epoch { + epoch(tid, 0) +} + + +/* + * VC + */ +type VC = [Tid]Epoch; + +// primite accessors to array +// len of VC is stored at -1. +function {:define} VCArrayLen(vc: VC): int { clock#epoch(vc[-1]) } +function {:define} VCArraySetLen(vc: VC, n: int): VC { vc[-1 := epoch(-1,n)] } +function {:define} VCArrayGet(vc: VC, i: int): Epoch { vc[i] } + + +/* + * Shadow State + */ +type Lock; +type Var; + +/* + * datatype Shadowable = tid | lock | var + */ +type{:datatype} Shadowable; +function {:constructor} ShadowableTid(tid: Tid): Shadowable; +function {:constructor} ShadowableLock(l: Lock): Shadowable; +function {:constructor} ShadowableVar(x: Var): Shadowable; + +var {:layer 0,30} shadow.VC : [Shadowable] VC; +var {:layer 0,30} shadow.Lock : [Shadowable] Tid; +var {:layer 0,30} sx.W : [Var]Epoch; +var {:layer 0,30} sx.R : [Var]Epoch; + +/* + * Trace Invariant Support + */ +type ThreadStatus = int; +function{:define} UNUSED(): ThreadStatus { 0 } +function{:define} NEW(): ThreadStatus { 1 } +function{:define} RUNNING(): ThreadStatus { 2 } +function{:define} STOPPED(): ThreadStatus { 3 } + +var {:layer 0,30} thread.State: [Tid]ThreadStatus; // status of each thread +var {:layer 0,30} thread.ForkedBy: [Tid]Tid; // if forkedBy[t] = u, the u started t +var {:layer 0,30} thread.HasJoined: [Tid,Tid]bool; // if hasJoined[t,u], then t joined u. + + +/* + * Needed for [Read Share] + */ +const unique EMPTY_MAP: [Tid]Epoch; +axiom (forall i : Tid :: EMPTY_MAP[i] == EpochInit(i)); + +function {:define} VC.bottom(): VC { VCArraySetLen(EMPTY_MAP,0) } + + +/* + * State Invariants + */ +function {:inline false} VarsRepOk(w: [Var]Epoch, r: [Var]Epoch ): bool { + (forall v: Var :: ValidTid(tid#epoch(w[v]))) && + (forall v: Var :: r[v] == SHARED || (tid#epoch(r[v]) >= 0 && tid#epoch(r[v]) != nil)) +} + +function {:inline false} VCRepOk(vc: VC): bool { + VCArrayLen(vc) >= 0 && + (forall j: int :: {vc[j]} 0 <= j && j < VCArrayLen(vc) ==> clock#epoch(vc[j]) >= 0) && + (forall j: int :: {vc[j]} 0 <= j && j < VCArrayLen(vc) ==> tid#epoch(vc[j]) == j) && + (forall j: int :: VCArrayLen(vc) <= j ==> vc[j] == EpochInit(j)) +} + +function {:define} VCsRepOk(vcs: [Shadowable]VC): bool { + (forall s : Shadowable :: VCRepOk(vcs[s])) +} + +function {:define} FTRepOk(vcs: [Shadowable]VC, w: [Var]Epoch, r: [Var]Epoch): bool { + VCsRepOk(vcs) && + VarsRepOk(w, r) +} + + +/* + * Environment Assumptions -- what's preserved across yields + */ +function {:define} LocksPreserved({:linear "tid" } tid: Tid, oldLocks: [Shadowable] Tid, locks: [Shadowable]Tid): bool { + (forall v: Shadowable :: oldLocks[v] == tid ==> locks[v] == tid) +} + +function {:define} SharedInvPreserved(oldR: [Var] Epoch, r: [Var] Epoch): bool { + (forall x: Var :: oldR[x] == SHARED ==> r[x] == SHARED) +} + +function {:define} FTPreserved({:linear "tid" } tid:Tid, + oldLocks: [Shadowable] Tid, oldVcs: [Shadowable]VC, oldW: [Var]Epoch, oldR: [Var]Epoch, + locks: [Shadowable] Tid, vcs: [Shadowable]VC, w: [Var]Epoch, r: [Var]Epoch): bool { + LocksPreserved(tid, oldLocks, locks) && + SharedInvPreserved(oldR, r) && + (forall s: Shadowable :: oldLocks[s] == tid ==> vcs[s] == oldVcs[s]) && + (forall x: Var :: oldLocks[ShadowableVar(x)] == tid ==> r[x] == oldR[x]) && + (forall x: Var :: oldLocks[ShadowableVar(x)] == tid ==> w[x] == oldW[x]) +} + +/****** Layer 0 ******/ + +// VarState Lock +procedure {:yields} {:layer 0} {:refines "AtomicAcquireVarLock"} AcquireVarLock({:linear "tid"} tid: Tid, x : Var); +procedure {:right} {:layer 1,20} AtomicAcquireVarLock({:linear "tid"} tid: Tid, x : Var) +modifies shadow.Lock; +{ assert ValidTid(tid); assume shadow.Lock[ShadowableVar(x)] == nil; shadow.Lock[ShadowableVar(x)] := tid; } + +procedure {:yields} {:layer 0} {:refines "AtomicReleaseVarLock"} ReleaseVarLock({:linear "tid"} tid: Tid, x : Var); +procedure {:left} {:layer 1,20} AtomicReleaseVarLock({:linear "tid"} tid: Tid, x : Var) +modifies shadow.Lock; +{ assert ValidTid(tid); assert shadow.Lock[ShadowableVar(x)] == tid; shadow.Lock[ShadowableVar(x)] := nil; } + + +// ThreadState +procedure {:yields} {:layer 0} {:refines "AtomicThreadStateGetE"} ThreadStateGetE({:linear "tid"} tid: Tid) returns (e:Epoch); +procedure {:both} {:layer 1,20} AtomicThreadStateGetE({:linear "tid"} tid: Tid) returns (e:Epoch) +{ assert ValidTid(tid); assert shadow.Lock[ShadowableTid(tid)] == tid; e := shadow.VC[ShadowableTid(tid)][tid]; } + + +// VarState +procedure {:yields} {:layer 0} {:refines "AtomicVarStateSetW"} VarStateSetW({:linear "tid"} tid:Tid, x : Var, e:Epoch); +procedure {:atomic} {:layer 1,20} AtomicVarStateSetW({:linear "tid"} tid:Tid, x : Var, e:Epoch) +modifies sx.W; +{ assert ValidTid(tid); assert shadow.Lock[ShadowableVar(x)] == tid; sx.W[x] := e; } + +procedure {:yields} {:layer 0} {:refines "AtomicVarStateGetW"} VarStateGetW({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch); +procedure {:both} {:layer 1,20} AtomicVarStateGetW({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch) +{ assert ValidTid(tid); assert shadow.Lock[ShadowableVar(x)] == tid; e := sx.W[x]; } + +procedure {:yields} {:layer 0} {:refines "AtomicVarStateGetWNoLock"} VarStateGetWNoLock({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch); +procedure {:atomic} {:layer 1,20} AtomicVarStateGetWNoLock({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch) +{ assert ValidTid(tid); e := sx.W[x]; } + +procedure {:yields} {:layer 0} {:refines "AtomicVarStateSetR"} VarStateSetR({:linear "tid"} tid:Tid, x : Var, e:Epoch); +procedure {:atomic} {:layer 1,20} AtomicVarStateSetR({:linear "tid"} tid:Tid, x : Var, e:Epoch) +modifies sx.R; +{ assert ValidTid(tid); assert shadow.Lock[ShadowableVar(x)] == tid; assert sx.R[x] != SHARED; sx.R[x] := e; } + +procedure {:yields} {:layer 0} {:refines "AtomicVarStateGetRNoLock"} VarStateGetRNoLock({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch); +procedure {:atomic} {:layer 1,20} AtomicVarStateGetRNoLock({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch) +{ assert ValidTid(tid); e := sx.R[x]; } + +procedure {:yields} {:layer 0} {:refines "AtomicVarStateGetR"} VarStateGetR({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch); +procedure {:both} {:layer 1,20} AtomicVarStateGetR({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch) +{ assert ValidTid(tid); assert shadow.Lock[ShadowableVar(x)] == tid; e := sx.R[x]; } + +procedure {:yields} {:layer 0} {:refines "AtomicVarStateGetRShared"} VarStateGetRShared({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch); +procedure {:right} {:layer 1,20} AtomicVarStateGetRShared({:linear "tid"} tid:Tid, x : Var) returns (e:Epoch) +{ assert ValidTid(tid); assume sx.R[x] == SHARED; e := SHARED; } + + +// VCs + +procedure {:yields} {:layer 0} {:refines "AtomicVCGetSize"} VCGetSize({:linear "tid" } tid: Tid, r: Shadowable) returns (i: int); +procedure {:both} {:layer 1,10} AtomicVCGetSize({:linear "tid" } tid: Tid, r: Shadowable) returns (i: int) +{ + assert ValidTid(tid); + assert (shadow.Lock[r] == tid); + i := VCArrayLen(shadow.VC[r]); +} + +procedure {:yields} {:layer 0} {:refines "AtomicVCGetElem"} VCGetElem({:linear "tid" } tid: Tid, r: Shadowable, i: int) returns (e: Epoch); +procedure {:both} {:layer 1,20} AtomicVCGetElem({:linear "tid" } tid: Tid, r: Shadowable, i: int) returns (e: Epoch) +{ + assert ValidTid(tid); + assert (shadow.Lock[r] == tid); + e := VCArrayGet(shadow.VC[r], i); +} + +procedure {:yields} {:layer 0} {:refines "AtomicVCGetElemShared"} VCGetElemShared({:linear "tid" } tid: Tid, x : Var) returns (e: Epoch); +procedure {:atomic} {:layer 1,20} AtomicVCGetElemShared({:linear "tid" } tid: Tid, x : Var) returns (e: Epoch) +{ + assert sx.R[x] == SHARED; + assert ValidTid(tid); + e := VCArrayGet(shadow.VC[ShadowableVar(x)], tid); +} + +procedure {:yields} {:layer 0} {:refines "AtomicVCSetElemShared"} VCSetElemShared({:linear "tid" } tid: Tid, x : Var, e: Epoch); +procedure {:both} {:layer 1,20} AtomicVCSetElemShared({:linear "tid" } tid: Tid, x : Var, e: Epoch) +modifies shadow.VC; +{ + assert sx.R[x] == SHARED; + assert ValidTid(tid); + assert (shadow.Lock[ShadowableVar(x)] == tid); + shadow.VC[ShadowableVar(x)][tid] := e; + shadow.VC[ShadowableVar(x)] := VCArraySetLen(shadow.VC[ShadowableVar(x)], max(VCArrayLen(shadow.VC[ShadowableVar(x)]),tid+1)); +} + +procedure {:yields} {:layer 0} {:refines "AtomicVCSetElem"} VCSetElem({:linear "tid" } tid: Tid, r: Shadowable, i: int, e: Epoch); +procedure {:both} {:layer 1,20} AtomicVCSetElem({:linear "tid" } tid: Tid, r: Shadowable, i: int, e: Epoch) +modifies shadow.VC; +{ + assert is#ShadowableVar(r) ==> sx.R[x#ShadowableVar(r)] != SHARED; + assert ValidTid(tid); + assert (shadow.Lock[r] == tid); + shadow.VC[r][i] := e; + shadow.VC[r] := VCArraySetLen(shadow.VC[r], max(VCArrayLen(shadow.VC[r]),i+1)); +} + +procedure {:yields} {:layer 0} {:refines "AtomicVCInit"} VCInit({:linear "tid" } tid: Tid, r: Shadowable); +procedure {:both} {:layer 1,20} AtomicVCInit({:linear "tid" } tid: Tid, r: Shadowable) +modifies shadow.VC; +{ + assert ValidTid(tid); + assert is#ShadowableVar(r) ==> sx.R[x#ShadowableVar(r)] != SHARED; + assert (shadow.Lock[r] == tid); + shadow.VC[r] := VC.bottom(); +} + + +/****** Layer 10 -> 20 ******/ + + procedure {:yields} {:layer 10} Yield10({:linear "tid"} tid:Tid) + requires {:layer 10} ValidTid(tid); + requires {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + ensures {:layer 10} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10} FTPreserved(tid, old(shadow.Lock), old(shadow.VC), old(sx.W), old(sx.R), shadow.Lock, shadow.VC, sx.W, sx.R); + ensures {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + { + yield; + assert {:layer 10} ValidTid(tid); + assert {:layer 10} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + assert {:layer 10} FTPreserved(tid, old(shadow.Lock), old(shadow.VC), old(sx.W), old(sx.R), shadow.Lock, shadow.VC, sx.W, sx.R); + assert {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + } + +procedure {:both} {:layer 11,20} AtomicVC.Leq({:linear "tid"} tid: Tid, v1: Shadowable, v2: Shadowable) returns (res: bool) +{ + assert ValidTid(tid); + assert shadow.Lock[v1] == tid; + assert shadow.Lock[v2] == tid; + assert shadow.Lock[ShadowableTid(tid)] == tid; + assert is#ShadowableVar(v1) ==> sx.R[x#ShadowableVar(v1)] == SHARED; + assert !is#ShadowableVar(v2); + res := (forall j : int :: {f(j)} 0 <= j && f(j) ==> EpochLeq(VCArrayGet(shadow.VC[v1], j), VCArrayGet(shadow.VC[v2], j))); +} + +procedure {:yields} {:layer 10} {:refines "AtomicVC.Leq"} VC.Leq({:linear "tid"} tid: Tid, v1: Shadowable, v2: Shadowable) returns (res: bool) + requires {:layer 10} ValidTid(tid); + requires {:layer 10} shadow.Lock[v1] == tid; + requires {:layer 10} shadow.Lock[v2] == tid; + requires {:layer 10} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + requires {:layer 10} is#ShadowableVar(v1) ==> sx.R[x#ShadowableVar(v1)] == SHARED; + requires {:layer 10} !is#ShadowableVar(v2); + + ensures {:layer 10} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10} FTPreserved(tid, old(shadow.Lock), old(shadow.VC), old(sx.W), old(sx.R), shadow.Lock, shadow.VC, sx.W, sx.R); + ensures {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); +{ + var vc1, vc2: VC; + var len1, len2 : int; + var e1, e2: Epoch; + var i: int; + + call Yield10(tid); + + call len1 := VCGetSize(tid, v1); + call len2 := VCGetSize(tid, v1); + + i := 0; + while (i < max(len1, len2)) + invariant {:layer 10} 0 <= i; + invariant {:layer 10} (forall j : int :: {f(j)} + 0 <= j && j < i && f(j) ==> + EpochLeq(VCArrayGet(shadow.VC[v1], j), VCArrayGet(shadow.VC[v2], j))); + { + call e1 := VCGetElem(tid, v1, i); + call e2 := VCGetElem(tid, v2, i); + if (!EpochLeq(e1, e2)) { + assert {:layer 10} f(i); + res := false; + call Yield10(tid); + return; + } + + i := i + 1; + } + + res := true; + call Yield10(tid); + return; +} + +procedure {:both} {:layer 11,20} AtomicVC.Copy({:linear "tid"} tid: Tid, v1: Shadowable, v2: Shadowable) +modifies shadow.VC; +{ + assert ValidTid(tid); + assert v1 != v2; + assert shadow.Lock[ShadowableTid(tid)] == tid; + assert shadow.Lock[v1] == tid; + assert shadow.Lock[v2] == tid; + assert !is#ShadowableVar(v1); + assert !is#ShadowableVar(v2); + assert VCRepOk(shadow.VC[v2]); + assert VCRepOk(shadow.VC[v1]); + if (*) { + havoc shadow.VC; + assume VCRepOk(shadow.VC[v1]); + assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); + assume (forall j: int :: 0 <= j ==> VCArrayGet(shadow.VC[v1], j) == VCArrayGet(old(shadow.VC)[v2], j)); + assume shadow.VC == old(shadow.VC)[v1 := shadow.VC[v1]]; + } else { + shadow.VC[v1] := shadow.VC[v2]; + } +} + +procedure {:yields} {:layer 10} {:refines "AtomicVC.Copy"} VC.Copy({:linear "tid"} tid: Tid, v1: Shadowable, v2: Shadowable) + requires {:layer 10} ValidTid(tid); + requires {:layer 10} v1 != v2; + requires {:layer 10} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10} shadow.Lock[v1] == tid; + requires {:layer 10} shadow.Lock[v2] == tid; + requires {:layer 10} !is#ShadowableVar(v1); + requires {:layer 10} !is#ShadowableVar(v2); + requires {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + ensures {:layer 10} (forall s: Shadowable :: s != v1 && old(shadow.Lock)[s] == tid ==> old(shadow.VC)[s] == shadow.VC[s]); +{ + var len1, len2 : int; + var e1, e2: Epoch; + var i: int; + + var {:layer 10} oldVC : [Shadowable] [Tid]Epoch; + var {:layer 10} oldLock : [Shadowable] Tid; + + call Yield10(tid); + + call oldLock, oldVC := GhostRead(); + + call len1 := VCGetSize(tid, v1); + call len2 := VCGetSize(tid, v2); + + i := 0; + while (i < max(len1, len2)) + invariant {:layer 10} (forall s: Shadowable :: s != v1 ==> shadow.VC[s] == oldVC[s]); + invariant {:layer 10} (forall s: Shadowable :: oldLock[s] == tid ==> shadow.Lock[s] == tid); + invariant {:layer 10} VCRepOk(shadow.VC[v1]); + invariant {:layer 10} i >= 0; + invariant {:layer 10} i <= max(len1, len2); + invariant {:layer 10} VCArrayLen(shadow.VC[v1]) == max(len1, i); + invariant {:layer 10} (forall j : int :: 0 <= j && j < i ==> VCArrayGet(shadow.VC[v1], j) == VCArrayGet(shadow.VC[v2], j)); + invariant {:layer 10} (forall j : int :: max(len1, len2) <=j ==> VCArrayGet(shadow.VC[v1], j) == VCArrayGet(shadow.VC[v2], j)); + { + call e2 := VCGetElem(tid, v2, i); + call VCSetElem(tid, v1, i, e2); + i := i + 1; + } + + call Yield10(tid); +} + + +procedure {:right} {:layer 11,20} AtomicVC.Join({:linear "tid"} tid: Tid, v1: Shadowable, v2: Shadowable) +modifies shadow.VC; +{ + assert ValidTid(tid); + assert v1 != v2; + assert shadow.Lock[ShadowableTid(tid)] == tid; + assert shadow.Lock[v1] == tid; + assert shadow.Lock[v2] == tid; + assert !is#ShadowableVar(v1); + assert !is#ShadowableVar(v2); + assert VCRepOk(shadow.VC[v2]); + havoc shadow.VC; + assume VCRepOk(shadow.VC[v1]); + assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); + assume (forall j: int :: 0 <= j ==> VCArrayGet(shadow.VC[v1], j) == EpochMax(VCArrayGet(old(shadow.VC)[v1], j), VCArrayGet(old(shadow.VC)[v2], j))); + assume shadow.VC == old(shadow.VC)[v1 := shadow.VC[v1]]; +} + +procedure {:yields} {:layer 10} {:refines "AtomicVC.Join"} VC.Join({:linear "tid"} tid: Tid, v1: Shadowable, v2: Shadowable) + requires {:layer 10} ValidTid(tid); + requires {:layer 10} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10} shadow.Lock[v1] == tid; + requires {:layer 10} shadow.Lock[v2] == tid; + requires {:layer 10} !is#ShadowableVar(v1); + requires {:layer 10} !is#ShadowableVar(v2); + requires {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + ensures {:layer 10} (forall s: Shadowable :: s != v1 && old(shadow.Lock)[s] == tid ==> old(shadow.VC)[s] == shadow.VC[s]); +{ + var len1, len2 : int; + var e1, e2: Epoch; + var i: int; + + var {:layer 10} oldVC : [Shadowable] [Tid]Epoch; + var {:layer 10} oldLock : [Shadowable] Tid; + + call Yield10(tid); + + call oldLock, oldVC := GhostRead(); + + call len1 := VCGetSize(tid, v1); + call len2 := VCGetSize(tid, v2); + + i := 0; + while (i < max(len1, len2)) + invariant {:layer 10} (forall s: Shadowable :: s != v1 ==> shadow.VC[s] == oldVC[s]); + invariant {:layer 10} (forall s: Shadowable :: oldLock[s] == tid ==> shadow.Lock[s] == tid); + invariant {:layer 10} VCRepOk(shadow.VC[v1]); + invariant {:layer 10} i >= 0; + invariant {:layer 10} i <= max(len1, len2); + invariant {:layer 10} VCArrayLen(shadow.VC[v1]) == max(len1, i); + invariant {:layer 10} (forall j : int :: 0 <= j && i <= j ==> VCArrayGet(shadow.VC[v1], j) == VCArrayGet(oldVC[v1], j)); + invariant {:layer 10} (forall j : int :: 0 <= j && j < i ==> VCArrayGet(shadow.VC[v1], j) == EpochMax(VCArrayGet(oldVC[v1], j), VCArrayGet(shadow.VC[v2], j))); + { + call e1 := VCGetElem(tid, v1, i); + call e2 := VCGetElem(tid, v2, i); + call VCSetElem(tid, v1, i, EpochMax(e1, e2)); + i := i + 1; + } + + call Yield10(tid); +} + + +procedure {:intro} {:layer 10} GhostRead() returns (lock : [Shadowable]Tid, data : [Shadowable] [Tid]Epoch) +{ + lock := shadow.Lock; + data := shadow.VC; +} + +procedure {:both} {:layer 11,20} AtomicVC.Inc({:linear "tid" } tid: Tid, v: Shadowable, i: int) +modifies shadow.VC; +{ + assert ValidTid(tid); + assert shadow.Lock[ShadowableTid(tid)] == tid; + assert shadow.Lock[v] == tid; + assert !is#ShadowableVar(v); + assert i >= 0; + assert VCRepOk(shadow.VC[v]); + shadow.VC[v] := VCArraySetLen(shadow.VC[v], max(VCArrayLen(shadow.VC[v]), i+1)); + shadow.VC[v] := shadow.VC[v][i := EpochInc(shadow.VC[v][i])]; +} + +procedure {:yields} {:layer 10} {:refines "AtomicVC.Inc"} VC.Inc({:linear "tid" } tid: Tid, v: Shadowable, i: int) + requires {:layer 10} ValidTid(tid); + requires {:layer 10} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10} shadow.Lock[v] == tid; + requires {:layer 10} !is#ShadowableVar(v); + requires {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + requires {:layer 10} VCRepOk(shadow.VC[v]); + requires {:layer 10} i >= 0; + + ensures {:layer 10} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10} FTRepOk(shadow.VC, sx.W, sx.R); + ensures {:layer 10} VCRepOk(shadow.VC[v]); + ensures {:layer 10} (forall s: Shadowable :: s != v && old(shadow.Lock)[s] == tid ==> old(shadow.VC)[s] == shadow.VC[s]); +{ + var e: Epoch; + + call Yield10(tid); + + call e := VCGetElem(tid, v, i); + + call VCSetElem(tid, v, i, EpochInc(e)); + + call Yield10(tid); +} + + + +/****** Layer 20 --> 30 ******/ + + +procedure {:yields} {:layer 20} Yield20({:linear "tid"} tid:Tid) + requires {:layer 10,20} ValidTid(tid); + requires {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10,20} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10,20} FTPreserved(tid, old(shadow.Lock), old(shadow.VC), old(sx.W), old(sx.R), shadow.Lock, shadow.VC, sx.W, sx.R); + ensures {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); +{ + yield; + assert {:layer 10,20} ValidTid(tid); + assert {:layer 10,20} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + assert {:layer 10,20} FTPreserved(tid, old(shadow.Lock), old(shadow.VC), old(sx.W), old(sx.R), shadow.Lock, shadow.VC, sx.W, sx.R); + assert {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); +} + + +procedure {:atomic} {:layer 21,30} AtomicFork({:linear "tid"} tid:Tid, uid : Tid) +modifies shadow.VC; +{ + var v1,v2: Shadowable; + + assert ValidTid(tid); + assert ValidTid(uid); + assert shadow.Lock[ShadowableTid(tid)] == tid; + assert shadow.Lock[ShadowableTid(uid)] == tid; + assert tid != uid; + + v1 := ShadowableTid(uid); + v2 := ShadowableTid(tid); + + havoc shadow.VC; + + assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); + assume VCRepOk(shadow.VC[v1]); + assume (forall j: int :: 0 <= j ==> VCArrayGet(shadow.VC[v1], j) == EpochMax(VCArrayGet(old(shadow.VC)[v1], j), VCArrayGet(old(shadow.VC)[v2], j))); + + assume VCRepOk(shadow.VC[v2]); + assume VCArrayLen(shadow.VC[v2]) == max(VCArrayLen(shadow.VC[v2]), tid+1); + assume (forall j: int :: 0 <= j && j != tid ==> VCArrayGet(shadow.VC[v2], j) == VCArrayGet(old(shadow.VC)[v2], j)); + assume VCArrayGet(shadow.VC[v2], tid) == EpochInc(VCArrayGet(old(shadow.VC)[v2], tid)); + + assume shadow.VC == old(shadow.VC)[v1 := shadow.VC[v1]][v2 := shadow.VC[v2]]; +} + +procedure {:yields} {:layer 20} {:refines "AtomicFork"} Fork({:linear "tid"} tid:Tid, uid : Tid) + requires {:layer 10,20} ValidTid(tid); + requires {:layer 10,20} ValidTid(uid); + requires {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} shadow.Lock[ShadowableTid(uid)] == tid; + requires {:layer 10,20} tid != uid; + requires {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10,20} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + ensures {:layer 10,20} (forall s: Shadowable :: s != ShadowableTid(tid) && s != ShadowableTid(uid) ==> + (old(shadow.Lock)[s] == tid ==> old(shadow.VC)[s] == shadow.VC[s])); +{ + call Yield20(tid); + + call VC.Join(tid, ShadowableTid(uid), ShadowableTid(tid)); + + call VC.Inc(tid, ShadowableTid(tid), tid); + + call Yield20(tid); +} + + +procedure {:atomic} {:layer 21,30} AtomicJoin({:linear "tid"} tid:Tid, uid : Tid) +modifies shadow.VC; +{ + var v1, v2: Shadowable; + + assert ValidTid(tid); + assert ValidTid(uid); + assert shadow.Lock[ShadowableTid(tid)] == tid; + assert shadow.Lock[ShadowableTid(uid)] == tid; + assert tid != uid; + + v1 := ShadowableTid(uid); + v2 := ShadowableTid(tid); + + havoc shadow.VC; + assume VCArrayLen(shadow.VC[v2]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); + assume VCRepOk(shadow.VC[v2]); + assume (forall j: int :: 0 <= j ==> + VCArrayGet(shadow.VC[v2], j) == + EpochMax(VCArrayGet(old(shadow.VC)[v2], j), VCArrayGet(old(shadow.VC)[v1], j))); + assume shadow.VC == old(shadow.VC)[v2 := shadow.VC[v2]]; +} + +procedure {:yields} {:layer 20} {:refines "AtomicJoin"} Join({:linear "tid"} tid:Tid, uid : Tid) + requires {:layer 10,20} ValidTid(tid); + requires {:layer 10,20} ValidTid(uid); + requires {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} shadow.Lock[ShadowableTid(uid)] == tid; + requires {:layer 10,20} tid != uid; + requires {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10,20} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + ensures {:layer 10,20} (forall s: Shadowable :: s != ShadowableTid(tid) && old(shadow.Lock)[s] == tid ==> old(shadow.VC)[s] == shadow.VC[s]); +{ + call Yield20(tid); + call VC.Join(tid, ShadowableTid(tid), ShadowableTid(uid)); + call Yield20(tid); +} + + +procedure {:atomic} {:layer 21,30} AtomicAcquire({:linear "tid"} tid: Tid, l: Lock) +modifies shadow.VC; +{ + var v1, v2: Shadowable; + + assert ValidTid(tid); + assert shadow.Lock[ShadowableLock(l)] == tid; + assert shadow.Lock[ShadowableTid(tid)] == tid; + + v1 := ShadowableTid(tid); + v2 := ShadowableLock(l); + havoc shadow.VC; + assume VCRepOk(shadow.VC[v1]); + assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); + assume (forall j: int :: 0 <= j ==> + VCArrayGet(shadow.VC[v1], j) == + EpochMax(VCArrayGet(old(shadow.VC)[v1], j), VCArrayGet(old(shadow.VC)[v2], j))); + assume shadow.VC == old(shadow.VC)[v1 := shadow.VC[v1]]; +} + +procedure {:yields} {:layer 20} {:refines "AtomicAcquire"} Acquire({:linear "tid"} tid: Tid, l: Lock) + requires {:layer 10,20} ValidTid(tid); + requires {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} shadow.Lock[ShadowableLock(l)] == tid; + requires {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10,20} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + ensures {:layer 10,20} (forall s: Shadowable :: s != ShadowableTid(tid) && old(shadow.Lock)[s] == tid ==> old(shadow.VC)[s] == shadow.VC[s]); +{ + call Yield20(tid); + + call VC.Join(tid, ShadowableTid(tid), ShadowableLock(l)); + + call Yield20(tid); +} + +procedure {:atomic} {:layer 21,30} AtomicRelease({:linear "tid"} tid: Tid, l: Lock) +modifies shadow.VC; +{ + var v1,v2: Shadowable; + + assert ValidTid(tid); + assert shadow.Lock[ShadowableTid(tid)] == tid; + assert shadow.Lock[ShadowableLock(l)] == tid; + + v1 := ShadowableLock(l); + v2 := ShadowableTid(tid); + + havoc shadow.VC; + + // Use the same strategy as in Copy's atomic spec. + if (*) { + assume VCRepOk(shadow.VC[v1]); + assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); + assume (forall j: int :: 0 <= j ==> VCArrayGet(shadow.VC[v1], j) == VCArrayGet(old(shadow.VC)[v2], j)); + } else { + assume shadow.VC[v1] == old(shadow.VC)[v2]; + } + + assume VCRepOk(shadow.VC[v2]); + assume VCArrayLen(shadow.VC[v2]) == max(VCArrayLen(shadow.VC[v2]), tid+1); + assume (forall j: int :: 0 <= j && j != tid ==> VCArrayGet(shadow.VC[v2], j) == VCArrayGet(old(shadow.VC)[v2], j)); + assume VCArrayGet(shadow.VC[v2], tid) == EpochInc(VCArrayGet(old(shadow.VC)[v2], tid)); + + assume shadow.VC == old(shadow.VC)[v1 := shadow.VC[v1]][v2 := shadow.VC[v2]]; +} + +procedure {:yields} {:layer 20} {:refines "AtomicRelease"} Release({:linear "tid"} tid: Tid, l: Lock) + requires {:layer 10,20} ValidTid(tid); + requires {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} shadow.Lock[ShadowableLock(l)] == tid; + requires {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10,20} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + ensures {:layer 10,20} (forall s: Shadowable :: s != ShadowableTid(tid) && s != ShadowableLock(l) && old(shadow.Lock)[s] == tid ==> old(shadow.VC)[s] == shadow.VC[s]); +{ + var sm : Shadowable; + var st : Shadowable; + + call Yield20(tid); + + call VC.Copy(tid, ShadowableLock(l), ShadowableTid(tid)); + + call VC.Inc(tid, ShadowableTid(tid), tid); + + call Yield20(tid); +} + + +procedure {:atomic} {:layer 21,30} AtomicWrite({:linear "tid"} tid:Tid, x : Var) returns (ok : bool) +modifies sx.W; +{ + var st : Shadowable; + var sx : Shadowable; + + assert ValidTid(tid); + st := ShadowableTid(tid); + sx := ShadowableVar(x); + goto WriteFastPath, WriteExclusive, WritedShared, WriteWriteRace, ReadWriteRace, SharedWriteRace; + WriteFastPath: + ok := true; + assume sx.W[x] == VCArrayGet(shadow.VC[st], tid); + return; + WriteExclusive: + ok := true; + assume EpochLeq(sx.W[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.W[x]))); + assume sx.R[x] != SHARED; + assume EpochLeq(sx.R[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.R[x]))); + sx.W[x] := VCArrayGet(shadow.VC[st], tid); + return; + WritedShared: + ok := true; + assume EpochLeq(sx.W[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.W[x]))); + assume sx.R[x] == SHARED; + assume (forall j : int :: {f(j)} + 0 <= j && j < max(VCArrayLen(shadow.VC[sx]), VCArrayLen(shadow.VC[st])) && f(j) ==> + EpochLeq(VCArrayGet(shadow.VC[sx], j), VCArrayGet(shadow.VC[st], j))); + sx.W[x] := VCArrayGet(shadow.VC[st], tid); + return; + WriteWriteRace: + ok := false; + assume !EpochLeq(sx.W[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.W[x]))); + return; + ReadWriteRace: + ok := false; + assume sx.R[x] != SHARED; + assume !EpochLeq(sx.R[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.R[x]))); + return; + SharedWriteRace: + ok := false; + assume sx.R[x] == SHARED; + assume !(forall j : int :: {f(j)} + 0 <= j && j < max(VCArrayLen(shadow.VC[st]),VCArrayLen(shadow.VC[sx])) && f(j) ==> + EpochLeq(VCArrayGet(shadow.VC[sx], j), VCArrayGet(shadow.VC[st], j))); + return; +} + +procedure {:yields} {:layer 20} {:refines "AtomicWrite"} Write({:linear "tid"} tid:Tid, x : Var) returns (ok : bool) + requires {:layer 10,20} ValidTid(tid); + requires {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10,20} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); +{ + var e, w, vw, r, vr: Epoch; + + call Yield20(tid); + + call e := ThreadStateGetE(tid); + + // optional block + call w := VarStateGetWNoLock(tid, x); + if (w == e) { + // write same epoch + ok := true; + call Yield20(tid); + return; + } + + call Yield20(tid); + + call AcquireVarLock(tid, x); + call w := VarStateGetW(tid, x); + call vw := VCGetElem(tid, ShadowableTid(tid), tid#epoch(w)); + if (!EpochLeq(w, vw)) { + // write-write race + call ReleaseVarLock(tid, x); ok := false; call Yield20(tid); return; + } + call r := VarStateGetR(tid, x); + if (r != SHARED) { + call vr := VCGetElem(tid, ShadowableTid(tid), tid#epoch(r)); + if (!EpochLeq(r, vr)) { + // read-write race + call ReleaseVarLock(tid, x); ok := false; call Yield20(tid); return; + } + // write exclusive + call VarStateSetW(tid, x, e); + } else { + call ok := VC.Leq(tid, ShadowableVar(x), ShadowableTid(tid)); + if (!ok) { + // shared-write race + call ReleaseVarLock(tid, x); + ok := false; + call Yield20(tid); return; + } + // write shared + call VarStateSetW(tid, x, e); + } + + call ReleaseVarLock(tid, x); + ok := true; + call Yield20(tid); + return; +} + + +procedure {:atomic} {:layer 21,30} AtomicRead({:linear "tid"} tid:Tid, x : Var) returns (ok : bool) +modifies sx.R, shadow.VC; +{ + var st : Shadowable; + var sx : Shadowable; + + assert ValidTid(tid); + assert tid != nil && tid >= 0 && tid >= 0; + st := ShadowableTid(tid); + sx := ShadowableVar(x); + goto ReadSameEpoch, ReadSharedSameEpoch, ReadExclusive, ReadShared, ReadShare, WriteReadRace; + ReadSameEpoch: + ok := true; + assume sx.R[x] == VCArrayGet(shadow.VC[st], tid); + return; + ReadSharedSameEpoch: + ok := true; + assume sx.R[x] == SHARED; + assume VCArrayGet(shadow.VC[sx], tid) == VCArrayGet(shadow.VC[st], tid); + return; + ReadExclusive: + ok := true; + assume sx.R[x] != SHARED; + assume EpochLeq(sx.W[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.W[x]))); + assume EpochLeq(sx.R[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.R[x]))); + sx.R[x] := VCArrayGet(shadow.VC[st], tid); + return; + ReadShared: + ok := true; + assume sx.R[x] == SHARED; + assume EpochLeq(sx.W[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.W[x]))); + shadow.VC[sx][tid] := VCArrayGet(shadow.VC[st], tid); + shadow.VC[sx] := VCArraySetLen(shadow.VC[sx], max(VCArrayLen(shadow.VC[sx]), tid+1)); + return; + ReadShare: + assume sx.R[x] != SHARED; + assume EpochLeq(sx.W[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.W[x]))); + shadow.VC[sx] := VC.bottom(); + shadow.VC[sx][tid#epoch(sx.R[x])] := sx.R[x]; + shadow.VC[sx][tid] := VCArrayGet(shadow.VC[st], tid); + shadow.VC[sx] := VCArraySetLen(shadow.VC[sx], max(tid#epoch(sx.R[x])+1, tid+1)); + sx.R[x] := SHARED; + ok := true; + return; + WriteReadRace: + ok := false; + assume !EpochLeq(sx.W[x], VCArrayGet(shadow.VC[st], tid#epoch(sx.W[x]))); + return; +} + +procedure {:yields} {:layer 20} {:refines "AtomicRead"} Read({:linear "tid"} tid:Tid, x : Var) returns (ok : bool) + requires {:layer 10,20} ValidTid(tid); + requires {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 10,20} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); +{ + var e, w, vw, r, vr: Epoch; + var xVC, stVC: VC; + + call Yield20(tid); + + call e := ThreadStateGetE(tid); + + // optional block + if (*) { + // read same epoch + call r := VarStateGetRNoLock(tid, x); + assume r != SHARED; + if (r == e) { + ok := true; + call Yield20(tid); + return; + } + } else { + call r := VarStateGetRShared(tid, x); + assume r == SHARED; + call vw := VCGetElemShared(tid, x); + if (vw == e) { + ok := true; + call Yield20(tid); + return; + } + } + + call Yield20(tid); + + call AcquireVarLock(tid, x); + call w := VarStateGetW(tid, x); + call vw := VCGetElem(tid, ShadowableTid(tid), tid#epoch(w)); + if (!EpochLeq(w, vw)) { + // write-read race + call ReleaseVarLock(tid, x); + ok := false; + call Yield20(tid); + return; + } + call r := VarStateGetR(tid, x); + if (r != SHARED) { + call vr := VCGetElem(tid, ShadowableTid(tid), tid#epoch(r)); + if (EpochLeq(r, vr)) { + // Read Exclusive + assert {:layer 10,20} tid#epoch(e) >= 0; + call VarStateSetR(tid, x, e); + call ReleaseVarLock(tid, x); + ok := true; + call Yield20(tid); + return; + } else { + call VCInit(tid, ShadowableVar(x)); + call VCSetElem(tid, ShadowableVar(x), tid#epoch(r), r); + call VCSetElem(tid, ShadowableVar(x), tid, e); + call VarStateSetR(tid, x, SHARED); + call ReleaseVarLock(tid, x); + ok := true; + call Yield20(tid); + return; + } + } else { + // Read Shared + call VCSetElemShared(tid, x, e); + call ReleaseVarLock(tid, x); + ok := true; + call Yield20(tid); + return; + } +} + + +/****** Layer 30 --> 40 ******/ + + + +procedure {:yields} {:layer 30} Yield30({:linear "tid"} tid:Tid) + requires {:layer 10,20,30} ValidTid(tid); + requires {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + requires {:layer 30} thread.State[tid] == RUNNING(); + requires {:layer 30} (forall t: Tid :: thread.State[t] == UNUSED() ==> shadow.Lock[ShadowableTid(t)] == nil); + + ensures {:layer 10,20,30} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + ensures {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + ensures {:layer 30} thread.State[tid] == RUNNING(); + ensures {:layer 30} (forall t: Tid :: old(shadow.Lock)[ShadowableTid(t)] == tid ==> thread.State[t] == old(thread.State)[t]); + ensures {:layer 30} (forall t: Tid :: thread.State[t] == UNUSED() ==> shadow.Lock[ShadowableTid(t)] == nil); + +{ + yield; + + assert {:layer 10,20,30} ValidTid(tid); + + assert {:layer 10,20,30} LocksPreserved(tid, old(shadow.Lock), shadow.Lock); + assert {:layer 10,20} FTRepOk(shadow.VC, sx.W, sx.R); + + assert {:layer 10,20} FTPreserved(tid, old(shadow.Lock), old(shadow.VC), old(sx.W), old(sx.R), shadow.Lock, shadow.VC, sx.W, sx.R); + + assert {:layer 30} thread.State[tid] == RUNNING(); + assert {:layer 30} (forall t: Tid :: old(shadow.Lock)[ShadowableTid(t)] == tid ==> thread.State[t] == old(thread.State)[t]); + assert {:layer 30} (forall t: Tid :: thread.State[t] == UNUSED() ==> shadow.Lock[ShadowableTid(t)] == nil); +} + + +procedure {:yields} {:layer 30} Driver({:linear "tid"} tid:Tid) returns (ok: bool) + requires {:layer 10,20,30} ValidTid(tid); + requires {:layer 10,20,30} shadow.Lock[ShadowableTid(tid)] == tid; + requires {:layer 10,20} (forall s: Shadowable :: VCRepOk(shadow.VC[s])); + requires {:layer 10,20} VarsRepOk(sx.W, sx.R); + requires {:layer 30} thread.State[tid] == RUNNING(); + requires {:layer 30} (forall t: Tid :: thread.State[t] == UNUSED() ==> shadow.Lock[ShadowableTid(t)] == nil); +{ + var x: Var; + var l: Lock; + var uid: Tid; + call Yield30(tid); + ok := true; + while (ok) + invariant {:layer 10,20,30} ValidTid(tid); + invariant {:layer 10,20,30} shadow.Lock[ShadowableTid(tid)] == tid; + invariant {:layer 30} thread.State[tid] == RUNNING(); + invariant {:layer 10,20} (forall s: Shadowable :: VCRepOk(shadow.VC[s])); + invariant {:layer 10,20} VarsRepOk(sx.W, sx.R); + invariant {:layer 30} (forall t: Tid :: thread.State[t] == UNUSED() ==> shadow.Lock[ShadowableTid(t)] == nil); + { + if (*) { + havoc x; + call ok := Write(tid, x); + } else if (*) { + havoc x; + call ok := Read(tid, x); + } else if (*) { + assert {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + call l := ChooseLockToAcquire(tid); + call Yield30(tid); + call Acquire(tid, l); + } else if (*) { + call l := ChooseLockToRelease(tid); + call Yield30(tid); + call Release(tid, l); + call Yield30(tid); + call ReleaseChosenLock(tid, l); + call Yield30(tid); + } else if (*) { + call uid := AllocTid(tid); + assert {:layer 10,20} shadow.Lock[ShadowableTid(tid)] == tid; + assert {:layer 10,20} shadow.Lock[ShadowableTid(uid)] == tid; + assert {:layer 10,20} (forall s: Shadowable :: VCRepOk(shadow.VC[s])); + assert {:layer 10,20,30} tid != uid; + assert {:layer 10,20,30} ValidTid(tid); + assert {:layer 10,20,30} ValidTid(uid); + call Yield30(tid); + assert {:layer 10,20,30} ValidTid(tid); + assert {:layer 10,20,30} ValidTid(uid); + call Fork(tid, uid); + call Yield30(tid); + call StartThread(tid, uid); + call Yield30(tid); + } else { + call Yield30(tid); + call uid := ChooseThreadToJoin(tid); + call Yield30(tid); + call Join(tid, uid); + call Yield30(tid); + call ReleaseJoinLock(tid, uid); + call Yield30(tid); + } + call Yield30(tid); + assert {:layer 20} shadow.Lock[ShadowableTid(tid)] == tid; + } + yield; +} + +procedure {:yields} {:layer 0} {:refines "AtomicReleaseJoinLock"} ReleaseJoinLock({:linear "tid"} tid:Tid, uid: Tid); +procedure {:atomic} {:layer 1,30} AtomicReleaseJoinLock({:linear "tid"} tid:Tid, uid: Tid) +modifies shadow.Lock; +{ + assert ValidTid(tid); + assert ValidTid(uid); + assert tid != uid; + assert shadow.Lock[ShadowableTid(uid)] == tid; + shadow.Lock[ShadowableTid(uid)] := nil; +} + +procedure {:yields} {:layer 0} {:refines "AtomicChooseThreadToJoin"} ChooseThreadToJoin({:linear "tid"} tid:Tid) returns (uid: Tid); +procedure {:atomic} {:layer 1,30} AtomicChooseThreadToJoin({:linear "tid"} tid:Tid) returns (uid: Tid) +modifies shadow.Lock, thread.HasJoined; +{ + assert thread.State[tid] == RUNNING() && ValidTid(tid); + assume tid != uid; + assume thread.State[uid] == STOPPED() && ValidTid(uid); + assume shadow.Lock[ShadowableTid(uid)] == nil; + shadow.Lock[ShadowableTid(uid)] := tid; + thread.HasJoined[tid, uid] := true; +} + +procedure {:yields} {:layer 0} {:refines "AtomicAllocTid"} AllocTid({:linear "tid"} tid:Tid) returns (uid: Tid); +procedure {:atomic} {:layer 1,30} AtomicAllocTid({:linear "tid"} tid:Tid) returns (uid: Tid) +modifies thread.State, thread.ForkedBy, shadow.Lock; +{ + assert thread.State[tid] == RUNNING() && ValidTid(tid); + assert (forall t: Tid :: thread.State[t] == UNUSED() ==> shadow.Lock[ShadowableTid(t)] == nil); + assume tid != uid; + assume thread.State[uid] == UNUSED() && ValidTid(uid); + thread.State[uid] := NEW(); + thread.ForkedBy[uid] := tid; + shadow.Lock[ShadowableTid(uid)] := tid; + assume VCRepOk(shadow.VC[ShadowableTid(uid)]); +} + +procedure {:yields} {:layer 0} {:refines "AtomicStartThread"} StartThread({:linear "tid"} tid:Tid, uid: Tid); +procedure {:atomic} {:layer 1,30} AtomicStartThread({:linear "tid"} tid:Tid, uid: Tid) +modifies thread.State, shadow.Lock; +{ + assert ValidTid(tid); + assert ValidTid(uid); + assert tid != uid; + assert shadow.Lock[ShadowableTid(uid)] == tid; + assert thread.State[uid] == NEW(); + thread.State[uid] := RUNNING(); + shadow.Lock[ShadowableTid(uid)] := uid; +} + +procedure {:yields} {:layer 0} {:refines "AtomicChooseLockToAcquire"} ChooseLockToAcquire({:linear "tid"} tid:Tid) returns (l: Lock); +procedure {:atomic} {:layer 1,30} AtomicChooseLockToAcquire({:linear "tid"} tid:Tid) returns (l: Lock) +modifies shadow.Lock; +{ + assert ValidTid(tid); + assume shadow.Lock[ShadowableLock(l)] == nil; + shadow.Lock[ShadowableLock(l)] := tid; +} + +procedure {:yields} {:layer 0} {:refines "AtomicChooseLockToRelease"} ChooseLockToRelease({:linear "tid"} tid:Tid) returns (l: Lock); +procedure {:atomic} {:layer 1,30} AtomicChooseLockToRelease({:linear "tid"} tid:Tid) returns (l: Lock) +{ + assert ValidTid(tid); + assume shadow.Lock[ShadowableLock(l)] == tid; +} + +procedure {:yields} {:layer 0} {:refines "AtomicReleaseChosenLock"} ReleaseChosenLock({:linear "tid"} tid:Tid, l: Lock); +procedure {:atomic} {:layer 1,30} AtomicReleaseChosenLock({:linear "tid"} tid:Tid, l: Lock) +modifies shadow.Lock; +{ + assert ValidTid(tid); + assert shadow.Lock[ShadowableLock(l)] == tid; + shadow.Lock[ShadowableLock(l)] := nil; +} + + + + + + +// needed for linear Tids --- don't forget... +function {:builtin "MapConst"} TidMapConstBool(bool): [Tid]bool; + +function {:define} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +{ + TidMapConstBool(false)[x := true] +} + +// for matching quantifiers +function {:inline false} f(i: int): bool { true } + + + + +function +{:witness "shadow.VC"} +{:commutativity "AtomicVC.Inc","AtomicVC.Copy"} +{:commutativity "AtomicVC.Inc","AtomicVC.Join"} +{:commutativity "AtomicVCSetElem","AtomicVC.Copy"} +{:commutativity "AtomicVCSetElem","AtomicVC.Join"} +{:commutativity "AtomicVCSetElemShared","AtomicVC.Copy"} +{:commutativity "AtomicVCSetElemShared","AtomicVC.Join"} +{:commutativity "AtomicVCInit","AtomicVC.Copy"} +{:commutativity "AtomicVCInit","AtomicVC.Join"} +{:commutativity "AtomicVC.Copy","AtomicVC.Copy"} +{:commutativity "AtomicVC.Copy","AtomicVC.Join"} +{:commutativity "AtomicVC.Join","AtomicVC.Copy"} +{:commutativity "AtomicVC.Join","AtomicVC.Join"} +witness (shadow.VC:[Shadowable]VC, shadow.VC':[Shadowable]VC, second_v1:Shadowable) : [Shadowable]VC +{ + shadow.VC[second_v1 := shadow.VC'[second_v1]] +} diff --git a/Test/civl/verified-ft-define.bpl.expect b/Test/civl/verified-ft-define.bpl.expect new file mode 100644 index 000000000..50f2eca38 --- /dev/null +++ b/Test/civl/verified-ft-define.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 340 verified, 0 errors diff --git a/Test/civl/wsq-define.bpl b/Test/civl/wsq-define.bpl new file mode 100644 index 000000000..7b507ecf8 --- /dev/null +++ b/Test/civl/wsq-define.bpl @@ -0,0 +1,530 @@ +// RUN: %boogie -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Tid; +const nil: Tid; + +function {:builtin "MapConst"} MapConstBool(bool) : [Tid]bool; +function {:define} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +{ + MapConstBool(false)[x := true] +} + +var {:layer 0,3} H: int; +var {:layer 0,3} T: int; +var {:layer 0,3} items: [int]int; +var {:layer 0,4} status: [int]bool; +var {:layer 0,3} take_in_cs: bool; +var {:layer 0,3} put_in_cs: bool; +var {:layer 0,3} steal_in_cs: [Tid]bool; +var {:layer 0,3} h_ss: [Tid]int; +var {:layer 0,3} t_ss: [Tid]int; + +const IN_Q: bool; +const NOT_IN_Q: bool; +axiom IN_Q == true; +axiom NOT_IN_Q == false; + +const unique EMPTY: int; +const unique NIL: Tid; +const unique ptTid: Tid; +axiom ptTid != NIL; + +function {:define} stealerTid(tid: Tid):(bool) { tid != NIL && tid != ptTid } + +function {:define} ideasInv(put_in_cs:bool, + items:[int]int, + status: [int]bool, + H:int, T:int, + take_in_cs:bool, + steal_in_cs:[Tid]bool, + h_ss:[Tid]int, + t_ss:[Tid]int + ):(bool) +{ + ( + ( (take_in_cs) && h_ss[ptTid] < t_ss[ptTid] ==> (t_ss[ptTid] == T && H <= T && + items[T] != EMPTY && status[T] == IN_Q) ) && + (put_in_cs ==> !take_in_cs) && (take_in_cs ==> !put_in_cs) && + (( (take_in_cs) && H != h_ss[ptTid]) ==> H > h_ss[ptTid]) && + (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H == h_ss[td] && H < t_ss[td]) ==> (items[H] != EMPTY && status[H] == IN_Q)) && + (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H != h_ss[td]) ==> H > h_ss[td]) + ) +} + +function {:define} queueInv(steal_in_cs:[Tid]bool, + put_in_cs:bool, + take_in_cs:bool, + items:[int]int, status: [int]bool, _H:int, _T:int):(bool) +{ + ( (forall i:int :: (_H <= i && i <= _T) ==> (status[i] == IN_Q && items[i] != EMPTY)) ) +} + +function {:define} emptyInv(put_in_cs:bool, take_in_cs:bool, items:[int]int, status:[int]bool, T:int):(bool) +{ + (forall i:int :: (i>=T && !put_in_cs && !take_in_cs) ==> status[i] == NOT_IN_Q && items[i] == EMPTY) +} + +function {:define} putInv(items:[int]int, status: [int]bool, H:int, T:int):(bool) +{ + (forall i:int :: (H <= i && i < T) ==> (status[i] == IN_Q && items[i] != EMPTY)) +} + +function {:define} takeInv(items:[int]int, status: [int]bool, H:int, T:int, t:int, h:int):(bool) +{ + (forall i:int :: (h <= i && i <= t) ==> (status[i] == IN_Q && + items[i] != EMPTY) && + t == T + ) +} + +procedure {:atomic} {:layer 4} atomic_put({:linear "tid"} tid:Tid, task: int) +modifies status; +{ + var i: int; + assume status[i] == NOT_IN_Q; + status[i] := IN_Q; +} + +procedure {:yields} {:layer 3} {:refines "atomic_put"} put({:linear "tid"} tid:Tid, task: int) +requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && task != EMPTY && !take_in_cs && !put_in_cs; +requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +requires {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); +ensures {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; +ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); +{ + var t: int; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; + var {:layer 3} oldStatusT:bool; + + yield; + assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); + + call t := readT_put(tid); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs; + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} tid == ptTid && t == T; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); + + call writeItems_put(tid,t, task); + + call oldH, oldT := GhostRead(); + call oldStatusT := GhostReadStatus(); + yield; + assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs; + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} items[t] == task; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); + + + call writeT_put(tid, t+1); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} T == t + 1; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); +} + +procedure {:atomic} {:layer 4} atomic_take({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) +modifies status; +{ + var i: int; + if (*) { + assume status[i] == IN_Q; + status[i] := NOT_IN_Q; + } +} + +procedure {:yields} {:layer 3} {:refines "atomic_take"} take({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) +requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; +requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs && (task != EMPTY ==> taskstatus == IN_Q); +ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +{ + var h, t: int; + var chk: bool; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; + + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + + while(true) + invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + { + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && oldT == T; + + call t := readT_take_init(tid); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T; + assert {:layer 3} items[t-1] == EMPTY ==> H > t-1; + assert {:layer 3} oldH <= H && oldT == T; + + t := t-1; + call writeT_take(tid, t); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T; + assert {:layer 3} items[t] == EMPTY ==> H > t; + assert {:layer 3} oldH <= H && oldT == T; + + call h := readH_take(tid); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T; + assert {:layer 3} h <= H; + assert {:layer 3} items[t] == EMPTY ==> H > t; + assert {:layer 3} oldH <= H; + assert {:layer 3} oldT == T; + assert {:layer 3} h <= H; + assert {:layer 3} oldH == h; + + if (t= h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T && task == items[T]; + assert {:layer 3} T > H ==> items[T] != EMPTY; + assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && take_in_cs; + + if (t>h) { + call takeExitCS(tid); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T && task == items[t] && task != EMPTY && taskstatus == IN_Q; + assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && !take_in_cs; + return; + } + call writeT_take_eq(tid, h+1); + call oldH, oldT := GhostRead(); + + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} T == h + 1; + assert {:layer 3} oldH <= H; + assert {:layer 3} oldT == T; + assert {:layer 3} task == items[t]; + assert {:layer 3} !put_in_cs; + + call chk := CAS_H_take(tid, h,h+1); + + if (chk) { + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; + assert {:layer 3} oldH <= H && oldT == T && task != EMPTY && taskstatus == IN_Q; + return; + } + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; + assert {:layer 3} oldH <= H && oldT == T; + } + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && oldT == T; +} + +procedure {:atomic} {:layer 4} atomic_steal({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) +modifies status; +{ + var i: int; + if (*) { + assume status[i] == IN_Q; + status[i] := NOT_IN_Q; + } +} + +procedure {:yields} {:layer 3} {:refines "atomic_steal"} steal({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) +requires {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && stealerTid(tid) && + !steal_in_cs[tid]; +requires {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && + !steal_in_cs[tid] && (task != EMPTY ==> taskstatus == IN_Q); +ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +{ + var h, t: int; + var chk: bool; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; + + yield; + assert {:layer 3} stealerTid(tid); + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} !steal_in_cs[tid]; + + while(true) + invariant {:layer 3} stealerTid(tid); + invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + invariant {:layer 3} !steal_in_cs[tid]; + { + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} stealerTid(tid); + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + assert {:layer 3} !steal_in_cs[tid]; + + call h := readH_steal(tid); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} H >= h; + assert {:layer 3} !steal_in_cs[tid]; + assert {:layer 3} h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + + call t := readT_steal(tid); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} steal_in_cs[tid]; + assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && t == t_ss[tid]; + assert {:layer 3} (h < t && take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T); + assert {:layer 3} H >= h; + + if( h>= t) { + task := EMPTY; + call stealExitCS(tid); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} !steal_in_cs[tid]; + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + return; + } + + call task, taskstatus := readItems(tid, h); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + assert {:layer 3} oldH == H && H == h && h_ss[tid] == h ==> task != EMPTY; + assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T); + assert {:layer 3} h == H ==> status[H] == IN_Q; + + call chk := CAS_H_steal(tid, h,h+1); + if (chk) { + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && task != EMPTY; + return; + } + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} h_ss[tid] == h; + assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q); + assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && chk) ==> ((oldH-1) < T); + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} oldH <= H; + } + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} chk && task != EMPTY; + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; + assert {:layer 3} oldH <= H; +} + +procedure {:intro} {:layer 3} GhostRead() returns (oldH: int, oldT: int) +{ + oldH := H; + oldT := T; +} + +procedure {:intro} {:layer 3} GhostReadStatus() returns (oldStatus: bool) +{ + oldStatus := status[T]; +} + +procedure {:atomic} {:layer 1,3} atomic_readH_take({:linear "tid"} tid:Tid) returns (y: int) +modifies take_in_cs, h_ss; +{ assert tid == ptTid; y := H; take_in_cs := true; h_ss[tid] := H; } + +procedure {:yields} {:layer 0} {:refines "atomic_readH_take"} readH_take({:linear "tid"} tid:Tid) returns (y: int); + +procedure {:atomic} {:layer 1,3} atomic_readH_steal({:linear "tid"} tid:Tid) returns (y: int) +modifies h_ss; +{ assert stealerTid(tid); assert !steal_in_cs[tid]; y := H; h_ss[tid] := H; } + +procedure {:yields} {:layer 0} {:refines "atomic_readH_steal"} readH_steal({:linear "tid"} tid:Tid) returns (y: int); + +procedure {:atomic} {:layer 1,3} atomic_readT_take_init({:linear "tid"} tid:Tid) returns (y: int) +{ assert tid != NIL; assert tid == ptTid; y := T; } + +procedure {:yields} {:layer 0} {:refines "atomic_readT_take_init"} readT_take_init({:linear "tid"} tid:Tid) returns (y: int); + +procedure {:atomic} {:layer 1,3} atomic_readT_put({:linear "tid"} tid:Tid) returns (y: int) +modifies put_in_cs; +{ assert tid != NIL; assert tid == ptTid; put_in_cs := true; y := T; } + +procedure {:yields} {:layer 0} {:refines "atomic_readT_put"} readT_put({:linear "tid"} tid:Tid) returns (y: int); + +procedure {:atomic} {:layer 1,3} atomic_readT_steal({:linear "tid"} tid:Tid) returns (y: int) +modifies t_ss, steal_in_cs; +{ assert tid != NIL; assert stealerTid(tid); assert !steal_in_cs[tid]; y := T; t_ss[tid] := T; steal_in_cs[tid] := true; } + +procedure {:yields} {:layer 0} {:refines "atomic_readT_steal"} readT_steal({:linear "tid"} tid:Tid) returns (y: int); + +procedure {:atomic} {:layer 1,3} atomic_readItems({:linear "tid"} tid:Tid, ind: int) returns (y: int, b:bool) +{ y := items[ind]; b := status[ind]; } + +procedure {:yields} {:layer 0} {:refines "atomic_readItems"} readItems({:linear "tid"} tid:Tid, ind: int) returns (y: int, b:bool); + +procedure {:atomic} {:layer 1,3} atomic_writeT_put({:linear "tid"} tid:Tid, val: int) +modifies T, put_in_cs; +{ assert tid == ptTid; T := T+1; put_in_cs := false; } + +procedure {:yields} {:layer 0} {:refines "atomic_writeT_put"} writeT_put({:linear "tid"} tid:Tid, val: int); + +procedure {:atomic} {:layer 1,3} atomic_writeT_take({:linear "tid"} tid:Tid, val: int) +modifies T, t_ss; +{ assert tid == ptTid; T := val; t_ss[tid] := val; } + +procedure {:yields} {:layer 0} {:refines "atomic_writeT_take"} writeT_take({:linear "tid"} tid:Tid, val: int); + +procedure {:atomic} {:layer 1,3} atomic_writeT_take_abort({:linear "tid"} tid:Tid, val: int) +modifies T, take_in_cs; +{ assert tid == ptTid; assert take_in_cs; T := val; take_in_cs := false; } + +procedure {:yields} {:layer 0} {:refines "atomic_writeT_take_abort"} writeT_take_abort({:linear "tid"} tid:Tid, val: int); + +procedure {:atomic} {:layer 1,3} atomic_writeT_take_eq({:linear "tid"} tid:Tid, val: int) +modifies T; +{ assert tid == ptTid; T := val; } + +procedure {:yields} {:layer 0} {:refines "atomic_writeT_take_eq"} writeT_take_eq({:linear "tid"} tid:Tid, val: int); + +procedure {:atomic} {:layer 1,3} atomic_takeExitCS({:linear "tid"} tid:Tid) +modifies take_in_cs; +{ assert tid == ptTid; take_in_cs := false; } + +procedure {:yields} {:layer 0} {:refines "atomic_takeExitCS"} takeExitCS({:linear "tid"} tid:Tid); + +procedure {:atomic} {:layer 1,3} atomic_stealExitCS({:linear "tid"} tid:Tid) +modifies steal_in_cs; +{ assert stealerTid(tid); assert steal_in_cs[tid]; steal_in_cs[tid] := false; } + +procedure {:yields} {:layer 0} {:refines "atomic_stealExitCS"} stealExitCS({:linear "tid"} tid:Tid); + +procedure {:atomic} {:layer 1,3} atomic_writeItems({:linear "tid"} tid:Tid, idx: int, val: int) +modifies items, status; +{ assert tid == ptTid; assert val != EMPTY; items[idx] := val; status[idx] := IN_Q; } + +procedure {:yields} {:layer 0} {:refines "atomic_writeItems"} writeItems({:linear "tid"} tid:Tid, idx: int, val: int); + +procedure {:atomic} {:layer 1,3} atomic_writeItems_put({:linear "tid"} tid:Tid, idx: int, val: int) +modifies items, status; +{ assert tid == ptTid; assert val != EMPTY; items[idx] := val; status[idx] := IN_Q; } + +procedure {:yields} {:layer 0} {:refines "atomic_writeItems_put"} writeItems_put({:linear "tid"} tid:Tid, idx: int, val: int); + +procedure {:atomic} {:layer 1,3} atomic_CAS_H_take({:linear "tid"} tid:Tid, prevVal :int, val: int) returns (result: bool) +modifies status, H, take_in_cs; +{ + assert tid == ptTid; + if (H == prevVal) { + status[H] := NOT_IN_Q; + H := H+1; + result := true; + take_in_cs := false; + } else { + result := false; + take_in_cs := false; + } +} + +procedure {:yields} {:layer 0} {:refines "atomic_CAS_H_take"} CAS_H_take({:linear "tid"} tid:Tid, prevVal :int, val: int) returns (result: bool); + +procedure {:atomic} {:layer 1,3} atomic_CAS_H_steal({:linear "tid"} tid:Tid, prevVal :int, val: int) returns (result: bool) +modifies status, H, steal_in_cs; +{ + assert stealerTid(tid); + if (H == prevVal) { + status[H] := NOT_IN_Q; + H := H+1; + result := true; + steal_in_cs[tid] := false; + } else { + result := false; + steal_in_cs[tid] := false; + } +} + +procedure {:yields} {:layer 0} {:refines "atomic_CAS_H_steal"} CAS_H_steal({:linear "tid"} tid:Tid, prevVal :int, val: int) returns (result: bool); diff --git a/Test/civl/wsq-define.bpl.expect b/Test/civl/wsq-define.bpl.expect new file mode 100644 index 000000000..ac3dd058c --- /dev/null +++ b/Test/civl/wsq-define.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 22 verified, 0 errors diff --git a/Test/functiondefine/fundef.bpl b/Test/functiondefine/fundef.bpl new file mode 100644 index 000000000..6cea992be --- /dev/null +++ b/Test/functiondefine/fundef.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -proverLog:"%t1" -env:0 "%s" +// RUN: grep define "%t1" > "%t2" +// RUN: %diff "%s.expect" "%t2" + +function {:define} foo(x:int) returns(bool) + { foo2(x) > 0 } +function {:define} foo2(x:int) returns(int) + { x + 1 } + +procedure test(x:int) returns (r:int) + ensures r > 0; +{ + if (foo(x)) { + r := foo2(x); + } else { + r := 1; + } +} diff --git a/Test/functiondefine/fundef.bpl.expect b/Test/functiondefine/fundef.bpl.expect new file mode 100644 index 000000000..ab1536a68 --- /dev/null +++ b/Test/functiondefine/fundef.bpl.expect @@ -0,0 +1,2 @@ +(define-fun foo2 ((x Int) ) Int (+ x 1)) +(define-fun foo ((x@@0 Int) ) Bool (> (foo2 x@@0) 0)) diff --git a/Test/functiondefine/fundef1.bpl b/Test/functiondefine/fundef1.bpl new file mode 100644 index 000000000..df333f5a2 --- /dev/null +++ b/Test/functiondefine/fundef1.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -proverLog:"%t1" -env:0 "%s" +// RUN: grep define "%t1" > "%t2" +// RUN: %diff "%s.expect" "%t2" + +function {:define} foo(x:int) returns(bool) + { foo2(x, x) > 0 } +function {:define} foo2(x:int, y:int) returns(int) + { x + y } + +procedure test(x:int) returns (r:int) + ensures r > 0; +{ + if (foo(x)) { + r := foo2(x, x); + } else { + r := 1; + } +} diff --git a/Test/functiondefine/fundef1.bpl.expect b/Test/functiondefine/fundef1.bpl.expect new file mode 100644 index 000000000..853cae063 --- /dev/null +++ b/Test/functiondefine/fundef1.bpl.expect @@ -0,0 +1,2 @@ +(define-fun foo2 ((x Int) (y Int) ) Int (+ x y)) +(define-fun foo ((x@@0 Int) ) Bool (> (foo2 x@@0 x@@0) 0)) diff --git a/Test/functiondefine/fundef2.bpl b/Test/functiondefine/fundef2.bpl new file mode 100644 index 000000000..0c77bcdf9 --- /dev/null +++ b/Test/functiondefine/fundef2.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:define} foo(x:int) returns(bool) + { foo2(x, x) > 0 } +function {:define} foo2(x:int, y:int) returns(int) + { x + y } + +procedure test(x:int) returns (r:int) + ensures r > 0; +{ + if (foo(x)) { + r := foo2(x, x); + } else { + r := 1; + } +} + +procedure test1(x:int) returns (r:int) + ensures r > 0; +{ + if (foo(x)) { + r := foo2(x, -x); + } else { + r := 1; + } +} diff --git a/Test/functiondefine/fundef2.bpl.expect b/Test/functiondefine/fundef2.bpl.expect new file mode 100644 index 000000000..5ec025c0a --- /dev/null +++ b/Test/functiondefine/fundef2.bpl.expect @@ -0,0 +1,7 @@ +fundef2.bpl(24,3): Error BP5003: A postcondition might not hold on this return path. +fundef2.bpl(20,3): Related location: This is the postcondition that might not hold. +Execution trace: + fundef2.bpl(22,3): anon0 + fundef2.bpl(23,7): anon3_Then + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/functiondefine/fundef3.bpl b/Test/functiondefine/fundef3.bpl new file mode 100644 index 000000000..ce6e2565f --- /dev/null +++ b/Test/functiondefine/fundef3.bpl @@ -0,0 +1,16 @@ +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +var M:[int]int; +function {:define} store(M:[int]int, p:int, i:int) returns ([int]int) { M[p := i] } + +procedure test(ArgM:[int]int) returns (r:int) + ensures r == 20; +{ + var i:int; + var M:[int]int; + M := ArgM; + M[i] := 10; + M := store(M, i, 20); + r := M[i]; +} diff --git a/Test/functiondefine/fundef3.bpl.expect b/Test/functiondefine/fundef3.bpl.expect new file mode 100644 index 000000000..37fad75c9 --- /dev/null +++ b/Test/functiondefine/fundef3.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/functiondefine/fundef4.bpl b/Test/functiondefine/fundef4.bpl new file mode 100644 index 000000000..b0e88c86b --- /dev/null +++ b/Test/functiondefine/fundef4.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:define} foo(x:int) returns(bool) + { foo2(x) > 0 } +function {:define} {:inline} foo2(x:int) returns(int) + { x + 1 } + +procedure test(x:int) returns (r:int) + ensures r > 0; +{ + if (foo(x)) { + r := foo2(x); + } else { + r := 1; + } +} diff --git a/Test/functiondefine/fundef4.bpl.expect b/Test/functiondefine/fundef4.bpl.expect new file mode 100644 index 000000000..d6565ca03 --- /dev/null +++ b/Test/functiondefine/fundef4.bpl.expect @@ -0,0 +1,2 @@ +fundef4.bpl(7,11): error: function cannot have both :inline and :define attributes +1 parse errors detected in fundef4.bpl diff --git a/Test/functiondefine/fundef5.bpl b/Test/functiondefine/fundef5.bpl new file mode 100644 index 000000000..140e18499 --- /dev/null +++ b/Test/functiondefine/fundef5.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -proverLog:"%t1" -env:0 "%s" +// RUN: grep define "%t1" > "%t2" +// RUN: %diff "%s.expect" "%t2" + +function {:define true} foo(x:int) returns(bool) + { foo2(x) > 0 } +function {:define true} foo2(x:int) returns(int) + { x + 1 } + +procedure test(x:int) returns (r:int) + ensures r > 0; +{ + if (foo(x)) { + r := foo2(x); + } else { + r := 1; + } +} diff --git a/Test/functiondefine/fundef5.bpl.expect b/Test/functiondefine/fundef5.bpl.expect new file mode 100644 index 000000000..ab1536a68 --- /dev/null +++ b/Test/functiondefine/fundef5.bpl.expect @@ -0,0 +1,2 @@ +(define-fun foo2 ((x Int) ) Int (+ x 1)) +(define-fun foo ((x@@0 Int) ) Bool (> (foo2 x@@0) 0)) diff --git a/Test/functiondefine/fundef6.bpl b/Test/functiondefine/fundef6.bpl new file mode 100644 index 000000000..ba88ce16e --- /dev/null +++ b/Test/functiondefine/fundef6.bpl @@ -0,0 +1,10 @@ +// RUN: %boogie -print:- -env:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:define} foo(x:int) returns(bool) + { x > 0 } +function {:define true} foo1(x:int) returns(bool) + { x > 0 } +function {:define false} foo2(x:int) returns(bool) + { x > 0 } +function foo3(x:int) returns(bool) + { x > 0 } diff --git a/Test/functiondefine/fundef6.bpl.expect b/Test/functiondefine/fundef6.bpl.expect new file mode 100644 index 000000000..1bf6a54b1 --- /dev/null +++ b/Test/functiondefine/fundef6.bpl.expect @@ -0,0 +1,20 @@ + +function {:define} foo(x: int) : bool +{ + x > 0 +} + +function {:define true} foo1(x: int) : bool +{ + x > 0 +} + +function {:define false} foo2(x: int) : bool; + +axiom (forall x: int :: {:define false} { foo2(x): bool } foo2(x): bool == (x > 0)); + +function foo3(x: int) : bool; + +axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0)); + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/functiondefine/fundef7.bpl b/Test/functiondefine/fundef7.bpl new file mode 100644 index 000000000..be896f7c9 --- /dev/null +++ b/Test/functiondefine/fundef7.bpl @@ -0,0 +1,50 @@ +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// defined functions + +function Twice(x: int) returns (int) +{ + x + x +} + +function {:define} Double(x: int) returns (int) +{ + 3 * x - x +} + +function f(int) returns (int); +function g(int) returns (int); +function h(int) returns (int); +function k(int) returns (int); +axiom (forall x: int :: Twice(x) == f(x)); // here, Twice(x) and f(x) are both triggers +axiom (forall x: int :: Double(x) == g(x)); // if Double was inlined, the trigger would be just g(x); what is trigger when Double is defined? +axiom (forall x: int :: { f(x) } f(x) < h(x) ); +axiom (forall x: int :: { g(x) } g(x) < k(x) ); + +procedure P(a: int, b: int, c: int) +{ + // The following is provable, because Twice triggers its definition and the resulting f(a) + // triggers the relation to h(a). + assert Twice(a) < h(a); + if (*) { + // The following is NOT provable, it seems because Double is defined and thus no g(b) term is ever + // created; double-check this + assert Double(b) < k(b); // error + } else { + // The following IS provable, because the explicit g(c) will cause both of the necessary + // quantifiers to trigger + assert g(c) == 2*c; + assert Double(c) < k(c); + } +} + +// nullary functions + +function Five() returns (int) { 5 } + +function {:define} Eight() returns (e: int) { 8 } + +procedure Q() +{ + assert 8 * Five() == 5 * Eight(); +} diff --git a/Test/functiondefine/fundef7.bpl.expect b/Test/functiondefine/fundef7.bpl.expect new file mode 100644 index 000000000..8a24630cb --- /dev/null +++ b/Test/functiondefine/fundef7.bpl.expect @@ -0,0 +1,6 @@ +fundef7.bpl(32,5): Error BP5001: This assertion might not hold. +Execution trace: + fundef7.bpl(28,3): anon0 + fundef7.bpl(32,5): anon3_Then + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/functiondefine/fundef8.bpl b/Test/functiondefine/fundef8.bpl new file mode 100644 index 000000000..a600e6390 --- /dev/null +++ b/Test/functiondefine/fundef8.bpl @@ -0,0 +1,8 @@ +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:define} eqC2(x:alpha) returns (bool) { x == 2 } + +procedure P() { + assert eqC2(2, 2); +} diff --git a/Test/functiondefine/fundef8.bpl.expect b/Test/functiondefine/fundef8.bpl.expect new file mode 100644 index 000000000..bfee00f47 --- /dev/null +++ b/Test/functiondefine/fundef8.bpl.expect @@ -0,0 +1,2 @@ +fundef8.bpl(4,65): error: function with :define attribute has to be monomorphic +1 parse errors detected in fundef8.bpl diff --git a/Test/functiondefine/fundef9.bpl b/Test/functiondefine/fundef9.bpl new file mode 100644 index 000000000..282ce2131 --- /dev/null +++ b/Test/functiondefine/fundef9.bpl @@ -0,0 +1,19 @@ +// RUN: %boogie "%s" | %OutputCheck "%s" + +// CHECK-L: Prover error: Function definition cycle detected: foo depends on foo2 +function {:define} foo(x:int) returns(int) + { foo2(x) + 1 } +function {:define} foo2(x:int) returns(int) + { foo(x) + 2 } + +procedure test(x:int) returns (r:int) + ensures r > 0; +{ + if (foo(x) > 0) { + r := foo2(x); + } else { + r := 1; + } +} + +// CHECK-L: Boogie program verifier finished with 0 verified, 0 errors, 1 inconclusive diff --git a/Test/smack/git-issue-203-define.bpl b/Test/smack/git-issue-203-define.bpl new file mode 100644 index 000000000..7febc5b64 --- /dev/null +++ b/Test/smack/git-issue-203-define.bpl @@ -0,0 +1,2087 @@ +// generated by SMACK version 2.4.0 for boogie +// via /usr/local/bin/smack two_arrays.c --loop-limit=11 --unroll=11 --verifier=boogie --debug --bpl=pero.bpl + +// RUN: %boogie -doModSetAnalysis -timeLimit:1200 -errorLimit:1 -loopUnroll:15 -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// Basic types +type i1 = int; +type i5 = int; +type i6 = int; +type i8 = int; +type i16 = int; +type i24 = int; +type i32 = int; +type i40 = int; +type i48 = int; +type i56 = int; +type i64 = int; +type i80 = int; +type i88 = int; +type i96 = int; +type i128 = int; +type i160 = int; +type i256 = int; +type ref = i64; +type float; + +// Basic constants +const $0: i32; +axiom ($0 == 0); +const $1: i32; +axiom ($1 == 1); +const $0.ref: ref; +axiom ($0.ref == 0); +const $1.ref: ref; +axiom ($1.ref == 1); +const $1024.ref: ref; +axiom ($1024.ref == 1024); +// Memory model constants +const $GLOBALS_BOTTOM: ref; +const $EXTERNS_BOTTOM: ref; +const $MALLOC_TOP: ref; + +// Memory maps (3 regions) +var $M.0: [ref] i32; +var $M.1: ref; +var $M.2: i32; + +// Memory address bounds +axiom ($GLOBALS_BOTTOM == $sub.ref(0, 47475)); +axiom ($EXTERNS_BOTTOM == $add.ref($GLOBALS_BOTTOM, $sub.ref(0, 32768))); +axiom ($MALLOC_TOP == 9223372036854775807); +function {:define} $isExternal(p: ref) returns (bool) { $slt.ref.bool(p, $EXTERNS_BOTTOM) } + +// SMT bit-vector/integer conversion +function {:builtin "(_ int2bv 64)"} $int2bv.64(i: i64) returns (bv64); +function {:builtin "bv2nat"} $bv2int.64(i: bv64) returns (i64); + +// Integer arithmetic operations +function {:define} $add.i1(i1: i1, i2: i1) returns (i1) { (i1 + i2) } +function {:define} $add.i5(i1: i5, i2: i5) returns (i5) { (i1 + i2) } +function {:define} $add.i6(i1: i6, i2: i6) returns (i6) { (i1 + i2) } +function {:define} $add.i8(i1: i8, i2: i8) returns (i8) { (i1 + i2) } +function {:define} $add.i16(i1: i16, i2: i16) returns (i16) { (i1 + i2) } +function {:define} $add.i24(i1: i24, i2: i24) returns (i24) { (i1 + i2) } +function {:define} $add.i32(i1: i32, i2: i32) returns (i32) { (i1 + i2) } +function {:define} $add.i40(i1: i40, i2: i40) returns (i40) { (i1 + i2) } +function {:define} $add.i48(i1: i48, i2: i48) returns (i48) { (i1 + i2) } +function {:define} $add.i56(i1: i56, i2: i56) returns (i56) { (i1 + i2) } +function {:define} $add.i64(i1: i64, i2: i64) returns (i64) { (i1 + i2) } +function {:define} $add.i80(i1: i80, i2: i80) returns (i80) { (i1 + i2) } +function {:define} $add.i88(i1: i88, i2: i88) returns (i88) { (i1 + i2) } +function {:define} $add.i96(i1: i96, i2: i96) returns (i96) { (i1 + i2) } +function {:define} $add.i128(i1: i128, i2: i128) returns (i128) { (i1 + i2) } +function {:define} $add.i160(i1: i160, i2: i160) returns (i160) { (i1 + i2) } +function {:define} $add.i256(i1: i256, i2: i256) returns (i256) { (i1 + i2) } +function {:define} $sub.i1(i1: i1, i2: i1) returns (i1) { (i1 - i2) } +function {:define} $sub.i5(i1: i5, i2: i5) returns (i5) { (i1 - i2) } +function {:define} $sub.i6(i1: i6, i2: i6) returns (i6) { (i1 - i2) } +function {:define} $sub.i8(i1: i8, i2: i8) returns (i8) { (i1 - i2) } +function {:define} $sub.i16(i1: i16, i2: i16) returns (i16) { (i1 - i2) } +function {:define} $sub.i24(i1: i24, i2: i24) returns (i24) { (i1 - i2) } +function {:define} $sub.i32(i1: i32, i2: i32) returns (i32) { (i1 - i2) } +function {:define} $sub.i40(i1: i40, i2: i40) returns (i40) { (i1 - i2) } +function {:define} $sub.i48(i1: i48, i2: i48) returns (i48) { (i1 - i2) } +function {:define} $sub.i56(i1: i56, i2: i56) returns (i56) { (i1 - i2) } +function {:define} $sub.i64(i1: i64, i2: i64) returns (i64) { (i1 - i2) } +function {:define} $sub.i80(i1: i80, i2: i80) returns (i80) { (i1 - i2) } +function {:define} $sub.i88(i1: i88, i2: i88) returns (i88) { (i1 - i2) } +function {:define} $sub.i96(i1: i96, i2: i96) returns (i96) { (i1 - i2) } +function {:define} $sub.i128(i1: i128, i2: i128) returns (i128) { (i1 - i2) } +function {:define} $sub.i160(i1: i160, i2: i160) returns (i160) { (i1 - i2) } +function {:define} $sub.i256(i1: i256, i2: i256) returns (i256) { (i1 - i2) } +function {:define} $mul.i1(i1: i1, i2: i1) returns (i1) { (i1 * i2) } +function {:define} $mul.i5(i1: i5, i2: i5) returns (i5) { (i1 * i2) } +function {:define} $mul.i6(i1: i6, i2: i6) returns (i6) { (i1 * i2) } +function {:define} $mul.i8(i1: i8, i2: i8) returns (i8) { (i1 * i2) } +function {:define} $mul.i16(i1: i16, i2: i16) returns (i16) { (i1 * i2) } +function {:define} $mul.i24(i1: i24, i2: i24) returns (i24) { (i1 * i2) } +function {:define} $mul.i32(i1: i32, i2: i32) returns (i32) { (i1 * i2) } +function {:define} $mul.i40(i1: i40, i2: i40) returns (i40) { (i1 * i2) } +function {:define} $mul.i48(i1: i48, i2: i48) returns (i48) { (i1 * i2) } +function {:define} $mul.i56(i1: i56, i2: i56) returns (i56) { (i1 * i2) } +function {:define} $mul.i64(i1: i64, i2: i64) returns (i64) { (i1 * i2) } +function {:define} $mul.i80(i1: i80, i2: i80) returns (i80) { (i1 * i2) } +function {:define} $mul.i88(i1: i88, i2: i88) returns (i88) { (i1 * i2) } +function {:define} $mul.i96(i1: i96, i2: i96) returns (i96) { (i1 * i2) } +function {:define} $mul.i128(i1: i128, i2: i128) returns (i128) { (i1 * i2) } +function {:define} $mul.i160(i1: i160, i2: i160) returns (i160) { (i1 * i2) } +function {:define} $mul.i256(i1: i256, i2: i256) returns (i256) { (i1 * i2) } +function {:builtin "div"} $sdiv.i1(i1: i1, i2: i1) returns (i1); +function {:builtin "div"} $sdiv.i5(i1: i5, i2: i5) returns (i5); +function {:builtin "div"} $sdiv.i6(i1: i6, i2: i6) returns (i6); +function {:builtin "div"} $sdiv.i8(i1: i8, i2: i8) returns (i8); +function {:builtin "div"} $sdiv.i16(i1: i16, i2: i16) returns (i16); +function {:builtin "div"} $sdiv.i24(i1: i24, i2: i24) returns (i24); +function {:builtin "div"} $sdiv.i32(i1: i32, i2: i32) returns (i32); +function {:builtin "div"} $sdiv.i40(i1: i40, i2: i40) returns (i40); +function {:builtin "div"} $sdiv.i48(i1: i48, i2: i48) returns (i48); +function {:builtin "div"} $sdiv.i56(i1: i56, i2: i56) returns (i56); +function {:builtin "div"} $sdiv.i64(i1: i64, i2: i64) returns (i64); +function {:builtin "div"} $sdiv.i80(i1: i80, i2: i80) returns (i80); +function {:builtin "div"} $sdiv.i88(i1: i88, i2: i88) returns (i88); +function {:builtin "div"} $sdiv.i96(i1: i96, i2: i96) returns (i96); +function {:builtin "div"} $sdiv.i128(i1: i128, i2: i128) returns (i128); +function {:builtin "div"} $sdiv.i160(i1: i160, i2: i160) returns (i160); +function {:builtin "div"} $sdiv.i256(i1: i256, i2: i256) returns (i256); +function {:builtin "mod"} $smod.i1(i1: i1, i2: i1) returns (i1); +function {:builtin "mod"} $smod.i5(i1: i5, i2: i5) returns (i5); +function {:builtin "mod"} $smod.i6(i1: i6, i2: i6) returns (i6); +function {:builtin "mod"} $smod.i8(i1: i8, i2: i8) returns (i8); +function {:builtin "mod"} $smod.i16(i1: i16, i2: i16) returns (i16); +function {:builtin "mod"} $smod.i24(i1: i24, i2: i24) returns (i24); +function {:builtin "mod"} $smod.i32(i1: i32, i2: i32) returns (i32); +function {:builtin "mod"} $smod.i40(i1: i40, i2: i40) returns (i40); +function {:builtin "mod"} $smod.i48(i1: i48, i2: i48) returns (i48); +function {:builtin "mod"} $smod.i56(i1: i56, i2: i56) returns (i56); +function {:builtin "mod"} $smod.i64(i1: i64, i2: i64) returns (i64); +function {:builtin "mod"} $smod.i80(i1: i80, i2: i80) returns (i80); +function {:builtin "mod"} $smod.i88(i1: i88, i2: i88) returns (i88); +function {:builtin "mod"} $smod.i96(i1: i96, i2: i96) returns (i96); +function {:builtin "mod"} $smod.i128(i1: i128, i2: i128) returns (i128); +function {:builtin "mod"} $smod.i160(i1: i160, i2: i160) returns (i160); +function {:builtin "mod"} $smod.i256(i1: i256, i2: i256) returns (i256); +function {:builtin "div"} $udiv.i1(i1: i1, i2: i1) returns (i1); +function {:builtin "div"} $udiv.i5(i1: i5, i2: i5) returns (i5); +function {:builtin "div"} $udiv.i6(i1: i6, i2: i6) returns (i6); +function {:builtin "div"} $udiv.i8(i1: i8, i2: i8) returns (i8); +function {:builtin "div"} $udiv.i16(i1: i16, i2: i16) returns (i16); +function {:builtin "div"} $udiv.i24(i1: i24, i2: i24) returns (i24); +function {:builtin "div"} $udiv.i32(i1: i32, i2: i32) returns (i32); +function {:builtin "div"} $udiv.i40(i1: i40, i2: i40) returns (i40); +function {:builtin "div"} $udiv.i48(i1: i48, i2: i48) returns (i48); +function {:builtin "div"} $udiv.i56(i1: i56, i2: i56) returns (i56); +function {:builtin "div"} $udiv.i64(i1: i64, i2: i64) returns (i64); +function {:builtin "div"} $udiv.i80(i1: i80, i2: i80) returns (i80); +function {:builtin "div"} $udiv.i88(i1: i88, i2: i88) returns (i88); +function {:builtin "div"} $udiv.i96(i1: i96, i2: i96) returns (i96); +function {:builtin "div"} $udiv.i128(i1: i128, i2: i128) returns (i128); +function {:builtin "div"} $udiv.i160(i1: i160, i2: i160) returns (i160); +function {:builtin "div"} $udiv.i256(i1: i256, i2: i256) returns (i256); +function {:define} $srem.i1(i1: i1, i2: i1) returns (i1) { (if ($ne.i1.bool($smod.i1(i1, i2), 0) && $slt.i1.bool(i1, 0)) then $sub.i1($smod.i1(i1, i2), $smax.i1(i2, $sub.i1(0, i2))) else $smod.i1(i1, i2)) } +function {:define} $srem.i5(i1: i5, i2: i5) returns (i5) { (if ($ne.i5.bool($smod.i5(i1, i2), 0) && $slt.i5.bool(i1, 0)) then $sub.i5($smod.i5(i1, i2), $smax.i5(i2, $sub.i5(0, i2))) else $smod.i5(i1, i2)) } +function {:define} $srem.i6(i1: i6, i2: i6) returns (i6) { (if ($ne.i6.bool($smod.i6(i1, i2), 0) && $slt.i6.bool(i1, 0)) then $sub.i6($smod.i6(i1, i2), $smax.i6(i2, $sub.i6(0, i2))) else $smod.i6(i1, i2)) } +function {:define} $srem.i8(i1: i8, i2: i8) returns (i8) { (if ($ne.i8.bool($smod.i8(i1, i2), 0) && $slt.i8.bool(i1, 0)) then $sub.i8($smod.i8(i1, i2), $smax.i8(i2, $sub.i8(0, i2))) else $smod.i8(i1, i2)) } +function {:define} $srem.i16(i1: i16, i2: i16) returns (i16) { (if ($ne.i16.bool($smod.i16(i1, i2), 0) && $slt.i16.bool(i1, 0)) then $sub.i16($smod.i16(i1, i2), $smax.i16(i2, $sub.i16(0, i2))) else $smod.i16(i1, i2)) } +function {:define} $srem.i24(i1: i24, i2: i24) returns (i24) { (if ($ne.i24.bool($smod.i24(i1, i2), 0) && $slt.i24.bool(i1, 0)) then $sub.i24($smod.i24(i1, i2), $smax.i24(i2, $sub.i24(0, i2))) else $smod.i24(i1, i2)) } +function {:define} $srem.i32(i1: i32, i2: i32) returns (i32) { (if ($ne.i32.bool($smod.i32(i1, i2), 0) && $slt.i32.bool(i1, 0)) then $sub.i32($smod.i32(i1, i2), $smax.i32(i2, $sub.i32(0, i2))) else $smod.i32(i1, i2)) } +function {:define} $srem.i40(i1: i40, i2: i40) returns (i40) { (if ($ne.i40.bool($smod.i40(i1, i2), 0) && $slt.i40.bool(i1, 0)) then $sub.i40($smod.i40(i1, i2), $smax.i40(i2, $sub.i40(0, i2))) else $smod.i40(i1, i2)) } +function {:define} $srem.i48(i1: i48, i2: i48) returns (i48) { (if ($ne.i48.bool($smod.i48(i1, i2), 0) && $slt.i48.bool(i1, 0)) then $sub.i48($smod.i48(i1, i2), $smax.i48(i2, $sub.i48(0, i2))) else $smod.i48(i1, i2)) } +function {:define} $srem.i56(i1: i56, i2: i56) returns (i56) { (if ($ne.i56.bool($smod.i56(i1, i2), 0) && $slt.i56.bool(i1, 0)) then $sub.i56($smod.i56(i1, i2), $smax.i56(i2, $sub.i56(0, i2))) else $smod.i56(i1, i2)) } +function {:define} $srem.i64(i1: i64, i2: i64) returns (i64) { (if ($ne.i64.bool($smod.i64(i1, i2), 0) && $slt.i64.bool(i1, 0)) then $sub.i64($smod.i64(i1, i2), $smax.i64(i2, $sub.i64(0, i2))) else $smod.i64(i1, i2)) } +function {:define} $srem.i80(i1: i80, i2: i80) returns (i80) { (if ($ne.i80.bool($smod.i80(i1, i2), 0) && $slt.i80.bool(i1, 0)) then $sub.i80($smod.i80(i1, i2), $smax.i80(i2, $sub.i80(0, i2))) else $smod.i80(i1, i2)) } +function {:define} $srem.i88(i1: i88, i2: i88) returns (i88) { (if ($ne.i88.bool($smod.i88(i1, i2), 0) && $slt.i88.bool(i1, 0)) then $sub.i88($smod.i88(i1, i2), $smax.i88(i2, $sub.i88(0, i2))) else $smod.i88(i1, i2)) } +function {:define} $srem.i96(i1: i96, i2: i96) returns (i96) { (if ($ne.i96.bool($smod.i96(i1, i2), 0) && $slt.i96.bool(i1, 0)) then $sub.i96($smod.i96(i1, i2), $smax.i96(i2, $sub.i96(0, i2))) else $smod.i96(i1, i2)) } +function {:define} $srem.i128(i1: i128, i2: i128) returns (i128) { (if ($ne.i128.bool($smod.i128(i1, i2), 0) && $slt.i128.bool(i1, 0)) then $sub.i128($smod.i128(i1, i2), $smax.i128(i2, $sub.i128(0, i2))) else $smod.i128(i1, i2)) } +function {:define} $srem.i160(i1: i160, i2: i160) returns (i160) { (if ($ne.i160.bool($smod.i160(i1, i2), 0) && $slt.i160.bool(i1, 0)) then $sub.i160($smod.i160(i1, i2), $smax.i160(i2, $sub.i160(0, i2))) else $smod.i160(i1, i2)) } +function {:define} $srem.i256(i1: i256, i2: i256) returns (i256) { (if ($ne.i256.bool($smod.i256(i1, i2), 0) && $slt.i256.bool(i1, 0)) then $sub.i256($smod.i256(i1, i2), $smax.i256(i2, $sub.i256(0, i2))) else $smod.i256(i1, i2)) } +function {:define} $urem.i1(i1: i1, i2: i1) returns (i1) { $smod.i1(i1, i2) } +function {:define} $urem.i5(i1: i5, i2: i5) returns (i5) { $smod.i5(i1, i2) } +function {:define} $urem.i6(i1: i6, i2: i6) returns (i6) { $smod.i6(i1, i2) } +function {:define} $urem.i8(i1: i8, i2: i8) returns (i8) { $smod.i8(i1, i2) } +function {:define} $urem.i16(i1: i16, i2: i16) returns (i16) { $smod.i16(i1, i2) } +function {:define} $urem.i24(i1: i24, i2: i24) returns (i24) { $smod.i24(i1, i2) } +function {:define} $urem.i32(i1: i32, i2: i32) returns (i32) { $smod.i32(i1, i2) } +function {:define} $urem.i40(i1: i40, i2: i40) returns (i40) { $smod.i40(i1, i2) } +function {:define} $urem.i48(i1: i48, i2: i48) returns (i48) { $smod.i48(i1, i2) } +function {:define} $urem.i56(i1: i56, i2: i56) returns (i56) { $smod.i56(i1, i2) } +function {:define} $urem.i64(i1: i64, i2: i64) returns (i64) { $smod.i64(i1, i2) } +function {:define} $urem.i80(i1: i80, i2: i80) returns (i80) { $smod.i80(i1, i2) } +function {:define} $urem.i88(i1: i88, i2: i88) returns (i88) { $smod.i88(i1, i2) } +function {:define} $urem.i96(i1: i96, i2: i96) returns (i96) { $smod.i96(i1, i2) } +function {:define} $urem.i128(i1: i128, i2: i128) returns (i128) { $smod.i128(i1, i2) } +function {:define} $urem.i160(i1: i160, i2: i160) returns (i160) { $smod.i160(i1, i2) } +function {:define} $urem.i256(i1: i256, i2: i256) returns (i256) { $smod.i256(i1, i2) } +function $shl.i1(i1: i1, i2: i1) returns (i1); +function $shl.i5(i1: i5, i2: i5) returns (i5); +function $shl.i6(i1: i6, i2: i6) returns (i6); +function $shl.i8(i1: i8, i2: i8) returns (i8); +function $shl.i16(i1: i16, i2: i16) returns (i16); +function $shl.i24(i1: i24, i2: i24) returns (i24); +function $shl.i32(i1: i32, i2: i32) returns (i32); +function $shl.i40(i1: i40, i2: i40) returns (i40); +function $shl.i48(i1: i48, i2: i48) returns (i48); +function $shl.i56(i1: i56, i2: i56) returns (i56); +function $shl.i64(i1: i64, i2: i64) returns (i64); +function $shl.i80(i1: i80, i2: i80) returns (i80); +function $shl.i88(i1: i88, i2: i88) returns (i88); +function $shl.i96(i1: i96, i2: i96) returns (i96); +function $shl.i128(i1: i128, i2: i128) returns (i128); +function $shl.i160(i1: i160, i2: i160) returns (i160); +function $shl.i256(i1: i256, i2: i256) returns (i256); +function $lshr.i1(i1: i1, i2: i1) returns (i1); +function $lshr.i5(i1: i5, i2: i5) returns (i5); +function $lshr.i6(i1: i6, i2: i6) returns (i6); +function $lshr.i8(i1: i8, i2: i8) returns (i8); +function $lshr.i16(i1: i16, i2: i16) returns (i16); +function $lshr.i24(i1: i24, i2: i24) returns (i24); +function $lshr.i32(i1: i32, i2: i32) returns (i32); +function $lshr.i40(i1: i40, i2: i40) returns (i40); +function $lshr.i48(i1: i48, i2: i48) returns (i48); +function $lshr.i56(i1: i56, i2: i56) returns (i56); +function $lshr.i64(i1: i64, i2: i64) returns (i64); +function $lshr.i80(i1: i80, i2: i80) returns (i80); +function $lshr.i88(i1: i88, i2: i88) returns (i88); +function $lshr.i96(i1: i96, i2: i96) returns (i96); +function $lshr.i128(i1: i128, i2: i128) returns (i128); +function $lshr.i160(i1: i160, i2: i160) returns (i160); +function $lshr.i256(i1: i256, i2: i256) returns (i256); +function $ashr.i1(i1: i1, i2: i1) returns (i1); +function $ashr.i5(i1: i5, i2: i5) returns (i5); +function $ashr.i6(i1: i6, i2: i6) returns (i6); +function $ashr.i8(i1: i8, i2: i8) returns (i8); +function $ashr.i16(i1: i16, i2: i16) returns (i16); +function $ashr.i24(i1: i24, i2: i24) returns (i24); +function $ashr.i32(i1: i32, i2: i32) returns (i32); +function $ashr.i40(i1: i40, i2: i40) returns (i40); +function $ashr.i48(i1: i48, i2: i48) returns (i48); +function $ashr.i56(i1: i56, i2: i56) returns (i56); +function $ashr.i64(i1: i64, i2: i64) returns (i64); +function $ashr.i80(i1: i80, i2: i80) returns (i80); +function $ashr.i88(i1: i88, i2: i88) returns (i88); +function $ashr.i96(i1: i96, i2: i96) returns (i96); +function $ashr.i128(i1: i128, i2: i128) returns (i128); +function $ashr.i160(i1: i160, i2: i160) returns (i160); +function $ashr.i256(i1: i256, i2: i256) returns (i256); +function $and.i1(i1: i1, i2: i1) returns (i1); +function $and.i5(i1: i5, i2: i5) returns (i5); +function $and.i6(i1: i6, i2: i6) returns (i6); +function $and.i8(i1: i8, i2: i8) returns (i8); +function $and.i16(i1: i16, i2: i16) returns (i16); +function $and.i24(i1: i24, i2: i24) returns (i24); +function $and.i32(i1: i32, i2: i32) returns (i32); +function $and.i40(i1: i40, i2: i40) returns (i40); +function $and.i48(i1: i48, i2: i48) returns (i48); +function $and.i56(i1: i56, i2: i56) returns (i56); +function $and.i64(i1: i64, i2: i64) returns (i64); +function $and.i80(i1: i80, i2: i80) returns (i80); +function $and.i88(i1: i88, i2: i88) returns (i88); +function $and.i96(i1: i96, i2: i96) returns (i96); +function $and.i128(i1: i128, i2: i128) returns (i128); +function $and.i160(i1: i160, i2: i160) returns (i160); +function $and.i256(i1: i256, i2: i256) returns (i256); +function $or.i1(i1: i1, i2: i1) returns (i1); +function $or.i5(i1: i5, i2: i5) returns (i5); +function $or.i6(i1: i6, i2: i6) returns (i6); +function $or.i8(i1: i8, i2: i8) returns (i8); +function $or.i16(i1: i16, i2: i16) returns (i16); +function $or.i24(i1: i24, i2: i24) returns (i24); +function $or.i32(i1: i32, i2: i32) returns (i32); +function $or.i40(i1: i40, i2: i40) returns (i40); +function $or.i48(i1: i48, i2: i48) returns (i48); +function $or.i56(i1: i56, i2: i56) returns (i56); +function $or.i64(i1: i64, i2: i64) returns (i64); +function $or.i80(i1: i80, i2: i80) returns (i80); +function $or.i88(i1: i88, i2: i88) returns (i88); +function $or.i96(i1: i96, i2: i96) returns (i96); +function $or.i128(i1: i128, i2: i128) returns (i128); +function $or.i160(i1: i160, i2: i160) returns (i160); +function $or.i256(i1: i256, i2: i256) returns (i256); +function $xor.i1(i1: i1, i2: i1) returns (i1); +function $xor.i5(i1: i5, i2: i5) returns (i5); +function $xor.i6(i1: i6, i2: i6) returns (i6); +function $xor.i8(i1: i8, i2: i8) returns (i8); +function $xor.i16(i1: i16, i2: i16) returns (i16); +function $xor.i24(i1: i24, i2: i24) returns (i24); +function $xor.i32(i1: i32, i2: i32) returns (i32); +function $xor.i40(i1: i40, i2: i40) returns (i40); +function $xor.i48(i1: i48, i2: i48) returns (i48); +function $xor.i56(i1: i56, i2: i56) returns (i56); +function $xor.i64(i1: i64, i2: i64) returns (i64); +function $xor.i80(i1: i80, i2: i80) returns (i80); +function $xor.i88(i1: i88, i2: i88) returns (i88); +function $xor.i96(i1: i96, i2: i96) returns (i96); +function $xor.i128(i1: i128, i2: i128) returns (i128); +function $xor.i160(i1: i160, i2: i160) returns (i160); +function $xor.i256(i1: i256, i2: i256) returns (i256); +function $nand.i1(i1: i1, i2: i1) returns (i1); +function $nand.i5(i1: i5, i2: i5) returns (i5); +function $nand.i6(i1: i6, i2: i6) returns (i6); +function $nand.i8(i1: i8, i2: i8) returns (i8); +function $nand.i16(i1: i16, i2: i16) returns (i16); +function $nand.i24(i1: i24, i2: i24) returns (i24); +function $nand.i32(i1: i32, i2: i32) returns (i32); +function $nand.i40(i1: i40, i2: i40) returns (i40); +function $nand.i48(i1: i48, i2: i48) returns (i48); +function $nand.i56(i1: i56, i2: i56) returns (i56); +function $nand.i64(i1: i64, i2: i64) returns (i64); +function $nand.i80(i1: i80, i2: i80) returns (i80); +function $nand.i88(i1: i88, i2: i88) returns (i88); +function $nand.i96(i1: i96, i2: i96) returns (i96); +function $nand.i128(i1: i128, i2: i128) returns (i128); +function $nand.i160(i1: i160, i2: i160) returns (i160); +function $nand.i256(i1: i256, i2: i256) returns (i256); +function $not.i1(i: i1) returns (i1); +function $not.i5(i: i5) returns (i5); +function $not.i6(i: i6) returns (i6); +function $not.i8(i: i8) returns (i8); +function $not.i16(i: i16) returns (i16); +function $not.i24(i: i24) returns (i24); +function $not.i32(i: i32) returns (i32); +function $not.i40(i: i40) returns (i40); +function $not.i48(i: i48) returns (i48); +function $not.i56(i: i56) returns (i56); +function $not.i64(i: i64) returns (i64); +function $not.i80(i: i80) returns (i80); +function $not.i88(i: i88) returns (i88); +function $not.i96(i: i96) returns (i96); +function $not.i128(i: i128) returns (i128); +function $not.i160(i: i160) returns (i160); +function $not.i256(i: i256) returns (i256); +function {:define} $smin.i1(i1: i1, i2: i1) returns (i1) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i5(i1: i5, i2: i5) returns (i5) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i6(i1: i6, i2: i6) returns (i6) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i8(i1: i8, i2: i8) returns (i8) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i16(i1: i16, i2: i16) returns (i16) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i24(i1: i24, i2: i24) returns (i24) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i32(i1: i32, i2: i32) returns (i32) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i40(i1: i40, i2: i40) returns (i40) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i48(i1: i48, i2: i48) returns (i48) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i56(i1: i56, i2: i56) returns (i56) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i64(i1: i64, i2: i64) returns (i64) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i80(i1: i80, i2: i80) returns (i80) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i88(i1: i88, i2: i88) returns (i88) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i96(i1: i96, i2: i96) returns (i96) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i128(i1: i128, i2: i128) returns (i128) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i160(i1: i160, i2: i160) returns (i160) { (if (i1 < i2) then i1 else i2) } +function {:define} $smin.i256(i1: i256, i2: i256) returns (i256) { (if (i1 < i2) then i1 else i2) } +function {:define} $smax.i1(i1: i1, i2: i1) returns (i1) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i5(i1: i5, i2: i5) returns (i5) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i6(i1: i6, i2: i6) returns (i6) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i8(i1: i8, i2: i8) returns (i8) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i16(i1: i16, i2: i16) returns (i16) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i24(i1: i24, i2: i24) returns (i24) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i32(i1: i32, i2: i32) returns (i32) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i40(i1: i40, i2: i40) returns (i40) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i48(i1: i48, i2: i48) returns (i48) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i56(i1: i56, i2: i56) returns (i56) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i64(i1: i64, i2: i64) returns (i64) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i80(i1: i80, i2: i80) returns (i80) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i88(i1: i88, i2: i88) returns (i88) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i96(i1: i96, i2: i96) returns (i96) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i128(i1: i128, i2: i128) returns (i128) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i160(i1: i160, i2: i160) returns (i160) { (if (i2 < i1) then i1 else i2) } +function {:define} $smax.i256(i1: i256, i2: i256) returns (i256) { (if (i2 < i1) then i1 else i2) } +function {:define} $umin.i1(i1: i1, i2: i1) returns (i1) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i5(i1: i5, i2: i5) returns (i5) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i6(i1: i6, i2: i6) returns (i6) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i8(i1: i8, i2: i8) returns (i8) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i16(i1: i16, i2: i16) returns (i16) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i24(i1: i24, i2: i24) returns (i24) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i32(i1: i32, i2: i32) returns (i32) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i40(i1: i40, i2: i40) returns (i40) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i48(i1: i48, i2: i48) returns (i48) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i56(i1: i56, i2: i56) returns (i56) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i64(i1: i64, i2: i64) returns (i64) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i80(i1: i80, i2: i80) returns (i80) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i88(i1: i88, i2: i88) returns (i88) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i96(i1: i96, i2: i96) returns (i96) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i128(i1: i128, i2: i128) returns (i128) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i160(i1: i160, i2: i160) returns (i160) { (if (i1 < i2) then i1 else i2) } +function {:define} $umin.i256(i1: i256, i2: i256) returns (i256) { (if (i1 < i2) then i1 else i2) } +function {:define} $umax.i1(i1: i1, i2: i1) returns (i1) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i5(i1: i5, i2: i5) returns (i5) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i6(i1: i6, i2: i6) returns (i6) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i8(i1: i8, i2: i8) returns (i8) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i16(i1: i16, i2: i16) returns (i16) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i24(i1: i24, i2: i24) returns (i24) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i32(i1: i32, i2: i32) returns (i32) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i40(i1: i40, i2: i40) returns (i40) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i48(i1: i48, i2: i48) returns (i48) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i56(i1: i56, i2: i56) returns (i56) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i64(i1: i64, i2: i64) returns (i64) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i80(i1: i80, i2: i80) returns (i80) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i88(i1: i88, i2: i88) returns (i88) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i96(i1: i96, i2: i96) returns (i96) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i128(i1: i128, i2: i128) returns (i128) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i160(i1: i160, i2: i160) returns (i160) { (if (i2 < i1) then i1 else i2) } +function {:define} $umax.i256(i1: i256, i2: i256) returns (i256) { (if (i2 < i1) then i1 else i2) } +axiom ($and.i1(0, 0) == 0); +axiom ($or.i1(0, 0) == 0); +axiom ($xor.i1(0, 0) == 0); +axiom ($and.i1(0, 1) == 0); +axiom ($or.i1(0, 1) == 1); +axiom ($xor.i1(0, 1) == 1); +axiom ($and.i1(1, 0) == 0); +axiom ($or.i1(1, 0) == 1); +axiom ($xor.i1(1, 0) == 1); +axiom ($and.i1(1, 1) == 1); +axiom ($or.i1(1, 1) == 1); +axiom ($xor.i1(1, 1) == 0); +axiom ($and.i32(32, 16) == 0); +// Integer predicates +function {:define} $ule.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 <= i2) } +function {:define} $ule.i1(i1: i1, i2: i1) returns (i1) { (if $ule.i1.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 <= i2) } +function {:define} $ule.i5(i1: i5, i2: i5) returns (i1) { (if $ule.i5.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 <= i2) } +function {:define} $ule.i6(i1: i6, i2: i6) returns (i1) { (if $ule.i6.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 <= i2) } +function {:define} $ule.i8(i1: i8, i2: i8) returns (i1) { (if $ule.i8.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 <= i2) } +function {:define} $ule.i16(i1: i16, i2: i16) returns (i1) { (if $ule.i16.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 <= i2) } +function {:define} $ule.i24(i1: i24, i2: i24) returns (i1) { (if $ule.i24.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 <= i2) } +function {:define} $ule.i32(i1: i32, i2: i32) returns (i1) { (if $ule.i32.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 <= i2) } +function {:define} $ule.i40(i1: i40, i2: i40) returns (i1) { (if $ule.i40.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 <= i2) } +function {:define} $ule.i48(i1: i48, i2: i48) returns (i1) { (if $ule.i48.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 <= i2) } +function {:define} $ule.i56(i1: i56, i2: i56) returns (i1) { (if $ule.i56.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 <= i2) } +function {:define} $ule.i64(i1: i64, i2: i64) returns (i1) { (if $ule.i64.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 <= i2) } +function {:define} $ule.i80(i1: i80, i2: i80) returns (i1) { (if $ule.i80.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 <= i2) } +function {:define} $ule.i88(i1: i88, i2: i88) returns (i1) { (if $ule.i88.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 <= i2) } +function {:define} $ule.i96(i1: i96, i2: i96) returns (i1) { (if $ule.i96.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 <= i2) } +function {:define} $ule.i128(i1: i128, i2: i128) returns (i1) { (if $ule.i128.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 <= i2) } +function {:define} $ule.i160(i1: i160, i2: i160) returns (i1) { (if $ule.i160.bool(i1, i2) then 1 else 0) } +function {:define} $ule.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 <= i2) } +function {:define} $ule.i256(i1: i256, i2: i256) returns (i1) { (if $ule.i256.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 < i2) } +function {:define} $ult.i1(i1: i1, i2: i1) returns (i1) { (if $ult.i1.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 < i2) } +function {:define} $ult.i5(i1: i5, i2: i5) returns (i1) { (if $ult.i5.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 < i2) } +function {:define} $ult.i6(i1: i6, i2: i6) returns (i1) { (if $ult.i6.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 < i2) } +function {:define} $ult.i8(i1: i8, i2: i8) returns (i1) { (if $ult.i8.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 < i2) } +function {:define} $ult.i16(i1: i16, i2: i16) returns (i1) { (if $ult.i16.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 < i2) } +function {:define} $ult.i24(i1: i24, i2: i24) returns (i1) { (if $ult.i24.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 < i2) } +function {:define} $ult.i32(i1: i32, i2: i32) returns (i1) { (if $ult.i32.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 < i2) } +function {:define} $ult.i40(i1: i40, i2: i40) returns (i1) { (if $ult.i40.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 < i2) } +function {:define} $ult.i48(i1: i48, i2: i48) returns (i1) { (if $ult.i48.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 < i2) } +function {:define} $ult.i56(i1: i56, i2: i56) returns (i1) { (if $ult.i56.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 < i2) } +function {:define} $ult.i64(i1: i64, i2: i64) returns (i1) { (if $ult.i64.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 < i2) } +function {:define} $ult.i80(i1: i80, i2: i80) returns (i1) { (if $ult.i80.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 < i2) } +function {:define} $ult.i88(i1: i88, i2: i88) returns (i1) { (if $ult.i88.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 < i2) } +function {:define} $ult.i96(i1: i96, i2: i96) returns (i1) { (if $ult.i96.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 < i2) } +function {:define} $ult.i128(i1: i128, i2: i128) returns (i1) { (if $ult.i128.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 < i2) } +function {:define} $ult.i160(i1: i160, i2: i160) returns (i1) { (if $ult.i160.bool(i1, i2) then 1 else 0) } +function {:define} $ult.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 < i2) } +function {:define} $ult.i256(i1: i256, i2: i256) returns (i1) { (if $ult.i256.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 >= i2) } +function {:define} $uge.i1(i1: i1, i2: i1) returns (i1) { (if $uge.i1.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 >= i2) } +function {:define} $uge.i5(i1: i5, i2: i5) returns (i1) { (if $uge.i5.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 >= i2) } +function {:define} $uge.i6(i1: i6, i2: i6) returns (i1) { (if $uge.i6.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 >= i2) } +function {:define} $uge.i8(i1: i8, i2: i8) returns (i1) { (if $uge.i8.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 >= i2) } +function {:define} $uge.i16(i1: i16, i2: i16) returns (i1) { (if $uge.i16.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 >= i2) } +function {:define} $uge.i24(i1: i24, i2: i24) returns (i1) { (if $uge.i24.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 >= i2) } +function {:define} $uge.i32(i1: i32, i2: i32) returns (i1) { (if $uge.i32.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 >= i2) } +function {:define} $uge.i40(i1: i40, i2: i40) returns (i1) { (if $uge.i40.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 >= i2) } +function {:define} $uge.i48(i1: i48, i2: i48) returns (i1) { (if $uge.i48.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 >= i2) } +function {:define} $uge.i56(i1: i56, i2: i56) returns (i1) { (if $uge.i56.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 >= i2) } +function {:define} $uge.i64(i1: i64, i2: i64) returns (i1) { (if $uge.i64.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 >= i2) } +function {:define} $uge.i80(i1: i80, i2: i80) returns (i1) { (if $uge.i80.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 >= i2) } +function {:define} $uge.i88(i1: i88, i2: i88) returns (i1) { (if $uge.i88.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 >= i2) } +function {:define} $uge.i96(i1: i96, i2: i96) returns (i1) { (if $uge.i96.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 >= i2) } +function {:define} $uge.i128(i1: i128, i2: i128) returns (i1) { (if $uge.i128.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 >= i2) } +function {:define} $uge.i160(i1: i160, i2: i160) returns (i1) { (if $uge.i160.bool(i1, i2) then 1 else 0) } +function {:define} $uge.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 >= i2) } +function {:define} $uge.i256(i1: i256, i2: i256) returns (i1) { (if $uge.i256.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 > i2) } +function {:define} $ugt.i1(i1: i1, i2: i1) returns (i1) { (if $ugt.i1.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 > i2) } +function {:define} $ugt.i5(i1: i5, i2: i5) returns (i1) { (if $ugt.i5.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 > i2) } +function {:define} $ugt.i6(i1: i6, i2: i6) returns (i1) { (if $ugt.i6.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 > i2) } +function {:define} $ugt.i8(i1: i8, i2: i8) returns (i1) { (if $ugt.i8.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 > i2) } +function {:define} $ugt.i16(i1: i16, i2: i16) returns (i1) { (if $ugt.i16.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 > i2) } +function {:define} $ugt.i24(i1: i24, i2: i24) returns (i1) { (if $ugt.i24.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 > i2) } +function {:define} $ugt.i32(i1: i32, i2: i32) returns (i1) { (if $ugt.i32.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 > i2) } +function {:define} $ugt.i40(i1: i40, i2: i40) returns (i1) { (if $ugt.i40.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 > i2) } +function {:define} $ugt.i48(i1: i48, i2: i48) returns (i1) { (if $ugt.i48.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 > i2) } +function {:define} $ugt.i56(i1: i56, i2: i56) returns (i1) { (if $ugt.i56.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 > i2) } +function {:define} $ugt.i64(i1: i64, i2: i64) returns (i1) { (if $ugt.i64.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 > i2) } +function {:define} $ugt.i80(i1: i80, i2: i80) returns (i1) { (if $ugt.i80.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 > i2) } +function {:define} $ugt.i88(i1: i88, i2: i88) returns (i1) { (if $ugt.i88.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 > i2) } +function {:define} $ugt.i96(i1: i96, i2: i96) returns (i1) { (if $ugt.i96.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 > i2) } +function {:define} $ugt.i128(i1: i128, i2: i128) returns (i1) { (if $ugt.i128.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 > i2) } +function {:define} $ugt.i160(i1: i160, i2: i160) returns (i1) { (if $ugt.i160.bool(i1, i2) then 1 else 0) } +function {:define} $ugt.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 > i2) } +function {:define} $ugt.i256(i1: i256, i2: i256) returns (i1) { (if $ugt.i256.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 <= i2) } +function {:define} $sle.i1(i1: i1, i2: i1) returns (i1) { (if $sle.i1.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 <= i2) } +function {:define} $sle.i5(i1: i5, i2: i5) returns (i1) { (if $sle.i5.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 <= i2) } +function {:define} $sle.i6(i1: i6, i2: i6) returns (i1) { (if $sle.i6.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 <= i2) } +function {:define} $sle.i8(i1: i8, i2: i8) returns (i1) { (if $sle.i8.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 <= i2) } +function {:define} $sle.i16(i1: i16, i2: i16) returns (i1) { (if $sle.i16.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 <= i2) } +function {:define} $sle.i24(i1: i24, i2: i24) returns (i1) { (if $sle.i24.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 <= i2) } +function {:define} $sle.i32(i1: i32, i2: i32) returns (i1) { (if $sle.i32.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 <= i2) } +function {:define} $sle.i40(i1: i40, i2: i40) returns (i1) { (if $sle.i40.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 <= i2) } +function {:define} $sle.i48(i1: i48, i2: i48) returns (i1) { (if $sle.i48.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 <= i2) } +function {:define} $sle.i56(i1: i56, i2: i56) returns (i1) { (if $sle.i56.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 <= i2) } +function {:define} $sle.i64(i1: i64, i2: i64) returns (i1) { (if $sle.i64.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 <= i2) } +function {:define} $sle.i80(i1: i80, i2: i80) returns (i1) { (if $sle.i80.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 <= i2) } +function {:define} $sle.i88(i1: i88, i2: i88) returns (i1) { (if $sle.i88.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 <= i2) } +function {:define} $sle.i96(i1: i96, i2: i96) returns (i1) { (if $sle.i96.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 <= i2) } +function {:define} $sle.i128(i1: i128, i2: i128) returns (i1) { (if $sle.i128.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 <= i2) } +function {:define} $sle.i160(i1: i160, i2: i160) returns (i1) { (if $sle.i160.bool(i1, i2) then 1 else 0) } +function {:define} $sle.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 <= i2) } +function {:define} $sle.i256(i1: i256, i2: i256) returns (i1) { (if $sle.i256.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 < i2) } +function {:define} $slt.i1(i1: i1, i2: i1) returns (i1) { (if $slt.i1.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 < i2) } +function {:define} $slt.i5(i1: i5, i2: i5) returns (i1) { (if $slt.i5.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 < i2) } +function {:define} $slt.i6(i1: i6, i2: i6) returns (i1) { (if $slt.i6.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 < i2) } +function {:define} $slt.i8(i1: i8, i2: i8) returns (i1) { (if $slt.i8.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 < i2) } +function {:define} $slt.i16(i1: i16, i2: i16) returns (i1) { (if $slt.i16.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 < i2) } +function {:define} $slt.i24(i1: i24, i2: i24) returns (i1) { (if $slt.i24.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 < i2) } +function {:define} $slt.i32(i1: i32, i2: i32) returns (i1) { (if $slt.i32.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 < i2) } +function {:define} $slt.i40(i1: i40, i2: i40) returns (i1) { (if $slt.i40.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 < i2) } +function {:define} $slt.i48(i1: i48, i2: i48) returns (i1) { (if $slt.i48.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 < i2) } +function {:define} $slt.i56(i1: i56, i2: i56) returns (i1) { (if $slt.i56.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 < i2) } +function {:define} $slt.i64(i1: i64, i2: i64) returns (i1) { (if $slt.i64.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 < i2) } +function {:define} $slt.i80(i1: i80, i2: i80) returns (i1) { (if $slt.i80.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 < i2) } +function {:define} $slt.i88(i1: i88, i2: i88) returns (i1) { (if $slt.i88.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 < i2) } +function {:define} $slt.i96(i1: i96, i2: i96) returns (i1) { (if $slt.i96.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 < i2) } +function {:define} $slt.i128(i1: i128, i2: i128) returns (i1) { (if $slt.i128.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 < i2) } +function {:define} $slt.i160(i1: i160, i2: i160) returns (i1) { (if $slt.i160.bool(i1, i2) then 1 else 0) } +function {:define} $slt.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 < i2) } +function {:define} $slt.i256(i1: i256, i2: i256) returns (i1) { (if $slt.i256.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 >= i2) } +function {:define} $sge.i1(i1: i1, i2: i1) returns (i1) { (if $sge.i1.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 >= i2) } +function {:define} $sge.i5(i1: i5, i2: i5) returns (i1) { (if $sge.i5.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 >= i2) } +function {:define} $sge.i6(i1: i6, i2: i6) returns (i1) { (if $sge.i6.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 >= i2) } +function {:define} $sge.i8(i1: i8, i2: i8) returns (i1) { (if $sge.i8.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 >= i2) } +function {:define} $sge.i16(i1: i16, i2: i16) returns (i1) { (if $sge.i16.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 >= i2) } +function {:define} $sge.i24(i1: i24, i2: i24) returns (i1) { (if $sge.i24.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 >= i2) } +function {:define} $sge.i32(i1: i32, i2: i32) returns (i1) { (if $sge.i32.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 >= i2) } +function {:define} $sge.i40(i1: i40, i2: i40) returns (i1) { (if $sge.i40.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 >= i2) } +function {:define} $sge.i48(i1: i48, i2: i48) returns (i1) { (if $sge.i48.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 >= i2) } +function {:define} $sge.i56(i1: i56, i2: i56) returns (i1) { (if $sge.i56.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 >= i2) } +function {:define} $sge.i64(i1: i64, i2: i64) returns (i1) { (if $sge.i64.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 >= i2) } +function {:define} $sge.i80(i1: i80, i2: i80) returns (i1) { (if $sge.i80.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 >= i2) } +function {:define} $sge.i88(i1: i88, i2: i88) returns (i1) { (if $sge.i88.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 >= i2) } +function {:define} $sge.i96(i1: i96, i2: i96) returns (i1) { (if $sge.i96.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 >= i2) } +function {:define} $sge.i128(i1: i128, i2: i128) returns (i1) { (if $sge.i128.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 >= i2) } +function {:define} $sge.i160(i1: i160, i2: i160) returns (i1) { (if $sge.i160.bool(i1, i2) then 1 else 0) } +function {:define} $sge.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 >= i2) } +function {:define} $sge.i256(i1: i256, i2: i256) returns (i1) { (if $sge.i256.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 > i2) } +function {:define} $sgt.i1(i1: i1, i2: i1) returns (i1) { (if $sgt.i1.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 > i2) } +function {:define} $sgt.i5(i1: i5, i2: i5) returns (i1) { (if $sgt.i5.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 > i2) } +function {:define} $sgt.i6(i1: i6, i2: i6) returns (i1) { (if $sgt.i6.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 > i2) } +function {:define} $sgt.i8(i1: i8, i2: i8) returns (i1) { (if $sgt.i8.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 > i2) } +function {:define} $sgt.i16(i1: i16, i2: i16) returns (i1) { (if $sgt.i16.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 > i2) } +function {:define} $sgt.i24(i1: i24, i2: i24) returns (i1) { (if $sgt.i24.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 > i2) } +function {:define} $sgt.i32(i1: i32, i2: i32) returns (i1) { (if $sgt.i32.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 > i2) } +function {:define} $sgt.i40(i1: i40, i2: i40) returns (i1) { (if $sgt.i40.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 > i2) } +function {:define} $sgt.i48(i1: i48, i2: i48) returns (i1) { (if $sgt.i48.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 > i2) } +function {:define} $sgt.i56(i1: i56, i2: i56) returns (i1) { (if $sgt.i56.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 > i2) } +function {:define} $sgt.i64(i1: i64, i2: i64) returns (i1) { (if $sgt.i64.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 > i2) } +function {:define} $sgt.i80(i1: i80, i2: i80) returns (i1) { (if $sgt.i80.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 > i2) } +function {:define} $sgt.i88(i1: i88, i2: i88) returns (i1) { (if $sgt.i88.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 > i2) } +function {:define} $sgt.i96(i1: i96, i2: i96) returns (i1) { (if $sgt.i96.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 > i2) } +function {:define} $sgt.i128(i1: i128, i2: i128) returns (i1) { (if $sgt.i128.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 > i2) } +function {:define} $sgt.i160(i1: i160, i2: i160) returns (i1) { (if $sgt.i160.bool(i1, i2) then 1 else 0) } +function {:define} $sgt.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 > i2) } +function {:define} $sgt.i256(i1: i256, i2: i256) returns (i1) { (if $sgt.i256.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 == i2) } +function {:define} $eq.i1(i1: i1, i2: i1) returns (i1) { (if $eq.i1.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 == i2) } +function {:define} $eq.i5(i1: i5, i2: i5) returns (i1) { (if $eq.i5.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 == i2) } +function {:define} $eq.i6(i1: i6, i2: i6) returns (i1) { (if $eq.i6.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 == i2) } +function {:define} $eq.i8(i1: i8, i2: i8) returns (i1) { (if $eq.i8.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 == i2) } +function {:define} $eq.i16(i1: i16, i2: i16) returns (i1) { (if $eq.i16.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 == i2) } +function {:define} $eq.i24(i1: i24, i2: i24) returns (i1) { (if $eq.i24.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 == i2) } +function {:define} $eq.i32(i1: i32, i2: i32) returns (i1) { (if $eq.i32.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 == i2) } +function {:define} $eq.i40(i1: i40, i2: i40) returns (i1) { (if $eq.i40.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 == i2) } +function {:define} $eq.i48(i1: i48, i2: i48) returns (i1) { (if $eq.i48.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 == i2) } +function {:define} $eq.i56(i1: i56, i2: i56) returns (i1) { (if $eq.i56.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 == i2) } +function {:define} $eq.i64(i1: i64, i2: i64) returns (i1) { (if $eq.i64.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 == i2) } +function {:define} $eq.i80(i1: i80, i2: i80) returns (i1) { (if $eq.i80.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 == i2) } +function {:define} $eq.i88(i1: i88, i2: i88) returns (i1) { (if $eq.i88.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 == i2) } +function {:define} $eq.i96(i1: i96, i2: i96) returns (i1) { (if $eq.i96.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 == i2) } +function {:define} $eq.i128(i1: i128, i2: i128) returns (i1) { (if $eq.i128.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 == i2) } +function {:define} $eq.i160(i1: i160, i2: i160) returns (i1) { (if $eq.i160.bool(i1, i2) then 1 else 0) } +function {:define} $eq.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 == i2) } +function {:define} $eq.i256(i1: i256, i2: i256) returns (i1) { (if $eq.i256.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i1.bool(i1: i1, i2: i1) returns (bool) { (i1 != i2) } +function {:define} $ne.i1(i1: i1, i2: i1) returns (i1) { (if $ne.i1.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i5.bool(i1: i5, i2: i5) returns (bool) { (i1 != i2) } +function {:define} $ne.i5(i1: i5, i2: i5) returns (i1) { (if $ne.i5.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i6.bool(i1: i6, i2: i6) returns (bool) { (i1 != i2) } +function {:define} $ne.i6(i1: i6, i2: i6) returns (i1) { (if $ne.i6.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i8.bool(i1: i8, i2: i8) returns (bool) { (i1 != i2) } +function {:define} $ne.i8(i1: i8, i2: i8) returns (i1) { (if $ne.i8.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i16.bool(i1: i16, i2: i16) returns (bool) { (i1 != i2) } +function {:define} $ne.i16(i1: i16, i2: i16) returns (i1) { (if $ne.i16.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i24.bool(i1: i24, i2: i24) returns (bool) { (i1 != i2) } +function {:define} $ne.i24(i1: i24, i2: i24) returns (i1) { (if $ne.i24.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i32.bool(i1: i32, i2: i32) returns (bool) { (i1 != i2) } +function {:define} $ne.i32(i1: i32, i2: i32) returns (i1) { (if $ne.i32.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i40.bool(i1: i40, i2: i40) returns (bool) { (i1 != i2) } +function {:define} $ne.i40(i1: i40, i2: i40) returns (i1) { (if $ne.i40.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i48.bool(i1: i48, i2: i48) returns (bool) { (i1 != i2) } +function {:define} $ne.i48(i1: i48, i2: i48) returns (i1) { (if $ne.i48.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i56.bool(i1: i56, i2: i56) returns (bool) { (i1 != i2) } +function {:define} $ne.i56(i1: i56, i2: i56) returns (i1) { (if $ne.i56.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i64.bool(i1: i64, i2: i64) returns (bool) { (i1 != i2) } +function {:define} $ne.i64(i1: i64, i2: i64) returns (i1) { (if $ne.i64.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i80.bool(i1: i80, i2: i80) returns (bool) { (i1 != i2) } +function {:define} $ne.i80(i1: i80, i2: i80) returns (i1) { (if $ne.i80.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i88.bool(i1: i88, i2: i88) returns (bool) { (i1 != i2) } +function {:define} $ne.i88(i1: i88, i2: i88) returns (i1) { (if $ne.i88.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i96.bool(i1: i96, i2: i96) returns (bool) { (i1 != i2) } +function {:define} $ne.i96(i1: i96, i2: i96) returns (i1) { (if $ne.i96.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i128.bool(i1: i128, i2: i128) returns (bool) { (i1 != i2) } +function {:define} $ne.i128(i1: i128, i2: i128) returns (i1) { (if $ne.i128.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i160.bool(i1: i160, i2: i160) returns (bool) { (i1 != i2) } +function {:define} $ne.i160(i1: i160, i2: i160) returns (i1) { (if $ne.i160.bool(i1, i2) then 1 else 0) } +function {:define} $ne.i256.bool(i1: i256, i2: i256) returns (bool) { (i1 != i2) } +function {:define} $ne.i256(i1: i256, i2: i256) returns (i1) { (if $ne.i256.bool(i1, i2) then 1 else 0) } +// Integer load/store operations +function {:define} $load.i1(M: [ref] i1, p: ref) returns (i1) { M[p] } +function {:define} $store.i1(M: [ref] i1, p: ref, i: i1) returns ([ref] i1) { M[p := i] } +function {:define} $load.i5(M: [ref] i5, p: ref) returns (i5) { M[p] } +function {:define} $store.i5(M: [ref] i5, p: ref, i: i5) returns ([ref] i5) { M[p := i] } +function {:define} $load.i6(M: [ref] i6, p: ref) returns (i6) { M[p] } +function {:define} $store.i6(M: [ref] i6, p: ref, i: i6) returns ([ref] i6) { M[p := i] } +function {:define} $load.i8(M: [ref] i8, p: ref) returns (i8) { M[p] } +function {:define} $store.i8(M: [ref] i8, p: ref, i: i8) returns ([ref] i8) { M[p := i] } +function {:define} $load.i16(M: [ref] i16, p: ref) returns (i16) { M[p] } +function {:define} $store.i16(M: [ref] i16, p: ref, i: i16) returns ([ref] i16) { M[p := i] } +function {:define} $load.i24(M: [ref] i24, p: ref) returns (i24) { M[p] } +function {:define} $store.i24(M: [ref] i24, p: ref, i: i24) returns ([ref] i24) { M[p := i] } +function {:define} $load.i32(M: [ref] i32, p: ref) returns (i32) { M[p] } +function {:define} $store.i32(M: [ref] i32, p: ref, i: i32) returns ([ref] i32) { M[p := i] } +function {:define} $load.i40(M: [ref] i40, p: ref) returns (i40) { M[p] } +function {:define} $store.i40(M: [ref] i40, p: ref, i: i40) returns ([ref] i40) { M[p := i] } +function {:define} $load.i48(M: [ref] i48, p: ref) returns (i48) { M[p] } +function {:define} $store.i48(M: [ref] i48, p: ref, i: i48) returns ([ref] i48) { M[p := i] } +function {:define} $load.i56(M: [ref] i56, p: ref) returns (i56) { M[p] } +function {:define} $store.i56(M: [ref] i56, p: ref, i: i56) returns ([ref] i56) { M[p := i] } +function {:define} $load.i64(M: [ref] i64, p: ref) returns (i64) { M[p] } +function {:define} $store.i64(M: [ref] i64, p: ref, i: i64) returns ([ref] i64) { M[p := i] } +function {:define} $load.i80(M: [ref] i80, p: ref) returns (i80) { M[p] } +function {:define} $store.i80(M: [ref] i80, p: ref, i: i80) returns ([ref] i80) { M[p := i] } +function {:define} $load.i88(M: [ref] i88, p: ref) returns (i88) { M[p] } +function {:define} $store.i88(M: [ref] i88, p: ref, i: i88) returns ([ref] i88) { M[p := i] } +function {:define} $load.i96(M: [ref] i96, p: ref) returns (i96) { M[p] } +function {:define} $store.i96(M: [ref] i96, p: ref, i: i96) returns ([ref] i96) { M[p := i] } +function {:define} $load.i128(M: [ref] i128, p: ref) returns (i128) { M[p] } +function {:define} $store.i128(M: [ref] i128, p: ref, i: i128) returns ([ref] i128) { M[p := i] } +function {:define} $load.i160(M: [ref] i160, p: ref) returns (i160) { M[p] } +function {:define} $store.i160(M: [ref] i160, p: ref, i: i160) returns ([ref] i160) { M[p := i] } +function {:define} $load.i256(M: [ref] i256, p: ref) returns (i256) { M[p] } +function {:define} $store.i256(M: [ref] i256, p: ref, i: i256) returns ([ref] i256) { M[p := i] } +// Conversion between integer types +function {:define} $trunc.i5.i1(i: i5) returns (i1) { i } +function {:define} $trunc.i6.i1(i: i6) returns (i1) { i } +function {:define} $trunc.i8.i1(i: i8) returns (i1) { i } +function {:define} $trunc.i16.i1(i: i16) returns (i1) { i } +function {:define} $trunc.i24.i1(i: i24) returns (i1) { i } +function {:define} $trunc.i32.i1(i: i32) returns (i1) { i } +function {:define} $trunc.i40.i1(i: i40) returns (i1) { i } +function {:define} $trunc.i48.i1(i: i48) returns (i1) { i } +function {:define} $trunc.i56.i1(i: i56) returns (i1) { i } +function {:define} $trunc.i64.i1(i: i64) returns (i1) { i } +function {:define} $trunc.i80.i1(i: i80) returns (i1) { i } +function {:define} $trunc.i88.i1(i: i88) returns (i1) { i } +function {:define} $trunc.i96.i1(i: i96) returns (i1) { i } +function {:define} $trunc.i128.i1(i: i128) returns (i1) { i } +function {:define} $trunc.i160.i1(i: i160) returns (i1) { i } +function {:define} $trunc.i256.i1(i: i256) returns (i1) { i } +function {:define} $trunc.i6.i5(i: i6) returns (i5) { i } +function {:define} $trunc.i8.i5(i: i8) returns (i5) { i } +function {:define} $trunc.i16.i5(i: i16) returns (i5) { i } +function {:define} $trunc.i24.i5(i: i24) returns (i5) { i } +function {:define} $trunc.i32.i5(i: i32) returns (i5) { i } +function {:define} $trunc.i40.i5(i: i40) returns (i5) { i } +function {:define} $trunc.i48.i5(i: i48) returns (i5) { i } +function {:define} $trunc.i56.i5(i: i56) returns (i5) { i } +function {:define} $trunc.i64.i5(i: i64) returns (i5) { i } +function {:define} $trunc.i80.i5(i: i80) returns (i5) { i } +function {:define} $trunc.i88.i5(i: i88) returns (i5) { i } +function {:define} $trunc.i96.i5(i: i96) returns (i5) { i } +function {:define} $trunc.i128.i5(i: i128) returns (i5) { i } +function {:define} $trunc.i160.i5(i: i160) returns (i5) { i } +function {:define} $trunc.i256.i5(i: i256) returns (i5) { i } +function {:define} $trunc.i8.i6(i: i8) returns (i6) { i } +function {:define} $trunc.i16.i6(i: i16) returns (i6) { i } +function {:define} $trunc.i24.i6(i: i24) returns (i6) { i } +function {:define} $trunc.i32.i6(i: i32) returns (i6) { i } +function {:define} $trunc.i40.i6(i: i40) returns (i6) { i } +function {:define} $trunc.i48.i6(i: i48) returns (i6) { i } +function {:define} $trunc.i56.i6(i: i56) returns (i6) { i } +function {:define} $trunc.i64.i6(i: i64) returns (i6) { i } +function {:define} $trunc.i80.i6(i: i80) returns (i6) { i } +function {:define} $trunc.i88.i6(i: i88) returns (i6) { i } +function {:define} $trunc.i96.i6(i: i96) returns (i6) { i } +function {:define} $trunc.i128.i6(i: i128) returns (i6) { i } +function {:define} $trunc.i160.i6(i: i160) returns (i6) { i } +function {:define} $trunc.i256.i6(i: i256) returns (i6) { i } +function {:define} $trunc.i16.i8(i: i16) returns (i8) { i } +function {:define} $trunc.i24.i8(i: i24) returns (i8) { i } +function {:define} $trunc.i32.i8(i: i32) returns (i8) { i } +function {:define} $trunc.i40.i8(i: i40) returns (i8) { i } +function {:define} $trunc.i48.i8(i: i48) returns (i8) { i } +function {:define} $trunc.i56.i8(i: i56) returns (i8) { i } +function {:define} $trunc.i64.i8(i: i64) returns (i8) { i } +function {:define} $trunc.i80.i8(i: i80) returns (i8) { i } +function {:define} $trunc.i88.i8(i: i88) returns (i8) { i } +function {:define} $trunc.i96.i8(i: i96) returns (i8) { i } +function {:define} $trunc.i128.i8(i: i128) returns (i8) { i } +function {:define} $trunc.i160.i8(i: i160) returns (i8) { i } +function {:define} $trunc.i256.i8(i: i256) returns (i8) { i } +function {:define} $trunc.i24.i16(i: i24) returns (i16) { i } +function {:define} $trunc.i32.i16(i: i32) returns (i16) { i } +function {:define} $trunc.i40.i16(i: i40) returns (i16) { i } +function {:define} $trunc.i48.i16(i: i48) returns (i16) { i } +function {:define} $trunc.i56.i16(i: i56) returns (i16) { i } +function {:define} $trunc.i64.i16(i: i64) returns (i16) { i } +function {:define} $trunc.i80.i16(i: i80) returns (i16) { i } +function {:define} $trunc.i88.i16(i: i88) returns (i16) { i } +function {:define} $trunc.i96.i16(i: i96) returns (i16) { i } +function {:define} $trunc.i128.i16(i: i128) returns (i16) { i } +function {:define} $trunc.i160.i16(i: i160) returns (i16) { i } +function {:define} $trunc.i256.i16(i: i256) returns (i16) { i } +function {:define} $trunc.i32.i24(i: i32) returns (i24) { i } +function {:define} $trunc.i40.i24(i: i40) returns (i24) { i } +function {:define} $trunc.i48.i24(i: i48) returns (i24) { i } +function {:define} $trunc.i56.i24(i: i56) returns (i24) { i } +function {:define} $trunc.i64.i24(i: i64) returns (i24) { i } +function {:define} $trunc.i80.i24(i: i80) returns (i24) { i } +function {:define} $trunc.i88.i24(i: i88) returns (i24) { i } +function {:define} $trunc.i96.i24(i: i96) returns (i24) { i } +function {:define} $trunc.i128.i24(i: i128) returns (i24) { i } +function {:define} $trunc.i160.i24(i: i160) returns (i24) { i } +function {:define} $trunc.i256.i24(i: i256) returns (i24) { i } +function {:define} $trunc.i40.i32(i: i40) returns (i32) { i } +function {:define} $trunc.i48.i32(i: i48) returns (i32) { i } +function {:define} $trunc.i56.i32(i: i56) returns (i32) { i } +function {:define} $trunc.i64.i32(i: i64) returns (i32) { i } +function {:define} $trunc.i80.i32(i: i80) returns (i32) { i } +function {:define} $trunc.i88.i32(i: i88) returns (i32) { i } +function {:define} $trunc.i96.i32(i: i96) returns (i32) { i } +function {:define} $trunc.i128.i32(i: i128) returns (i32) { i } +function {:define} $trunc.i160.i32(i: i160) returns (i32) { i } +function {:define} $trunc.i256.i32(i: i256) returns (i32) { i } +function {:define} $trunc.i48.i40(i: i48) returns (i40) { i } +function {:define} $trunc.i56.i40(i: i56) returns (i40) { i } +function {:define} $trunc.i64.i40(i: i64) returns (i40) { i } +function {:define} $trunc.i80.i40(i: i80) returns (i40) { i } +function {:define} $trunc.i88.i40(i: i88) returns (i40) { i } +function {:define} $trunc.i96.i40(i: i96) returns (i40) { i } +function {:define} $trunc.i128.i40(i: i128) returns (i40) { i } +function {:define} $trunc.i160.i40(i: i160) returns (i40) { i } +function {:define} $trunc.i256.i40(i: i256) returns (i40) { i } +function {:define} $trunc.i56.i48(i: i56) returns (i48) { i } +function {:define} $trunc.i64.i48(i: i64) returns (i48) { i } +function {:define} $trunc.i80.i48(i: i80) returns (i48) { i } +function {:define} $trunc.i88.i48(i: i88) returns (i48) { i } +function {:define} $trunc.i96.i48(i: i96) returns (i48) { i } +function {:define} $trunc.i128.i48(i: i128) returns (i48) { i } +function {:define} $trunc.i160.i48(i: i160) returns (i48) { i } +function {:define} $trunc.i256.i48(i: i256) returns (i48) { i } +function {:define} $trunc.i64.i56(i: i64) returns (i56) { i } +function {:define} $trunc.i80.i56(i: i80) returns (i56) { i } +function {:define} $trunc.i88.i56(i: i88) returns (i56) { i } +function {:define} $trunc.i96.i56(i: i96) returns (i56) { i } +function {:define} $trunc.i128.i56(i: i128) returns (i56) { i } +function {:define} $trunc.i160.i56(i: i160) returns (i56) { i } +function {:define} $trunc.i256.i56(i: i256) returns (i56) { i } +function {:define} $trunc.i80.i64(i: i80) returns (i64) { i } +function {:define} $trunc.i88.i64(i: i88) returns (i64) { i } +function {:define} $trunc.i96.i64(i: i96) returns (i64) { i } +function {:define} $trunc.i128.i64(i: i128) returns (i64) { i } +function {:define} $trunc.i160.i64(i: i160) returns (i64) { i } +function {:define} $trunc.i256.i64(i: i256) returns (i64) { i } +function {:define} $trunc.i88.i80(i: i88) returns (i80) { i } +function {:define} $trunc.i96.i80(i: i96) returns (i80) { i } +function {:define} $trunc.i128.i80(i: i128) returns (i80) { i } +function {:define} $trunc.i160.i80(i: i160) returns (i80) { i } +function {:define} $trunc.i256.i80(i: i256) returns (i80) { i } +function {:define} $trunc.i96.i88(i: i96) returns (i88) { i } +function {:define} $trunc.i128.i88(i: i128) returns (i88) { i } +function {:define} $trunc.i160.i88(i: i160) returns (i88) { i } +function {:define} $trunc.i256.i88(i: i256) returns (i88) { i } +function {:define} $trunc.i128.i96(i: i128) returns (i96) { i } +function {:define} $trunc.i160.i96(i: i160) returns (i96) { i } +function {:define} $trunc.i256.i96(i: i256) returns (i96) { i } +function {:define} $trunc.i160.i128(i: i160) returns (i128) { i } +function {:define} $trunc.i256.i128(i: i256) returns (i128) { i } +function {:define} $trunc.i256.i160(i: i256) returns (i160) { i } +function {:define} $sext.i1.i5(i: i1) returns (i5) { i } +function {:define} $sext.i1.i6(i: i1) returns (i6) { i } +function {:define} $sext.i1.i8(i: i1) returns (i8) { i } +function {:define} $sext.i1.i16(i: i1) returns (i16) { i } +function {:define} $sext.i1.i24(i: i1) returns (i24) { i } +function {:define} $sext.i1.i32(i: i1) returns (i32) { i } +function {:define} $sext.i1.i40(i: i1) returns (i40) { i } +function {:define} $sext.i1.i48(i: i1) returns (i48) { i } +function {:define} $sext.i1.i56(i: i1) returns (i56) { i } +function {:define} $sext.i1.i64(i: i1) returns (i64) { i } +function {:define} $sext.i1.i80(i: i1) returns (i80) { i } +function {:define} $sext.i1.i88(i: i1) returns (i88) { i } +function {:define} $sext.i1.i96(i: i1) returns (i96) { i } +function {:define} $sext.i1.i128(i: i1) returns (i128) { i } +function {:define} $sext.i1.i160(i: i1) returns (i160) { i } +function {:define} $sext.i1.i256(i: i1) returns (i256) { i } +function {:define} $sext.i5.i6(i: i5) returns (i6) { i } +function {:define} $sext.i5.i8(i: i5) returns (i8) { i } +function {:define} $sext.i5.i16(i: i5) returns (i16) { i } +function {:define} $sext.i5.i24(i: i5) returns (i24) { i } +function {:define} $sext.i5.i32(i: i5) returns (i32) { i } +function {:define} $sext.i5.i40(i: i5) returns (i40) { i } +function {:define} $sext.i5.i48(i: i5) returns (i48) { i } +function {:define} $sext.i5.i56(i: i5) returns (i56) { i } +function {:define} $sext.i5.i64(i: i5) returns (i64) { i } +function {:define} $sext.i5.i80(i: i5) returns (i80) { i } +function {:define} $sext.i5.i88(i: i5) returns (i88) { i } +function {:define} $sext.i5.i96(i: i5) returns (i96) { i } +function {:define} $sext.i5.i128(i: i5) returns (i128) { i } +function {:define} $sext.i5.i160(i: i5) returns (i160) { i } +function {:define} $sext.i5.i256(i: i5) returns (i256) { i } +function {:define} $sext.i6.i8(i: i6) returns (i8) { i } +function {:define} $sext.i6.i16(i: i6) returns (i16) { i } +function {:define} $sext.i6.i24(i: i6) returns (i24) { i } +function {:define} $sext.i6.i32(i: i6) returns (i32) { i } +function {:define} $sext.i6.i40(i: i6) returns (i40) { i } +function {:define} $sext.i6.i48(i: i6) returns (i48) { i } +function {:define} $sext.i6.i56(i: i6) returns (i56) { i } +function {:define} $sext.i6.i64(i: i6) returns (i64) { i } +function {:define} $sext.i6.i80(i: i6) returns (i80) { i } +function {:define} $sext.i6.i88(i: i6) returns (i88) { i } +function {:define} $sext.i6.i96(i: i6) returns (i96) { i } +function {:define} $sext.i6.i128(i: i6) returns (i128) { i } +function {:define} $sext.i6.i160(i: i6) returns (i160) { i } +function {:define} $sext.i6.i256(i: i6) returns (i256) { i } +function {:define} $sext.i8.i16(i: i8) returns (i16) { i } +function {:define} $sext.i8.i24(i: i8) returns (i24) { i } +function {:define} $sext.i8.i32(i: i8) returns (i32) { i } +function {:define} $sext.i8.i40(i: i8) returns (i40) { i } +function {:define} $sext.i8.i48(i: i8) returns (i48) { i } +function {:define} $sext.i8.i56(i: i8) returns (i56) { i } +function {:define} $sext.i8.i64(i: i8) returns (i64) { i } +function {:define} $sext.i8.i80(i: i8) returns (i80) { i } +function {:define} $sext.i8.i88(i: i8) returns (i88) { i } +function {:define} $sext.i8.i96(i: i8) returns (i96) { i } +function {:define} $sext.i8.i128(i: i8) returns (i128) { i } +function {:define} $sext.i8.i160(i: i8) returns (i160) { i } +function {:define} $sext.i8.i256(i: i8) returns (i256) { i } +function {:define} $sext.i16.i24(i: i16) returns (i24) { i } +function {:define} $sext.i16.i32(i: i16) returns (i32) { i } +function {:define} $sext.i16.i40(i: i16) returns (i40) { i } +function {:define} $sext.i16.i48(i: i16) returns (i48) { i } +function {:define} $sext.i16.i56(i: i16) returns (i56) { i } +function {:define} $sext.i16.i64(i: i16) returns (i64) { i } +function {:define} $sext.i16.i80(i: i16) returns (i80) { i } +function {:define} $sext.i16.i88(i: i16) returns (i88) { i } +function {:define} $sext.i16.i96(i: i16) returns (i96) { i } +function {:define} $sext.i16.i128(i: i16) returns (i128) { i } +function {:define} $sext.i16.i160(i: i16) returns (i160) { i } +function {:define} $sext.i16.i256(i: i16) returns (i256) { i } +function {:define} $sext.i24.i32(i: i24) returns (i32) { i } +function {:define} $sext.i24.i40(i: i24) returns (i40) { i } +function {:define} $sext.i24.i48(i: i24) returns (i48) { i } +function {:define} $sext.i24.i56(i: i24) returns (i56) { i } +function {:define} $sext.i24.i64(i: i24) returns (i64) { i } +function {:define} $sext.i24.i80(i: i24) returns (i80) { i } +function {:define} $sext.i24.i88(i: i24) returns (i88) { i } +function {:define} $sext.i24.i96(i: i24) returns (i96) { i } +function {:define} $sext.i24.i128(i: i24) returns (i128) { i } +function {:define} $sext.i24.i160(i: i24) returns (i160) { i } +function {:define} $sext.i24.i256(i: i24) returns (i256) { i } +function {:define} $sext.i32.i40(i: i32) returns (i40) { i } +function {:define} $sext.i32.i48(i: i32) returns (i48) { i } +function {:define} $sext.i32.i56(i: i32) returns (i56) { i } +function {:define} $sext.i32.i64(i: i32) returns (i64) { i } +function {:define} $sext.i32.i80(i: i32) returns (i80) { i } +function {:define} $sext.i32.i88(i: i32) returns (i88) { i } +function {:define} $sext.i32.i96(i: i32) returns (i96) { i } +function {:define} $sext.i32.i128(i: i32) returns (i128) { i } +function {:define} $sext.i32.i160(i: i32) returns (i160) { i } +function {:define} $sext.i32.i256(i: i32) returns (i256) { i } +function {:define} $sext.i40.i48(i: i40) returns (i48) { i } +function {:define} $sext.i40.i56(i: i40) returns (i56) { i } +function {:define} $sext.i40.i64(i: i40) returns (i64) { i } +function {:define} $sext.i40.i80(i: i40) returns (i80) { i } +function {:define} $sext.i40.i88(i: i40) returns (i88) { i } +function {:define} $sext.i40.i96(i: i40) returns (i96) { i } +function {:define} $sext.i40.i128(i: i40) returns (i128) { i } +function {:define} $sext.i40.i160(i: i40) returns (i160) { i } +function {:define} $sext.i40.i256(i: i40) returns (i256) { i } +function {:define} $sext.i48.i56(i: i48) returns (i56) { i } +function {:define} $sext.i48.i64(i: i48) returns (i64) { i } +function {:define} $sext.i48.i80(i: i48) returns (i80) { i } +function {:define} $sext.i48.i88(i: i48) returns (i88) { i } +function {:define} $sext.i48.i96(i: i48) returns (i96) { i } +function {:define} $sext.i48.i128(i: i48) returns (i128) { i } +function {:define} $sext.i48.i160(i: i48) returns (i160) { i } +function {:define} $sext.i48.i256(i: i48) returns (i256) { i } +function {:define} $sext.i56.i64(i: i56) returns (i64) { i } +function {:define} $sext.i56.i80(i: i56) returns (i80) { i } +function {:define} $sext.i56.i88(i: i56) returns (i88) { i } +function {:define} $sext.i56.i96(i: i56) returns (i96) { i } +function {:define} $sext.i56.i128(i: i56) returns (i128) { i } +function {:define} $sext.i56.i160(i: i56) returns (i160) { i } +function {:define} $sext.i56.i256(i: i56) returns (i256) { i } +function {:define} $sext.i64.i80(i: i64) returns (i80) { i } +function {:define} $sext.i64.i88(i: i64) returns (i88) { i } +function {:define} $sext.i64.i96(i: i64) returns (i96) { i } +function {:define} $sext.i64.i128(i: i64) returns (i128) { i } +function {:define} $sext.i64.i160(i: i64) returns (i160) { i } +function {:define} $sext.i64.i256(i: i64) returns (i256) { i } +function {:define} $sext.i80.i88(i: i80) returns (i88) { i } +function {:define} $sext.i80.i96(i: i80) returns (i96) { i } +function {:define} $sext.i80.i128(i: i80) returns (i128) { i } +function {:define} $sext.i80.i160(i: i80) returns (i160) { i } +function {:define} $sext.i80.i256(i: i80) returns (i256) { i } +function {:define} $sext.i88.i96(i: i88) returns (i96) { i } +function {:define} $sext.i88.i128(i: i88) returns (i128) { i } +function {:define} $sext.i88.i160(i: i88) returns (i160) { i } +function {:define} $sext.i88.i256(i: i88) returns (i256) { i } +function {:define} $sext.i96.i128(i: i96) returns (i128) { i } +function {:define} $sext.i96.i160(i: i96) returns (i160) { i } +function {:define} $sext.i96.i256(i: i96) returns (i256) { i } +function {:define} $sext.i128.i160(i: i128) returns (i160) { i } +function {:define} $sext.i128.i256(i: i128) returns (i256) { i } +function {:define} $sext.i160.i256(i: i160) returns (i256) { i } +function {:define} $zext.i1.i5(i: i1) returns (i5) { i } +function {:define} $zext.i1.i6(i: i1) returns (i6) { i } +function {:define} $zext.i1.i8(i: i1) returns (i8) { i } +function {:define} $zext.i1.i16(i: i1) returns (i16) { i } +function {:define} $zext.i1.i24(i: i1) returns (i24) { i } +function {:define} $zext.i1.i32(i: i1) returns (i32) { i } +function {:define} $zext.i1.i40(i: i1) returns (i40) { i } +function {:define} $zext.i1.i48(i: i1) returns (i48) { i } +function {:define} $zext.i1.i56(i: i1) returns (i56) { i } +function {:define} $zext.i1.i64(i: i1) returns (i64) { i } +function {:define} $zext.i1.i80(i: i1) returns (i80) { i } +function {:define} $zext.i1.i88(i: i1) returns (i88) { i } +function {:define} $zext.i1.i96(i: i1) returns (i96) { i } +function {:define} $zext.i1.i128(i: i1) returns (i128) { i } +function {:define} $zext.i1.i160(i: i1) returns (i160) { i } +function {:define} $zext.i1.i256(i: i1) returns (i256) { i } +function {:define} $zext.i5.i6(i: i5) returns (i6) { i } +function {:define} $zext.i5.i8(i: i5) returns (i8) { i } +function {:define} $zext.i5.i16(i: i5) returns (i16) { i } +function {:define} $zext.i5.i24(i: i5) returns (i24) { i } +function {:define} $zext.i5.i32(i: i5) returns (i32) { i } +function {:define} $zext.i5.i40(i: i5) returns (i40) { i } +function {:define} $zext.i5.i48(i: i5) returns (i48) { i } +function {:define} $zext.i5.i56(i: i5) returns (i56) { i } +function {:define} $zext.i5.i64(i: i5) returns (i64) { i } +function {:define} $zext.i5.i80(i: i5) returns (i80) { i } +function {:define} $zext.i5.i88(i: i5) returns (i88) { i } +function {:define} $zext.i5.i96(i: i5) returns (i96) { i } +function {:define} $zext.i5.i128(i: i5) returns (i128) { i } +function {:define} $zext.i5.i160(i: i5) returns (i160) { i } +function {:define} $zext.i5.i256(i: i5) returns (i256) { i } +function {:define} $zext.i6.i8(i: i6) returns (i8) { i } +function {:define} $zext.i6.i16(i: i6) returns (i16) { i } +function {:define} $zext.i6.i24(i: i6) returns (i24) { i } +function {:define} $zext.i6.i32(i: i6) returns (i32) { i } +function {:define} $zext.i6.i40(i: i6) returns (i40) { i } +function {:define} $zext.i6.i48(i: i6) returns (i48) { i } +function {:define} $zext.i6.i56(i: i6) returns (i56) { i } +function {:define} $zext.i6.i64(i: i6) returns (i64) { i } +function {:define} $zext.i6.i80(i: i6) returns (i80) { i } +function {:define} $zext.i6.i88(i: i6) returns (i88) { i } +function {:define} $zext.i6.i96(i: i6) returns (i96) { i } +function {:define} $zext.i6.i128(i: i6) returns (i128) { i } +function {:define} $zext.i6.i160(i: i6) returns (i160) { i } +function {:define} $zext.i6.i256(i: i6) returns (i256) { i } +function {:define} $zext.i8.i16(i: i8) returns (i16) { i } +function {:define} $zext.i8.i24(i: i8) returns (i24) { i } +function {:define} $zext.i8.i32(i: i8) returns (i32) { i } +function {:define} $zext.i8.i40(i: i8) returns (i40) { i } +function {:define} $zext.i8.i48(i: i8) returns (i48) { i } +function {:define} $zext.i8.i56(i: i8) returns (i56) { i } +function {:define} $zext.i8.i64(i: i8) returns (i64) { i } +function {:define} $zext.i8.i80(i: i8) returns (i80) { i } +function {:define} $zext.i8.i88(i: i8) returns (i88) { i } +function {:define} $zext.i8.i96(i: i8) returns (i96) { i } +function {:define} $zext.i8.i128(i: i8) returns (i128) { i } +function {:define} $zext.i8.i160(i: i8) returns (i160) { i } +function {:define} $zext.i8.i256(i: i8) returns (i256) { i } +function {:define} $zext.i16.i24(i: i16) returns (i24) { i } +function {:define} $zext.i16.i32(i: i16) returns (i32) { i } +function {:define} $zext.i16.i40(i: i16) returns (i40) { i } +function {:define} $zext.i16.i48(i: i16) returns (i48) { i } +function {:define} $zext.i16.i56(i: i16) returns (i56) { i } +function {:define} $zext.i16.i64(i: i16) returns (i64) { i } +function {:define} $zext.i16.i80(i: i16) returns (i80) { i } +function {:define} $zext.i16.i88(i: i16) returns (i88) { i } +function {:define} $zext.i16.i96(i: i16) returns (i96) { i } +function {:define} $zext.i16.i128(i: i16) returns (i128) { i } +function {:define} $zext.i16.i160(i: i16) returns (i160) { i } +function {:define} $zext.i16.i256(i: i16) returns (i256) { i } +function {:define} $zext.i24.i32(i: i24) returns (i32) { i } +function {:define} $zext.i24.i40(i: i24) returns (i40) { i } +function {:define} $zext.i24.i48(i: i24) returns (i48) { i } +function {:define} $zext.i24.i56(i: i24) returns (i56) { i } +function {:define} $zext.i24.i64(i: i24) returns (i64) { i } +function {:define} $zext.i24.i80(i: i24) returns (i80) { i } +function {:define} $zext.i24.i88(i: i24) returns (i88) { i } +function {:define} $zext.i24.i96(i: i24) returns (i96) { i } +function {:define} $zext.i24.i128(i: i24) returns (i128) { i } +function {:define} $zext.i24.i160(i: i24) returns (i160) { i } +function {:define} $zext.i24.i256(i: i24) returns (i256) { i } +function {:define} $zext.i32.i40(i: i32) returns (i40) { i } +function {:define} $zext.i32.i48(i: i32) returns (i48) { i } +function {:define} $zext.i32.i56(i: i32) returns (i56) { i } +function {:define} $zext.i32.i64(i: i32) returns (i64) { i } +function {:define} $zext.i32.i80(i: i32) returns (i80) { i } +function {:define} $zext.i32.i88(i: i32) returns (i88) { i } +function {:define} $zext.i32.i96(i: i32) returns (i96) { i } +function {:define} $zext.i32.i128(i: i32) returns (i128) { i } +function {:define} $zext.i32.i160(i: i32) returns (i160) { i } +function {:define} $zext.i32.i256(i: i32) returns (i256) { i } +function {:define} $zext.i40.i48(i: i40) returns (i48) { i } +function {:define} $zext.i40.i56(i: i40) returns (i56) { i } +function {:define} $zext.i40.i64(i: i40) returns (i64) { i } +function {:define} $zext.i40.i80(i: i40) returns (i80) { i } +function {:define} $zext.i40.i88(i: i40) returns (i88) { i } +function {:define} $zext.i40.i96(i: i40) returns (i96) { i } +function {:define} $zext.i40.i128(i: i40) returns (i128) { i } +function {:define} $zext.i40.i160(i: i40) returns (i160) { i } +function {:define} $zext.i40.i256(i: i40) returns (i256) { i } +function {:define} $zext.i48.i56(i: i48) returns (i56) { i } +function {:define} $zext.i48.i64(i: i48) returns (i64) { i } +function {:define} $zext.i48.i80(i: i48) returns (i80) { i } +function {:define} $zext.i48.i88(i: i48) returns (i88) { i } +function {:define} $zext.i48.i96(i: i48) returns (i96) { i } +function {:define} $zext.i48.i128(i: i48) returns (i128) { i } +function {:define} $zext.i48.i160(i: i48) returns (i160) { i } +function {:define} $zext.i48.i256(i: i48) returns (i256) { i } +function {:define} $zext.i56.i64(i: i56) returns (i64) { i } +function {:define} $zext.i56.i80(i: i56) returns (i80) { i } +function {:define} $zext.i56.i88(i: i56) returns (i88) { i } +function {:define} $zext.i56.i96(i: i56) returns (i96) { i } +function {:define} $zext.i56.i128(i: i56) returns (i128) { i } +function {:define} $zext.i56.i160(i: i56) returns (i160) { i } +function {:define} $zext.i56.i256(i: i56) returns (i256) { i } +function {:define} $zext.i64.i80(i: i64) returns (i80) { i } +function {:define} $zext.i64.i88(i: i64) returns (i88) { i } +function {:define} $zext.i64.i96(i: i64) returns (i96) { i } +function {:define} $zext.i64.i128(i: i64) returns (i128) { i } +function {:define} $zext.i64.i160(i: i64) returns (i160) { i } +function {:define} $zext.i64.i256(i: i64) returns (i256) { i } +function {:define} $zext.i80.i88(i: i80) returns (i88) { i } +function {:define} $zext.i80.i96(i: i80) returns (i96) { i } +function {:define} $zext.i80.i128(i: i80) returns (i128) { i } +function {:define} $zext.i80.i160(i: i80) returns (i160) { i } +function {:define} $zext.i80.i256(i: i80) returns (i256) { i } +function {:define} $zext.i88.i96(i: i88) returns (i96) { i } +function {:define} $zext.i88.i128(i: i88) returns (i128) { i } +function {:define} $zext.i88.i160(i: i88) returns (i160) { i } +function {:define} $zext.i88.i256(i: i88) returns (i256) { i } +function {:define} $zext.i96.i128(i: i96) returns (i128) { i } +function {:define} $zext.i96.i160(i: i96) returns (i160) { i } +function {:define} $zext.i96.i256(i: i96) returns (i256) { i } +function {:define} $zext.i128.i160(i: i128) returns (i160) { i } +function {:define} $zext.i128.i256(i: i128) returns (i256) { i } +function {:define} $zext.i160.i256(i: i160) returns (i256) { i } +function $extractvalue.i1(p: ref, i: int) returns (i1); +function $extractvalue.i5(p: ref, i: int) returns (i5); +function $extractvalue.i6(p: ref, i: int) returns (i6); +function $extractvalue.i8(p: ref, i: int) returns (i8); +function $extractvalue.i16(p: ref, i: int) returns (i16); +function $extractvalue.i24(p: ref, i: int) returns (i24); +function $extractvalue.i32(p: ref, i: int) returns (i32); +function $extractvalue.i40(p: ref, i: int) returns (i40); +function $extractvalue.i48(p: ref, i: int) returns (i48); +function $extractvalue.i56(p: ref, i: int) returns (i56); +function $extractvalue.i64(p: ref, i: int) returns (i64); +function $extractvalue.i80(p: ref, i: int) returns (i80); +function $extractvalue.i88(p: ref, i: int) returns (i88); +function $extractvalue.i96(p: ref, i: int) returns (i96); +function $extractvalue.i128(p: ref, i: int) returns (i128); +function $extractvalue.i160(p: ref, i: int) returns (i160); +function $extractvalue.i256(p: ref, i: int) returns (i256); +// Pointer arithmetic operations +function {:define} $add.ref(p1: ref, p2: ref) returns (ref) { $add.i64(p1, p2) } +function {:define} $sub.ref(p1: ref, p2: ref) returns (ref) { $sub.i64(p1, p2) } +function {:define} $mul.ref(p1: ref, p2: ref) returns (ref) { $mul.i64(p1, p2) } + +// Pointer predicates +function {:define} $eq.ref(p1: ref, p2: ref) returns (i1) { (if $eq.i64.bool(p1, p2) then 1 else 0) } +function {:define} $eq.ref.bool(p1: ref, p2: ref) returns (bool) { $eq.i64.bool(p1, p2) } +function {:define} $ne.ref(p1: ref, p2: ref) returns (i1) { (if $ne.i64.bool(p1, p2) then 1 else 0) } +function {:define} $ne.ref.bool(p1: ref, p2: ref) returns (bool) { $ne.i64.bool(p1, p2) } +function {:define} $ugt.ref(p1: ref, p2: ref) returns (i1) { (if $ugt.i64.bool(p1, p2) then 1 else 0) } +function {:define} $ugt.ref.bool(p1: ref, p2: ref) returns (bool) { $ugt.i64.bool(p1, p2) } +function {:define} $uge.ref(p1: ref, p2: ref) returns (i1) { (if $uge.i64.bool(p1, p2) then 1 else 0) } +function {:define} $uge.ref.bool(p1: ref, p2: ref) returns (bool) { $uge.i64.bool(p1, p2) } +function {:define} $ult.ref(p1: ref, p2: ref) returns (i1) { (if $ult.i64.bool(p1, p2) then 1 else 0) } +function {:define} $ult.ref.bool(p1: ref, p2: ref) returns (bool) { $ult.i64.bool(p1, p2) } +function {:define} $ule.ref(p1: ref, p2: ref) returns (i1) { (if $ule.i64.bool(p1, p2) then 1 else 0) } +function {:define} $ule.ref.bool(p1: ref, p2: ref) returns (bool) { $ule.i64.bool(p1, p2) } +function {:define} $sgt.ref(p1: ref, p2: ref) returns (i1) { (if $sgt.i64.bool(p1, p2) then 1 else 0) } +function {:define} $sgt.ref.bool(p1: ref, p2: ref) returns (bool) { $sgt.i64.bool(p1, p2) } +function {:define} $sge.ref(p1: ref, p2: ref) returns (i1) { (if $sge.i64.bool(p1, p2) then 1 else 0) } +function {:define} $sge.ref.bool(p1: ref, p2: ref) returns (bool) { $sge.i64.bool(p1, p2) } +function {:define} $slt.ref(p1: ref, p2: ref) returns (i1) { (if $slt.i64.bool(p1, p2) then 1 else 0) } +function {:define} $slt.ref.bool(p1: ref, p2: ref) returns (bool) { $slt.i64.bool(p1, p2) } +function {:define} $sle.ref(p1: ref, p2: ref) returns (i1) { (if $sle.i64.bool(p1, p2) then 1 else 0) } +function {:define} $sle.ref.bool(p1: ref, p2: ref) returns (bool) { $sle.i64.bool(p1, p2) } + +// Pointer load/store operations +function {:define} $load.ref(M: [ref] ref, p: ref) returns (ref) { M[p] } +function {:define} $store.ref(M: [ref] ref, p: ref, i: ref) returns ([ref] ref) { M[p := i] } + +// Pointer conversion +function {:define} $bitcast.ref.ref(p: ref) returns (ref) { p } +function $extractvalue.ref(p: ref, i: int) returns (ref); +// Pointer-number conversion +function {:define} $p2i.ref.i8(p: ref) returns (i8) { $trunc.i64.i8(p) } +function {:define} $i2p.i8.ref(i: i8) returns (ref) { $zext.i8.i64(i) } +function {:define} $p2i.ref.i16(p: ref) returns (i16) { $trunc.i64.i16(p) } +function {:define} $i2p.i16.ref(i: i16) returns (ref) { $zext.i16.i64(i) } +function {:define} $p2i.ref.i32(p: ref) returns (i32) { $trunc.i64.i32(p) } +function {:define} $i2p.i32.ref(i: i32) returns (ref) { $zext.i32.i64(i) } +function {:define} $p2i.ref.i64(p: ref) returns (i64) { p } +function {:define} $i2p.i64.ref(i: i64) returns (ref) { i } + +function $fp(ipart: int, fpart: int, epart: int) returns (float); +// Floating-point arithmetic operations +function $abs.float(f: float) returns (float); +function $round.float(f: float) returns (float); +function $sqrt.float(f: float) returns (float); +function $fadd.float(f1: float, f2: float) returns (float); +function $fsub.float(f1: float, f2: float) returns (float); +function $fmul.float(f1: float, f2: float) returns (float); +function $fdiv.float(f1: float, f2: float) returns (float); +function $frem.float(f1: float, f2: float) returns (float); +function $min.float(f1: float, f2: float) returns (float); +function $max.float(f1: float, f2: float) returns (float); +function $fma.float(f1: float, f2: float, f3: float) returns (float); +// Floating-point predicates +function $foeq.float.bool(f1: float, f2: float) returns (bool); +function $fole.float.bool(f1: float, f2: float) returns (bool); +function $folt.float.bool(f1: float, f2: float) returns (bool); +function $foge.float.bool(f1: float, f2: float) returns (bool); +function $fogt.float.bool(f1: float, f2: float) returns (bool); +function $fone.float.bool(f1: float, f2: float) returns (bool); +function $ford.float.bool(f1: float, f2: float) returns (bool); +function $fueq.float.bool(f1: float, f2: float) returns (bool); +function $fugt.float.bool(f1: float, f2: float) returns (bool); +function $fuge.float.bool(f1: float, f2: float) returns (bool); +function $fult.float.bool(f1: float, f2: float) returns (bool); +function $fule.float.bool(f1: float, f2: float) returns (bool); +function $fune.float.bool(f1: float, f2: float) returns (bool); +function $funo.float.bool(f1: float, f2: float) returns (bool); +function $ffalse.float.bool(f1: float, f2: float) returns (bool); +function $ftrue.float.bool(f1: float, f2: float) returns (bool); +// Floating-point/integer conversion +function $bitcast.float.i8(f: float) returns (i8); +function $bitcast.float.i16(f: float) returns (i16); +function $bitcast.float.i32(f: float) returns (i32); +function $bitcast.float.i64(f: float) returns (i64); +function $bitcast.float.i80(f: float) returns (i80); +function $bitcast.i8.float(i: i8) returns (float); +function $bitcast.i16.float(i: i16) returns (float); +function $bitcast.i32.float(i: i32) returns (float); +function $bitcast.i64.float(i: i64) returns (float); +function $bitcast.i80.float(i: i80) returns (float); +function $fp2si.float.i1(f: float) returns (i1); +function $fp2si.float.i5(f: float) returns (i5); +function $fp2si.float.i6(f: float) returns (i6); +function $fp2si.float.i8(f: float) returns (i8); +function $fp2si.float.i16(f: float) returns (i16); +function $fp2si.float.i24(f: float) returns (i24); +function $fp2si.float.i32(f: float) returns (i32); +function $fp2si.float.i40(f: float) returns (i40); +function $fp2si.float.i48(f: float) returns (i48); +function $fp2si.float.i56(f: float) returns (i56); +function $fp2si.float.i64(f: float) returns (i64); +function $fp2si.float.i80(f: float) returns (i80); +function $fp2si.float.i88(f: float) returns (i88); +function $fp2si.float.i96(f: float) returns (i96); +function $fp2si.float.i128(f: float) returns (i128); +function $fp2si.float.i160(f: float) returns (i160); +function $fp2si.float.i256(f: float) returns (i256); +function $fp2ui.float.i1(f: float) returns (i1); +function $fp2ui.float.i5(f: float) returns (i5); +function $fp2ui.float.i6(f: float) returns (i6); +function $fp2ui.float.i8(f: float) returns (i8); +function $fp2ui.float.i16(f: float) returns (i16); +function $fp2ui.float.i24(f: float) returns (i24); +function $fp2ui.float.i32(f: float) returns (i32); +function $fp2ui.float.i40(f: float) returns (i40); +function $fp2ui.float.i48(f: float) returns (i48); +function $fp2ui.float.i56(f: float) returns (i56); +function $fp2ui.float.i64(f: float) returns (i64); +function $fp2ui.float.i80(f: float) returns (i80); +function $fp2ui.float.i88(f: float) returns (i88); +function $fp2ui.float.i96(f: float) returns (i96); +function $fp2ui.float.i128(f: float) returns (i128); +function $fp2ui.float.i160(f: float) returns (i160); +function $fp2ui.float.i256(f: float) returns (i256); +function $si2fp.i1.float(i: i1) returns (float); +function $si2fp.i5.float(i: i5) returns (float); +function $si2fp.i6.float(i: i6) returns (float); +function $si2fp.i8.float(i: i8) returns (float); +function $si2fp.i16.float(i: i16) returns (float); +function $si2fp.i24.float(i: i24) returns (float); +function $si2fp.i32.float(i: i32) returns (float); +function $si2fp.i40.float(i: i40) returns (float); +function $si2fp.i48.float(i: i48) returns (float); +function $si2fp.i56.float(i: i56) returns (float); +function $si2fp.i64.float(i: i64) returns (float); +function $si2fp.i80.float(i: i80) returns (float); +function $si2fp.i88.float(i: i88) returns (float); +function $si2fp.i96.float(i: i96) returns (float); +function $si2fp.i128.float(i: i128) returns (float); +function $si2fp.i160.float(i: i160) returns (float); +function $si2fp.i256.float(i: i256) returns (float); +function $ui2fp.i1.float(i: i1) returns (float); +function $ui2fp.i5.float(i: i5) returns (float); +function $ui2fp.i6.float(i: i6) returns (float); +function $ui2fp.i8.float(i: i8) returns (float); +function $ui2fp.i16.float(i: i16) returns (float); +function $ui2fp.i24.float(i: i24) returns (float); +function $ui2fp.i32.float(i: i32) returns (float); +function $ui2fp.i40.float(i: i40) returns (float); +function $ui2fp.i48.float(i: i48) returns (float); +function $ui2fp.i56.float(i: i56) returns (float); +function $ui2fp.i64.float(i: i64) returns (float); +function $ui2fp.i80.float(i: i80) returns (float); +function $ui2fp.i88.float(i: i88) returns (float); +function $ui2fp.i96.float(i: i96) returns (float); +function $ui2fp.i128.float(i: i128) returns (float); +function $ui2fp.i160.float(i: i160) returns (float); +function $ui2fp.i256.float(i: i256) returns (float); +// Floating-point conversion +function $fpext.float.float(f: float) returns (float); +function $fptrunc.float.float(f: float) returns (float); +// Floating-point load/store operations +function {:define} $load.float(M: [ref] float, p: ref) returns (float) { M[p] } +function {:define} $store.float(M: [ref] float, p: ref, f: float) returns ([ref] float) { M[p := f] } +function {:define} $load.unsafe.float(M: [ref] i8, p: ref) returns (float) { $bitcast.i8.float(M[p]) } +function {:define} $store.unsafe.float(M: [ref] i8, p: ref, f: float) returns ([ref] i8) { M[p := $bitcast.float.i8(f)] } +function $extractvalue.float(p: ref, i: int) returns (float); +const {:count 14} .str.2: ref; +axiom (.str.2 == $sub.ref(0, 1038)); +const env_value_str: ref; +axiom (env_value_str == $sub.ref(0, 2070)); +const {:count 3} .str.1.3: ref; +axiom (.str.1.3 == $sub.ref(0, 3097)); +const {:count 14} .str.20: ref; +axiom (.str.20 == $sub.ref(0, 4135)); +const errno_global: ref; +axiom (errno_global == $sub.ref(0, 5163)); +const resetArray: ref; +axiom (resetArray == $sub.ref(0, 6195)); +procedure {:inline 11} resetArray($p0: ref) +{ + var $i1: i32; + var $i2: i1; + var $i3: i64; + var $p4: ref; + var $i5: i32; +$bb0: + assume {:sourceloc "two_arrays.c", 16, 8} true; + assume {:verifier.code 0} true; + assume {:sourceloc "two_arrays.c", 16, 8} true; + assume {:verifier.code 0} true; + $i1 := 0; + goto $bb1; +$bb1: + assume {:sourceloc "two_arrays.c", 0, 0} true; + assume {:verifier.code 0} true; + assume {:sourceloc "two_arrays.c", 16, 17} true; + assume {:verifier.code 0} true; + $i2 := $slt.i32($i1, 10); + assume {:sourceloc "two_arrays.c", 16, 3} true; + assume {:verifier.code 0} true; + assume {:branchcond $i2} true; + goto $bb2, $bb3; +$bb2: + assume ($i2 == 1); + assume {:sourceloc "two_arrays.c", 17, 5} true; + assume {:verifier.code 0} true; + $i3 := $sext.i32.i64($i1); + assume {:sourceloc "two_arrays.c", 17, 5} true; + assume {:verifier.code 0} true; + $p4 := $add.ref($p0, $mul.ref($i3, 4)); + assume {:sourceloc "two_arrays.c", 17, 14} true; + assume {:verifier.code 0} true; + $M.0 := $store.i32($M.0, $p4, 0); + assume {:sourceloc "two_arrays.c", 18, 3} true; + assume {:verifier.code 0} true; + goto $bb4; +$bb3: + assume !(($i2 == 1)); + assume {:sourceloc "two_arrays.c", 19, 1} true; + assume {:verifier.code 0} true; + $exn := false; + return; +$bb4: + assume {:sourceloc "two_arrays.c", 16, 29} true; + assume {:verifier.code 0} true; + $i5 := $add.i32($i1, 1); + call {:cexpr "i"} boogie_si_record_i32($i5); + assume {:sourceloc "two_arrays.c", 16, 3} true; + assume {:verifier.code 0} true; + $i1 := $i5; + goto $bb1; +} +const setArray: ref; +axiom (setArray == $sub.ref(0, 7227)); +procedure {:inline 11} setArray($p0: ref) +{ + var $i1: i32; + var $i2: i1; + var $i3: i64; + var $p4: ref; + var $i5: i32; +$bb0: + assume {:sourceloc "two_arrays.c", 24, 8} true; + assume {:verifier.code 0} true; + assume {:sourceloc "two_arrays.c", 24, 8} true; + assume {:verifier.code 0} true; + $i1 := 0; + goto $bb1; +$bb1: + assume {:sourceloc "two_arrays.c", 0, 0} true; + assume {:verifier.code 0} true; + assume {:sourceloc "two_arrays.c", 24, 17} true; + assume {:verifier.code 0} true; + $i2 := $slt.i32($i1, 10); + assume {:sourceloc "two_arrays.c", 24, 3} true; + assume {:verifier.code 0} true; + assume {:branchcond $i2} true; + goto $bb2, $bb3; +$bb2: + assume ($i2 == 1); + assume {:sourceloc "two_arrays.c", 25, 5} true; + assume {:verifier.code 0} true; + $i3 := $sext.i32.i64($i1); + assume {:sourceloc "two_arrays.c", 25, 5} true; + assume {:verifier.code 0} true; + $p4 := $add.ref($p0, $mul.ref($i3, 4)); + assume {:sourceloc "two_arrays.c", 25, 14} true; + assume {:verifier.code 0} true; + $M.0 := $store.i32($M.0, $p4, 1); + assume {:sourceloc "two_arrays.c", 26, 3} true; + assume {:verifier.code 0} true; + goto $bb4; +$bb3: + assume !(($i2 == 1)); + assume {:sourceloc "two_arrays.c", 27, 1} true; + assume {:verifier.code 0} true; + $exn := false; + return; +$bb4: + assume {:sourceloc "two_arrays.c", 24, 29} true; + assume {:verifier.code 0} true; + $i5 := $add.i32($i1, 1); + call {:cexpr "i"} boogie_si_record_i32($i5); + assume {:sourceloc "two_arrays.c", 24, 3} true; + assume {:verifier.code 0} true; + $i1 := $i5; + goto $bb1; +} +const main: ref; +axiom (main == $sub.ref(0, 8259)); +procedure {:entrypoint} main() + returns ($r: i32) +{ + var $p0: ref; + var $p1: ref; + var $p2: ref; + var $p3: ref; + var $i4: i32; + var $i5: i1; + var $i6: i64; + var $p7: ref; + var $i8: i32; + var $i9: i1; + var $i10: i64; + var $p11: ref; + var $i12: i32; + var $i13: i1; + var $i14: i32; + var $i15: i32; + var $i16: i1; + var $i17: i64; + var $p18: ref; + var $i19: i32; + var $i20: i1; + var $i21: i64; + var $p22: ref; + var $i23: i32; + var $i24: i1; + var $i25: i32; + var $p26: ref; + var $p27: ref; +$bb0: + call $initialize(); + assume {:sourceloc "two_arrays.c", 31, 26} true; + assume {:verifier.code 0} true; + call {:cexpr "smack:entry:main"} boogie_si_record_ref(main); + assume {:sourceloc "two_arrays.c", 31, 26} true; + assume {:verifier.code 0} true; + call $p0 := malloc(40); + assume {:sourceloc "two_arrays.c", 31, 19} true; + assume {:verifier.code 0} true; + $p1 := $bitcast.ref.ref($p0); + assume {:sourceloc "two_arrays.c", 32, 26} true; + assume {:verifier.code 0} true; + call $p2 := malloc(40); + assume {:sourceloc "two_arrays.c", 32, 19} true; + assume {:verifier.code 0} true; + $p3 := $bitcast.ref.ref($p2); + assume {:sourceloc "two_arrays.c", 34, 3} true; + assume {:verifier.code 0} true; + call resetArray($p1); + assume {:sourceloc "two_arrays.c", 35, 3} true; + assume {:verifier.code 0} true; + call setArray($p3); + assume {:sourceloc "two_arrays.c", 37, 8} true; + assume {:verifier.code 0} true; + $i4 := 0; + goto $bb1; +$bb1: + assume {:sourceloc "two_arrays.c", 0, 0} true; + assume {:verifier.code 0} true; + assume {:sourceloc "two_arrays.c", 37, 17} true; + assume {:verifier.code 0} true; + $i5 := $slt.i32($i4, 10); + assume {:sourceloc "two_arrays.c", 37, 3} true; + assume {:verifier.code 0} true; + assume {:branchcond $i5} true; + goto $bb2, $bb3; +$bb2: + assume ($i5 == 1); + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + goto $bb4; +$bb3: + assume !(($i5 == 1)); + assume {:sourceloc "two_arrays.c", 42, 3} true; + assume {:verifier.code 0} true; + call setArray($p1); + assume {:sourceloc "two_arrays.c", 43, 3} true; + assume {:verifier.code 0} true; + call resetArray($p3); + assume {:sourceloc "two_arrays.c", 45, 8} true; + assume {:verifier.code 0} true; + $i15 := 0; + goto $bb15; +$bb4: + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + $i6 := $sext.i32.i64($i4); + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + $p7 := $add.ref($p1, $mul.ref($i6, 4)); + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + $i8 := $load.i32($M.0, $p7); + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + $i9 := $eq.i32($i8, 0); + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + assume {:branchcond $i9} true; + goto $bb5, $bb7; +$bb5: + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + assume ($i9 == 1); + goto $bb6; +$bb6: + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + goto $bb8; +$bb7: + assume !(($i9 == 1)); + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 1} true; + call __VERIFIER_assert(0); + assume {:sourceloc "two_arrays.c", 38, 5} true; + assume {:verifier.code 0} true; + goto $bb6; +$bb8: + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + goto $bb9; +$bb9: + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + $i10 := $sext.i32.i64($i4); + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + $p11 := $add.ref($p3, $mul.ref($i10, 4)); + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + $i12 := $load.i32($M.0, $p11); + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + $i13 := $eq.i32($i12, 1); + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + assume {:branchcond $i13} true; + goto $bb10, $bb12; +$bb10: + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + assume ($i13 == 1); + goto $bb11; +$bb11: + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + goto $bb13; +$bb12: + assume !(($i13 == 1)); + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 1} true; + call __VERIFIER_assert(0); + assume {:sourceloc "two_arrays.c", 39, 5} true; + assume {:verifier.code 0} true; + goto $bb11; +$bb13: + assume {:sourceloc "two_arrays.c", 40, 3} true; + assume {:verifier.code 0} true; + goto $bb14; +$bb14: + assume {:sourceloc "two_arrays.c", 37, 29} true; + assume {:verifier.code 0} true; + $i14 := $add.i32($i4, 1); + call {:cexpr "i"} boogie_si_record_i32($i14); + assume {:sourceloc "two_arrays.c", 37, 3} true; + assume {:verifier.code 0} true; + $i4 := $i14; + goto $bb1; +$bb15: + assume {:sourceloc "two_arrays.c", 0, 0} true; + assume {:verifier.code 0} true; + assume {:sourceloc "two_arrays.c", 45, 17} true; + assume {:verifier.code 0} true; + $i16 := $slt.i32($i15, 10); + assume {:sourceloc "two_arrays.c", 45, 3} true; + assume {:verifier.code 0} true; + assume {:branchcond $i16} true; + goto $bb16, $bb17; +$bb16: + assume ($i16 == 1); + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + goto $bb18; +$bb17: + assume !(($i16 == 1)); + assume {:sourceloc "two_arrays.c", 50, 8} true; + assume {:verifier.code 0} true; + $p26 := $bitcast.ref.ref($p1); + assume {:sourceloc "two_arrays.c", 50, 3} true; + assume {:verifier.code 0} true; + call free_($p26); + assume {:sourceloc "two_arrays.c", 51, 8} true; + assume {:verifier.code 0} true; + $p27 := $bitcast.ref.ref($p3); + assume {:sourceloc "two_arrays.c", 51, 3} true; + assume {:verifier.code 0} true; + call free_($p27); + assume {:sourceloc "two_arrays.c", 52, 3} true; + assume {:verifier.code 0} true; + $r := 0; + $exn := false; + return; +$bb18: + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + $i17 := $sext.i32.i64($i15); + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + $p18 := $add.ref($p1, $mul.ref($i17, 4)); + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + $i19 := $load.i32($M.0, $p18); + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + $i20 := $eq.i32($i19, 1); + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + assume {:branchcond $i20} true; + goto $bb19, $bb21; +$bb19: + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + assume ($i20 == 1); + goto $bb20; +$bb20: + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + goto $bb22; +$bb21: + assume !(($i20 == 1)); + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 1} true; + call __VERIFIER_assert(0); + assume {:sourceloc "two_arrays.c", 46, 5} true; + assume {:verifier.code 0} true; + goto $bb20; +$bb22: + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + goto $bb23; +$bb23: + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + $i21 := $sext.i32.i64($i15); + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + $p22 := $add.ref($p3, $mul.ref($i21, 4)); + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + $i23 := $load.i32($M.0, $p22); + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + $i24 := $eq.i32($i23, 0); + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + assume {:branchcond $i24} true; + goto $bb24, $bb26; +$bb24: + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + assume ($i24 == 1); + goto $bb25; +$bb25: + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + goto $bb27; +$bb26: + assume !(($i24 == 1)); + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 1} true; + call __VERIFIER_assert(0); + assume {:sourceloc "two_arrays.c", 47, 5} true; + assume {:verifier.code 0} true; + goto $bb25; +$bb27: + assume {:sourceloc "two_arrays.c", 48, 3} true; + assume {:verifier.code 0} true; + goto $bb28; +$bb28: + assume {:sourceloc "two_arrays.c", 45, 29} true; + assume {:verifier.code 0} true; + $i25 := $add.i32($i15, 1); + call {:cexpr "i"} boogie_si_record_i32($i25); + assume {:sourceloc "two_arrays.c", 45, 3} true; + assume {:verifier.code 0} true; + $i15 := $i25; + goto $bb15; +} +const malloc: ref; +axiom (malloc == $sub.ref(0, 9291)); +procedure {:inline 11} malloc($i0: i64) + returns ($r: ref) +{ + call $r := $malloc($i0); +} +const free_: ref; +axiom (free_ == $sub.ref(0, 10323)); +procedure {:inline 11} free_($p0: ref) +{ + call $free($p0); +} +const __VERIFIER_assume: ref; +axiom (__VERIFIER_assume == $sub.ref(0, 11355)); +procedure {:inline 11} __VERIFIER_assume($i0: i32) +{ +$bb0: + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 29} true; + assume {:verifier.code 1} true; + call {:cexpr "__VERIFIER_assume:arg:x"} boogie_si_record_i32($i0); + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 29} true; + assume {:verifier.code 1} true; + assume true; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 38, 3} true; + assume {:verifier.code 1} true; + assume $i0 != $0; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 39, 1} true; + assume {:verifier.code 0} true; + $exn := false; + return; +} +const __SMACK_code: ref; +axiom (__SMACK_code == $sub.ref(0, 12387)); +procedure {:inline 11} __SMACK_code.ref($p0: ref); +procedure {:inline 11} __SMACK_code.ref.i32($p0: ref, p.1: i32); +const __SMACK_dummy: ref; +axiom (__SMACK_dummy == $sub.ref(0, 13419)); +procedure {:inline 11} __SMACK_dummy($i0: i32) +{ +$bb0: + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 29} true; + assume {:verifier.code 1} true; + call {:cexpr "__SMACK_dummy:arg:v"} boogie_si_record_i32($i0); + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 29} true; + assume {:verifier.code 1} true; + assume true; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 59} true; + assume {:verifier.code 0} true; + $exn := false; + return; +} +const __VERIFIER_assert: ref; +axiom (__VERIFIER_assert == $sub.ref(0, 14451)); +procedure {:inline 11} __VERIFIER_assert($i0: i32) +{ +$bb0: + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 29} true; + assume {:verifier.code 1} true; + call {:cexpr "__VERIFIER_assert:arg:x"} boogie_si_record_i32($i0); + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 29} true; + assume {:verifier.code 1} true; + assume true; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 45, 3} true; + assume {:verifier.code 1} true; + assert $i0 != $0; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 47, 1} true; + assume {:verifier.code 0} true; + $exn := false; + return; +} +const __SMACK_check_overflow: ref; +axiom (__SMACK_check_overflow == $sub.ref(0, 15483)); +procedure {:inline 11} __SMACK_check_overflow($i0: i32) +{ +$bb0: + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 29} true; + assume {:verifier.code 1} true; + call {:cexpr "__SMACK_check_overflow:arg:flag"} boogie_si_record_i32($i0); + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 258, 29} true; + assume {:verifier.code 1} true; + assume true; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 63, 3} true; + assume {:verifier.code 1} true; + assert {:overflow} $i0 == $0; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 64, 1} true; + assume {:verifier.code 0} true; + $exn := false; + return; +} +const __SMACK_nondet_char: ref; +axiom (__SMACK_nondet_char == $sub.ref(0, 16515)); +procedure {:inline 11} __SMACK_nondet_char() + returns ($r: i8); +const __SMACK_nondet_signed_char: ref; +axiom (__SMACK_nondet_signed_char == $sub.ref(0, 17547)); +procedure {:inline 11} __SMACK_nondet_signed_char() + returns ($r: i8); +const __SMACK_nondet_unsigned_char: ref; +axiom (__SMACK_nondet_unsigned_char == $sub.ref(0, 18579)); +procedure {:inline 11} __SMACK_nondet_unsigned_char() + returns ($r: i8); +const __SMACK_nondet_short: ref; +axiom (__SMACK_nondet_short == $sub.ref(0, 19611)); +procedure {:inline 11} __SMACK_nondet_short() + returns ($r: i16); +const __SMACK_nondet_signed_short: ref; +axiom (__SMACK_nondet_signed_short == $sub.ref(0, 20643)); +procedure {:inline 11} __SMACK_nondet_signed_short() + returns ($r: i16); +const __SMACK_nondet_signed_short_int: ref; +axiom (__SMACK_nondet_signed_short_int == $sub.ref(0, 21675)); +procedure {:inline 11} __SMACK_nondet_signed_short_int() + returns ($r: i16); +const __SMACK_nondet_unsigned_short: ref; +axiom (__SMACK_nondet_unsigned_short == $sub.ref(0, 22707)); +procedure {:inline 11} __SMACK_nondet_unsigned_short() + returns ($r: i16); +const __SMACK_nondet_unsigned_short_int: ref; +axiom (__SMACK_nondet_unsigned_short_int == $sub.ref(0, 23739)); +procedure {:inline 11} __SMACK_nondet_unsigned_short_int() + returns ($r: i16); +const __SMACK_nondet_int: ref; +axiom (__SMACK_nondet_int == $sub.ref(0, 24771)); +procedure {:inline 11} __SMACK_nondet_int() + returns ($r: i32); +const __SMACK_nondet_signed_int: ref; +axiom (__SMACK_nondet_signed_int == $sub.ref(0, 25803)); +procedure {:inline 11} __SMACK_nondet_signed_int() + returns ($r: i32); +const __SMACK_nondet_unsigned: ref; +axiom (__SMACK_nondet_unsigned == $sub.ref(0, 26835)); +procedure {:inline 11} __SMACK_nondet_unsigned() + returns ($r: i32); +const __SMACK_nondet_unsigned_int: ref; +axiom (__SMACK_nondet_unsigned_int == $sub.ref(0, 27867)); +procedure {:inline 11} __SMACK_nondet_unsigned_int() + returns ($r: i32); +const __SMACK_nondet_long: ref; +axiom (__SMACK_nondet_long == $sub.ref(0, 28899)); +procedure {:inline 11} __SMACK_nondet_long() + returns ($r: i64); +const __SMACK_nondet_long_int: ref; +axiom (__SMACK_nondet_long_int == $sub.ref(0, 29931)); +procedure {:inline 11} __SMACK_nondet_long_int() + returns ($r: i64); +const __SMACK_nondet_signed_long: ref; +axiom (__SMACK_nondet_signed_long == $sub.ref(0, 30963)); +procedure {:inline 11} __SMACK_nondet_signed_long() + returns ($r: i64); +const __SMACK_nondet_signed_long_int: ref; +axiom (__SMACK_nondet_signed_long_int == $sub.ref(0, 31995)); +procedure {:inline 11} __SMACK_nondet_signed_long_int() + returns ($r: i64); +const __SMACK_nondet_unsigned_long: ref; +axiom (__SMACK_nondet_unsigned_long == $sub.ref(0, 33027)); +procedure {:inline 11} __SMACK_nondet_unsigned_long() + returns ($r: i64); +const __SMACK_nondet_unsigned_long_int: ref; +axiom (__SMACK_nondet_unsigned_long_int == $sub.ref(0, 34059)); +procedure {:inline 11} __SMACK_nondet_unsigned_long_int() + returns ($r: i64); +const __SMACK_nondet_long_long: ref; +axiom (__SMACK_nondet_long_long == $sub.ref(0, 35091)); +procedure {:inline 11} __SMACK_nondet_long_long() + returns ($r: i64); +const __SMACK_nondet_long_long_int: ref; +axiom (__SMACK_nondet_long_long_int == $sub.ref(0, 36123)); +procedure {:inline 11} __SMACK_nondet_long_long_int() + returns ($r: i64); +const __SMACK_nondet_signed_long_long: ref; +axiom (__SMACK_nondet_signed_long_long == $sub.ref(0, 37155)); +procedure {:inline 11} __SMACK_nondet_signed_long_long() + returns ($r: i64); +const __SMACK_nondet_signed_long_long_int: ref; +axiom (__SMACK_nondet_signed_long_long_int == $sub.ref(0, 38187)); +procedure {:inline 11} __SMACK_nondet_signed_long_long_int() + returns ($r: i64); +const __SMACK_nondet_unsigned_long_long: ref; +axiom (__SMACK_nondet_unsigned_long_long == $sub.ref(0, 39219)); +procedure {:inline 11} __SMACK_nondet_unsigned_long_long() + returns ($r: i64); +const __SMACK_nondet_unsigned_long_long_int: ref; +axiom (__SMACK_nondet_unsigned_long_long_int == $sub.ref(0, 40251)); +procedure {:inline 11} __SMACK_nondet_unsigned_long_long_int() + returns ($r: i64); +const __SMACK_decls: ref; +axiom (__SMACK_decls == $sub.ref(0, 41283)); +type $mop; +procedure {:inline 11} boogie_si_record_mop(m: $mop); +const $MOP: $mop; +var $exn: bool; +var $exnv: int; +procedure {:inline 11} corral_atomic_begin(); +procedure {:inline 11} corral_atomic_end(); +procedure {:inline 11} $alloc(n: ref) returns (p: ref) +{ + call corral_atomic_begin(); + call p := $$alloc(n); + call corral_atomic_end(); +} + +procedure {:inline 11} $malloc(n: ref) returns (p: ref) +{ + call corral_atomic_begin(); + call p := $$alloc(n); + call corral_atomic_end(); +} + +var $CurrAddr:ref; + +procedure {:inline 1} $$alloc(n: ref) returns (p: ref) +modifies $CurrAddr; +{ + assume $sge.ref.bool(n, $0.ref); + if ($sgt.ref.bool(n, $0.ref)) { + p := $CurrAddr; + havoc $CurrAddr; + assume $sge.ref.bool($sub.ref($CurrAddr, n), p); + assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, $MALLOC_TOP); + } else { + p := $0.ref; + } +} + +procedure {:inline 11} $free(p: ref); + +const __SMACK_top_decl: ref; +axiom (__SMACK_top_decl == $sub.ref(0, 42315)); +procedure {:inline 11} __SMACK_top_decl.ref($p0: ref); +const __SMACK_init_func_memory_model: ref; +axiom (__SMACK_init_func_memory_model == $sub.ref(0, 43347)); +procedure {:inline 11} __SMACK_init_func_memory_model() +{ +$bb0: + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 539, 3} true; + assume {:verifier.code 1} true; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 539, 3} true; + assume {:verifier.code 1} true; + $CurrAddr := $1024.ref; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 544, 1} true; + assume {:verifier.code 0} true; + $exn := false; + return; +} +const __VERIFIER_atomic_begin: ref; +axiom (__VERIFIER_atomic_begin == $sub.ref(0, 44379)); +procedure {:inline 11} __VERIFIER_atomic_begin() +{ +$bb0: + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 546, 34} true; + assume {:verifier.code 1} true; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 546, 34} true; + assume {:verifier.code 1} true; + call corral_atomic_begin(); + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 546, 79} true; + assume {:verifier.code 0} true; + $exn := false; + return; +} +const __VERIFIER_atomic_end: ref; +axiom (__VERIFIER_atomic_end == $sub.ref(0, 45411)); +procedure {:inline 11} __VERIFIER_atomic_end() +{ +$bb0: + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 548, 32} true; + assume {:verifier.code 1} true; + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 548, 32} true; + assume {:verifier.code 1} true; + call corral_atomic_end(); + assume {:sourceloc "/usr/local/share/smack/lib/smack.c", 548, 75} true; + assume {:verifier.code 0} true; + $exn := false; + return; +} +const llvm.dbg.value: ref; +axiom (llvm.dbg.value == $sub.ref(0, 46443)); +procedure {:inline 11} llvm.dbg.value($p0: ref, $p1: ref, $p2: ref); +const __SMACK_static_init: ref; +axiom (__SMACK_static_init == $sub.ref(0, 47475)); +procedure {:inline 11} __SMACK_static_init() +{ +$bb0: + $M.1 := .str.1.3; + $M.2 := 0; + call {:cexpr "errno_global"} boogie_si_record_i32(0); + $exn := false; + return; +} +procedure {:inline 11} boogie_si_record_i32(x: i32); +procedure {:inline 11} boogie_si_record_ref(x: ref); +procedure {:inline 11} $initialize() +{ + call __SMACK_static_init(); + call __SMACK_init_func_memory_model(); + return; +} diff --git a/Test/smack/git-issue-203-define.bpl.expect b/Test/smack/git-issue-203-define.bpl.expect new file mode 100644 index 000000000..37fad75c9 --- /dev/null +++ b/Test/smack/git-issue-203-define.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors