< Summary

Class:NanoCLang.NanoCSMT
Assembly:NanoCLang
File(s):C:\GitLab-Runner\builds\JxAESPd8\0\chenmichael\nanoc\src\NanoCLang\NanoCSMT.cs
Covered lines:74
Uncovered lines:11
Coverable lines:85
Total lines:175
Line coverage:87% (74 of 85)
Covered branches:21
Total branches:28
Branch coverage:75% (21 of 28)

Metrics

MethodBranch coverage Cyclomatic complexity Line coverage
get_Default()100%1100%
get_Context()100%1100%
get_InvocationCount()100%1100%
.ctor()100%1100%
IndicesCollide(...)75%492.3%
TryEvalConstExpression(...)77.77%1884.61%
Scoped(...)100%1100%
ValidImplication(...)66.66%686.66%
InvokeSolver(...)100%1100%
Dispose()100%10%
PAdd(...)100%1100%
BLen(...)100%1100%
Safe(...)100%1100%
SafeN(...)100%1100%
BS(...)100%1100%
BE(...)100%1100%

File(s)

C:\GitLab-Runner\builds\JxAESPd8\0\chenmichael\nanoc\src\NanoCLang\NanoCSMT.cs

#LineLine coverage
 1using Microsoft.Z3;
 2using NanoCLang.Entities;
 3using NanoCLang.Environemnts;
 4using System;
 5using System.Linq;
 6
 7namespace NanoCLang {
 8    /// <summary>
 9    /// Provides a class for validating subtyping refinements using an SMT solver.
 10    /// </summary>
 11    public class NanoCSMT : IDisposable {
 12        /// <summary>
 13        /// Gets the default instance of the NanoC SMT solver.
 14        /// </summary>
 16515        public static NanoCSMT Default { get; } = new NanoCSMT();
 16        /// <summary>
 17        /// Gets the currently used instance of the SMT context.
 18        /// </summary>
 438319        public Context Context { get; }
 20        /// <summary>
 21        /// Gets the number of SMT solver invocations of this solver instance.
 22        /// </summary>
 34723        public int InvocationCount { get; private set; } = 0;
 24        private readonly Solver solver;
 25        private readonly FuncDecl _bs;
 26        private readonly FuncDecl _be;
 27        /// <summary>
 28        /// Creates a new instance of the NanoC SMT solver.
 29        /// </summary>
 230        private NanoCSMT() {
 131            Context = new Context();
 132            solver = Context.MkSolver("QF_LIA");
 133            _bs = Context.MkFuncDecl(Context.MkSymbol("BS"), Context.IntSort, Context.IntSort);
 134            _be = Context.MkFuncDecl(Context.MkSymbol("BE"), Context.IntSort, Context.IntSort);
 135        }
 36        /// <inheritdoc cref="Entities.Index.CollidesWith(int, Entities.Index, int)"/>
 4437        public bool IndicesCollide(Entities.Index index1, int size, Entities.Index index2, int otherSize) => Scoped(solv
 2238            (var guard1, var value1) = index1.SMTPossibleValues(this, size, "l_");
 2239            (var guard2, var value2) = index2.SMTPossibleValues(this, otherSize, "r_");
 2240            solver.Assert(guard1, guard2, Context.MkEq(value1, value2));
 2241            VerbConsole.WriteLine(VerbosityLevel.Default, "Solving: {0} with type {1} collides {2} with type {3}!", inde
 2242            switch (InvokeSolver(solver)) {
 1043            case Status.UNSATISFIABLE: return false;
 2244            case Status.SATISFIABLE:
 1245                VerbConsole.WriteLine(VerbosityLevel.Default, "Bad: Indices collide at offset {0}!", solver.Model.Eval(v
 1246                return true;
 047            default: throw new IllFormedException(index1, $"Cannot determine index collision with fallback SMT solver!")
 2248            }
 4449        });
 50        /// <summary>
 51        /// Invokes the SMT solver to solve if the expression is always truthy.
 52        /// </summary>
 53        /// <param name="gamma">Current environment.</param>
 54        /// <param name="exp">Antecedent of the implication.</param>
 55        /// <returns>Boolean value that represents the value of the expression or <see langword="null"/> if the expressi
 4256        public bool? TryEvalConstExpression(LocalEnvironment gamma, PureExpression exp) => Scoped(solver => {
 2157            if (gamma.Count > 0)
 1758                solver.Assert(gamma.ToBoolean(this));
 4259            return Scoped(solver => {
 2160                solver.Assert(!exp.ToBoolean(gamma, this));
 2161                VerbConsole.WriteLine(VerbosityLevel.Default, "Solving: {0} always true\n{1}", exp, solver);
 2162                switch (InvokeSolver(solver)) {
 1263                case Status.UNSATISFIABLE: return true;
 064                case Status.UNKNOWN: return false;
 965                case Status.SATISFIABLE: return false;
 066                default: throw new IllFormedException(exp, $"Unexpected status in SMT solver!");
 2167                }
 2168            })
 2169                ? true
 970                : Scoped(solver => {
 971                    solver.Assert(exp.ToBoolean(gamma, this));
 972                    VerbConsole.WriteLine(VerbosityLevel.Default, "Solving: {0} always false\n{1}", exp, solver);
 973                    switch (InvokeSolver(solver)) {
 474                    case Status.UNSATISFIABLE: return true;
 075                    case Status.UNKNOWN: return false;
 576                    case Status.SATISFIABLE: return false;
 077                    default: throw new IllFormedException(exp, $"Unexpected status in SMT solver!");
 2178                    }
 979                }) ? false
 2180                   : (bool?)null;
 4281        });
 82        /// <summary>
 83        /// Safely pushes a solver scope and evaluates the function with the scoped solver.
 84        /// </summary>
 85        /// <typeparam name="T">Type of the return value to evaluate.</typeparam>
 86        /// <param name="p">Function to evaluate the return value with the solver.</param>
 87        /// <returns>Evaluated result inside the scope.</returns>
 19488        private T Scoped<T>(Func<Solver, T> p) {
 19489            solver.Push();
 19490            try {
 19491                return p(solver);
 19492            } finally {
 19493                solver.Pop();
 19494            }
 19495        }
 96        /// <summary>
 97        /// Invokes the SMT solver to solve Valid([gamma] and [a1] implies [a2]).
 98        /// This checks if <paramref name="a1"/> implies that <paramref name="a2"/> holds given the environment <paramre
 99        /// </summary>
 100        /// <param name="gamma">Current environment.</param>
 101        /// <param name="a1">Antecedent of the implication.</param>
 102        /// <param name="a2">Consequent of the implication.</param>
 103        /// <returns><see langword="true"/> iff the implication holds, otherwise <see langword="false"/>.</returns>
 104        /// <exception cref="IllFormedException">Solver is unable to check if the implication holds.</exception>
 242105        public bool ValidImplication(LocalEnvironment gamma, PureExpression a1, PureExpression a2) => Scoped(solver => {
 121106            VerbConsole.WriteLine(VerbosityLevel.Default, $"Checking implication {a1} => {a2}...");
 121107            if (gamma.Count > 0)
 121108                solver.Assert(gamma.ToBoolean(this));
 121109            solver.Assert(!Context.MkImplies(a1.ToBoolean(gamma, this), a2.ToBoolean(gamma, this)));
 121110            VerbConsole.WriteLine(VerbosityLevel.Default, "Solving: {0}", solver);
 121111            switch (InvokeSolver(solver)) {
 109112            case Status.UNSATISFIABLE: return true;
 0113            case Status.UNKNOWN: throw new IllFormedException(a2, $"Refinement cannot be verified!");
 121114            case Status.SATISFIABLE:
 35115                VerbConsole.WriteLine(VerbosityLevel.Default, $"Subtyping broken for values:\n\t{string.Join("\n\t", sol
 12116                return false;
 0117            default: throw new IllFormedException(a2, $"Unexpected status in SMT solver!");
 121118            }
 242119        });
 120
 173121        private Status InvokeSolver(Solver solver) {
 173122            InvocationCount++;
 173123            return solver.Check();
 173124        }
 125
 126        /// <inheritdoc/>
 0127        public void Dispose() {
 0128            ((IDisposable)Context).Dispose();
 0129            ((IDisposable)solver).Dispose();
 0130        }
 131        #region Support functions
 132        /// <summary>
 133        /// Creates a new boolean expression that ensures the pointer <paramref name="v"/> is is correctly offset by <pa
 134        /// </summary>
 135        /// <param name="v">Initial pointer.</param>
 136        /// <param name="x">Other pointer in the same block.</param>
 137        /// <param name="i">Offset between the pointers.</param>
 138        /// <returns><see langword="true"/> expression iff the pointer is offset correctly.</returns>
 32139        public BoolExpr PAdd(IntExpr v, IntExpr x, ArithExpr i) => Context.MkAnd(Context.MkEq(v, x + i), Context.MkEq(BS
 140        /// <summary>
 141        /// Creates a new boolean expression that ensures that the pointer <paramref name="v"/> points to the start of a
 142        /// </summary>
 143        /// <param name="v">Start of the current block (index 0).</param>
 144        /// <param name="n">Length of the block in bytes.</param>
 145        /// <returns><see langword="true"/> expression iff the block has the given length and position.</returns>
 153146        public BoolExpr BLen(IntExpr v, ArithExpr n) => Context.MkAnd(Context.MkEq(BS(v), v), Context.MkEq(BE(v), v + n)
 147        /// <summary>
 148        /// Creates a new boolean expression that ensures that a pointer is safely within bounds of the current block.
 149        /// </summary>
 150        /// <param name="v">Pointer to check for memory safety.</param>
 151        /// <returns><see langword="true"/> expression iff the pointer is within safe bounds.</returns>
 159152        public BoolExpr Safe(IntExpr v) => Context.MkAnd(v > 0, BS(v) <= v, v < BE(v));
 153        /// <summary>
 154        /// Creates a new boolean expression that ensures that a pointer is safely within bounds of the current block an
 155        /// This is essentially equal to SafeN(v, n) &lt;=&gt; AND_{0 &lt;= i &lt;= n} Safe(v + i)
 156        /// </summary>
 157        /// <param name="v">Pointer to check for memory safety.</param>
 158        /// <param name="n">Length of the memory block in bytes.</param>
 159        /// <returns><see langword="true"/> expression iff the pointer and its block is within safe bounds.</returns>
 38160        internal BoolExpr SafeN(IntExpr v, IntExpr n) => Context.MkAnd(v > 0, BS(v) <= v, (v + n) <= BE(v));
 161        /// <summary>
 162        /// Creates a new integer expression that maps a pointer to the start of the block that it points to.
 163        /// </summary>
 164        /// <param name="v">Pointer in the same block.</param>
 165        /// <returns>Integer expression to the start of the block.</returns>
 414166        public IntExpr BS(IntExpr v) => (IntExpr)_bs[v];
 167        /// <summary>
 168        /// Creates a new integer expression that maps a pointer to the end (exclusive) of the block that it points to.
 169        /// </summary>
 170        /// <param name="v">Pointer in the same block.</param>
 171        /// <returns>Integer expression to the end (exclusive) of the block.</returns>
 414172        public IntExpr BE(IntExpr v) => (IntExpr)_be[v];
 173        #endregion
 174    }
 175}
Generated by: ReportGenerator 4.8.8.0
28/07/2021 - 23:15:07
GitHub | www.palmmedia.de

Methods/Properties

get_Default()
get_Context()
get_InvocationCount()
.ctor()
IndicesCollide(...)
TryEvalConstExpression(...)
Scoped(...)
ValidImplication(...)
InvokeSolver(...)
Dispose()
PAdd(...)
BLen(...)
Safe(...)
SafeN(...)
BS(...)
BE(...)