Commit 521f4d70 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'master' into certification

parents 198b3cfc 1045a1af
......@@ -54,7 +54,7 @@ object SpecsProcessingPhase extends DaisyPhase {
// TODO: additional constraints
val (ranges, errors) = extractPreCondition(pre)
allRanges += (fnc.id -> ranges.mapValues( x => Interval(x._1, x._2) ))
allRanges += (fnc.id -> ranges.map( x => (x._1 -> Interval(x._2._1, x._2._2) )))
allErrors += (fnc.id -> errors)
// annotate the variables in the function body directly
......@@ -82,7 +82,8 @@ object SpecsProcessingPhase extends DaisyPhase {
case Some(post) =>
val (ranges, errors) = extractPostCondition(post)
requiredOutputRanges += (fnc.id -> ranges.mapValues( x => PartialInterval(x._1, x._2) ))
requiredOutputRanges += (fnc.id -> ranges.map( x =>
(x._1 -> PartialInterval(x._2._1, x._2._2) )))
requiredOutputErrors += (fnc.id -> errors)
case _ =>
......
......@@ -73,7 +73,7 @@ trait ErrorFunctions {
val (_, error) = evaluate[Interval, AffineForm](
expr,
inputValMap,
inputErrorMap.mapValues(AffineForm.fromError(_)),
inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
Interval.apply,
AffineForm.zero,
AffineForm.fromError,
......@@ -99,8 +99,8 @@ trait ErrorFunctions {
inputErrorMap: Map[Identifier, Rational]): Rational = {
val (_, error) = evaluate[AffineForm, AffineForm](
expr,
inputValMap.mapValues(AffineForm(_)),
inputErrorMap.mapValues(AffineForm.fromError(_)),
inputValMap.map(x => (x._1 -> AffineForm(x._2))),
inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
AffineForm.apply,
AffineForm.zero,
AffineForm.fromError,
......@@ -127,7 +127,7 @@ trait ErrorFunctions {
val (_, error) = evaluate[SMTRange, AffineForm](
expr,
inputValMap.map({ case (id, int) => (id -> SMTRange(Variable(id), int)) }),
inputErrorMap.mapValues(AffineForm.fromError(_)),
inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
SMTRange.apply,
AffineForm.zero,
AffineForm.fromError,
......@@ -517,7 +517,7 @@ trait ErrorFunctions {
val (resInterval, resError) = evaluate[Interval, AffineForm](
expr, inputsSubdiv.head,
getInputErrors(inputsSubdiv.head).mapValues(AffineForm.fromError(_)),
getInputErrors(inputsSubdiv.head).map(x => (x._1 -> AffineForm.fromError(x._2))),
Interval.apply, AffineForm.zero, AffineForm.fromError, AffineForm.apply,
false, trackRoundoffErrs, uniformPrecision)
......@@ -528,7 +528,7 @@ trait ErrorFunctions {
val (tmpRange, tmpError) = evaluate[Interval, AffineForm](
expr, m,
getInputErrors(m).mapValues(AffineForm.fromError(_)),
getInputErrors(m).map(x => (x._1 -> AffineForm.fromError(x._2))),
Interval.apply, AffineForm.zero, AffineForm.fromError, AffineForm.apply,
false, trackRoundoffErrs, uniformPrecision)
......@@ -766,7 +766,7 @@ trait ErrorFunctions {
attachInterval(expr)
// Now that we have the ranges, we can compute the errors
val resError = computeAndAttachError(expr, varErrorMap.mapValues(AffineForm.fromError(_)))
val resError = computeAndAttachError(expr, varErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))))
(currentRanges(expr), maxAbs(resError.toInterval))
}
......
......@@ -31,10 +31,10 @@ class RangeRegressionTest extends FunSuite {
for (fnc <- inputPrg.defs) if (!fnc.precondition.isEmpty && !fnc.body.isEmpty) {
val (ranges, errors) = analysis.SpecsProcessingPhase.extractPreCondition(fnc.precondition.get)
val inputRanges = ranges.mapValues( x => Interval(x._1, x._2) )
val inputRanges = ranges.map( x => (x._1 -> Interval(x._2._1, x._2._2)))
val affineRange = utils.Evaluators.evalAffine(fnc.body.get,
inputRanges.mapValues(AffineForm(_)))
inputRanges.map(x => (x._1 -> AffineForm(x._2))))
val intervalRange = utils.Evaluators.evalInterval(fnc.body.get,
inputRanges)
val smtRange = utils.Evaluators.evalSMT(fnc.body.get,
......
import daisy.lang._
import Real._
// Finds the arc length over the following function over the interval (0, pi)
// g(x) = x + \sum_{1 \leq k \leq 5} 2^{-k}\sin{2^{k}x}
object ArcLength {
def arcLength(z: Real): Real = {
require (100 <= z && z <= 103)
val main_i: Real = 1
// Precimonious paper used main_n as 1000000, but this leads to a divide-by-zero exception in daisy
val main_n: Real = 1000
val main_dppi: Real = 3.14159;
val main_s1_0: Real = 0.0;
val main_t1_0: Real = 0.0;
val main_h: Real = main_dppi / main_n;
// Iteration `main_i` of main loop
// One call to fun(i*h)
val x: Real = main_i * main_h
val t1_0: Real = x;
val d1_0: Real = 1.0;
// Iteration 1
val d1_1: Real = 2.0 * d1_0;
// Note: Uses small angle approximation. Originally sin(d1_1 * x), now (d1_1 * x)
val t1_1: Real = t1_0 + (d1_1 * x) / d1_1;
// Iteration 2
val d1_2: Real = 2.0 * d1_1;
val t1_2: Real = t1_1 + (d1_2 * x) / d1_2;
// Iteration 3
val d1_3: Real = 2.0 * d1_2;
val t1_3: Real = t1_2 + (d1_3 * x) / d1_3;
// Iteration 4
val d1_4: Real = 2.0 * d1_3;
val t1_4: Real = t1_3 + (d1_4 * x) / d1_4;
// Iteration 5
val d1_5: Real = 2.0 * d1_4;
val t1_5: Real = t1_4 + (d1_5 * x) / d1_5;
// Storing result of fun(i*h)
val main_t2: Real = (t1_5);
val main_s1_1: Real = main_s1_0 + sqrt(main_h*main_h + (main_t2 - main_t1_0)*(main_t2 - main_t1_0));
val main_t1_1: Real = main_t2;
// End of Iteration `main_i` of main loop
(main_s1_1)
} ensuring (res => res +/- 1e-14)
/*def fun(x: Real): Real = {
val t1_0: Real = x;
val d1_0: Real = 1.0;
// Iteration 1
val d1_1: Real = 2.0 * d1_0;
val t1_1: Real = t1_0 + sin(d1_1 * x) / d1_1;
// Iteration 2
val d1_2: Real = 2.0 * d1_1;
val t1_2: Real = t1_1 + sin(d1_2 * x) / d1_2;
// Iteration 3
val d1_3: Real = 2.0 * d1_2;
val t1_3: Real = t1_2 + sin(d1_3 * x) / d1_3;
// Iteration 4
val d1_4: Real = 2.0 * d1_3;
val t1_4: Real = t1_3 + sin(d1_4 * x) / d1_4;
// Iteration 5
val d1_5: Real = 2.0 * d1_4;
val t1_5: Real = t1_4 + sin(d1_5 * x) / d1_5;
(t1_5);
}*/
}
import daisy.lang._
import Real._
/*
Quadratic example from Goldberg's paper.
*/
object Quadratic {
def textBookQuadratic1(a: Real, b: Real, c: Real): Real = {
val discr = b*b - a * c * 4.0
val r1 = (-b - sqrt(discr))/(a * 2.0)
r1
}
def textBookQuadratic2(a: Real, b: Real, c: Real): Real = {
val discr = b*b - a * c * 4.0
val r2 = (-b + sqrt(discr))/(a * 2.0)
r2
}
def improvedQuadratic1(a: Real, b: Real, c: Real): Real = {
if(b*b - a*c > 10.0) {
if(b > 0.0) (-b - sqrt(discr))/(a * 2.0)
else if(b < 0.0) c * 2.0 /(-b + sqrt(discr))
else (-b - sqrt(discr))/(a * 2.0)
}
else {
(-b - sqrt(discr))/(a * 2.0)
}
}
def improvedQuadratic1(a: Real, b: Real, c: Real): Real = {
if(b*b - a*c > 10.0) {
if(b > 0.0) c * 2.0 /(-b - sqrt(discr))
else if(b < 0.0) (-b + sqrt(discr))/(a * 2.0)
else (-b + sqrt(discr))/(a * 2.0)
}
else {
(-b + sqrt(discr))/(a * 2.0)
}
}
// def improvedQuadratic(a: Real, b: Real, c: Real): Real = {
// if(b*b - a*c > 10.0) {
// if(b > 0.0) ((-b - sqrt(discr))/(a * 2.0), c * 2.0 /(-b - sqrt(discr)))
// else if(b < 0.0) (c * 2.0 /(-b + sqrt(discr)), (-b + sqrt(discr))/(a * 2.0))
// else ((-b - sqrt(discr))/(a * 2.0), (-b + sqrt(discr))/(a * 2.0))
// }
// else {
// ((-b - sqrt(discr))/(a * 2.0), (-b + sqrt(discr))/(a * 2.0))
// }
// }
}
\ No newline at end of file
import daisy.lang._
import Real._
/*
The famous formula for computing the area of a triangle.
*/
object Triangle {
def triangleUnstable(a: Real, b: Real, c: Real): Real = {
// TODO: this precondition can only be handled with SMT, and only
// if we add the usage of the additional constraints
//require(1 < a && a < 9 && 1 < b && b < 9 && 1 < c && c < 9 &&
// a + b > c + 0.000001 && a + c > b + 0.000001 && b + c > a + 0.000001)
require(4 <= a && a <= 5 && 4 <= b && b <= 4 && 4 <= c && c <= 5)
val s = (a + b + c)/2.0
sqrt(s * (s - a) * (s - b) * (s - c))
} ensuring (res => res >= 0.0 && res +/- 2e-9)
// def triangleKahan(aa: Real, bb: Real, cc: Real): Real = {
// var a = aa
// var b = bb
// var c = cc
// if(b < a) {
// val t = a
// if(c < b) {
// a = c; c = t
// }
// else {
// if(c < a) {
// a = b; b = c; c = t
// }
// else {
// a = b; b = t
// }
// }
// }
// else if(c < b) {
// val t = c; c = b;
// if(c < a) {
// b = a; a = t
// }
// else {
// b = t
// }
// }
// sqrt((a+(b+c)) * (c-(a-b)) * (c+(a-b)) * (a+(b-c))) / 4.0
// }
}
\ No newline at end of file
import daisy.lang._
import Real._
// LeadLag - Lead-lag compensator
// System of a single mass and a single spring, and is governed by an automatically synthesized controller.
// Tries to move the mass from the initial position y to the desired one yd.
// Taken from: Intra-procedural optimization of the numerical accuracy of programs
object LeadLag {
def leadLag(y: Real): Real = {
require(2.1 <= y && y <= 17.9)
val xc0: Real = 0.0
val xc1: Real = 0.0
val t: Real = 0.0
val yd: Real = 5.0
val Ac00: Real = 0.499
val Ac01: Real = -0.05
val Ac10: Real = 0.01
val Ac11: Real = 1.0
val Bc0: Real = 1.0
val Bc1: Real = 0.0
val Cc0: Real = 564.48
val Cc1: Real = 0.0
val Dc: Real = -1280.0
// Iteration 1
val yc_1: Real = 1.0
val xc0_1: Real = (Ac00*xc0)+(Ac01*xc1)+(Bc0*yc_1)
val xc1_1: Real = (Ac10*xc0_1)+(Ac11*xc1)+(Bc1*yc_1)
val u_1: Real = (Cc0* xc0_1)+(Cc1* xc1_1)+(Dc* yc_1)
val t_1: Real = (t + 0.1)
// Iteration 2
val yc_2: Real = -1.0
val xc0_2: Real = (Ac00*xc0_1)+(Ac01*xc1_1)+(Bc0*yc_2)
val xc1_2: Real = (Ac10*xc0_2)+(Ac11*xc1_1)+(Bc1*yc_2)
val u_2: Real = (Cc0* xc0_2)+(Cc1* xc1_2)+(Dc* yc_2)
val t_2: Real = (t_1 + 0.1)
// Iteration 3
val yc_3: Real = 1.0
val xc0_3: Real = (Ac00*xc0_2)+(Ac01*xc1_2)+(Bc0*yc_3)
val xc1_3: Real = (Ac10*xc0_3)+(Ac11*xc1_2)+(Bc1*yc_3)
val u_3: Real = (Cc0* xc0_3)+(Cc1* xc1_3)+(Dc* yc_3)
val t_3: Real = (t_2 + 0.1)
// Iteration 4
val yc_4: Real = -1.0
val xc0_4: Real = (Ac00*xc0_3)+(Ac01*xc1_3)+(Bc0*yc_4)
val xc1_4: Real = (Ac10*xc0_4)+(Ac11*xc1_3)+(Bc1*yc_4)
val u_4: Real = (Cc0* xc0_4)+(Cc1* xc1_4)+(Dc* yc_4)
val t_4: Real = (t_3 + 0.1)
(xc1_4)
} ensuring (res => res +/- 1e-07)
}
import daisy.lang._
import Real._
//Rocket Trajectory: Compute the trajectory of a rocket around the earth.
//Inputs: Mass Mf; Acceleration A
//Output: x and y co-ordinates of the rocket.
//Reference Paper: Optimizing the accuracy of a rocket trajectory simulation by program transformation
object Rocket {
def rocket_x_position(Mf: Real, A: Real) : Real = {
require(149999.0 <= Mf && Mf <= 150000.0)
require(139.0 <= A && A <= 140.0)
val R: Real = 6400000.0
val G: Real = 0.0000000000667428
val Mt: Real = 5973600000000000000000000.0
val dt: Real = 0.1
val T: Real = 24.0 * 3600.0
val nombrepas: Real = T / dt
val r0: Real = R + (400.0 * 10000)
val vr0: Real = 0.0
val teta0: Real = 0.0
val viss: Real = sqrt ( (G * Mt) / r0)
val vteta0: Real = viss / r0
val rf: Real = R
val vrf: Real = 0.0
val tetaf: Real = 0.0
val vl: Real = sqrt ( (G * Mt) / R)
val vlrad: Real = vl / r0
val vtetaf: Real = 1.1 * vlrad
val u1_im1: Real = r0
val u2_im1: Real = vr0
val u3_im1: Real = teta0
val u4_im1: Real = vteta0
val w1_im1: Real = rf
val w2_im1: Real = vrf
val w3_im1: Real = tetaf
val w4_im1: Real = vtetaf
val i: Real = 1.0
val mf_im1: Real = Mf
val t_im1: Real = 0.0
if (mf_im1 > 0.0){
val u1_i: Real = (u2_im1 * dt) + u1_im1
val u3_i: Real = (u4_im1 * dt) + u3_im1
val w1_i: Real = (w2_im1 * dt) + w1_im1
val w3_i: Real = (w4_im1 * dt) + w3_im1
val u2_i: Real = -G * Mt / (u1_im1 * u1_im1) * dt + u1_im1 * u4_im1 * u4_im1 * dt + u2_im1
val u4_i: Real = -2.0 * u2_im1 * u4_im1 / u1_im1 * dt + u4_im1
val w2_i: Real = - G * Mt /(w1_im1 * w1_im1) * dt + w1_im1 * w4_im1 * w4_im1 * dt
val w4_i: Real = -2.0 * w2_im1 * w4_im1 / w1_im1 * dt + A * w4_im1 / (Mf - A * t_im1) * dt + w4_im1
val mf_i: Real = mf_im1 - A * t_im1
val t_i: Real = t_im1 + dt
}
val c: Real = (1.0 - ((u3_i * u3_i)) * 0.5) + ((((u3_i * u3_i)* u3_i)* u3_i) / 24.0)
val x: Real = u1_i * c
(x)
}
def rocket_y_position(Mf: Real, A: Real) : Real = {
require(149999.0 <= Mf && Mf <= 150000.0)
require(139.0 <= A && A <= 140.0)
val R: Real = 6400000.0
val G: Real = 0.0000000000667428
val Mt: Real = 5973600000000000000000000.0
val dt: Real = 0.1
val T: Real = 24.0 * 3600.0
val nombrepas: Real = T / dt
val r0: Real = R + (400.0 * 10000)
val vr0: Real = 0.0
val teta0: Real = 0.0
val viss: Real = sqrt ( (G * Mt) / r0)
val vteta0: Real = viss / r0
val rf: Real = R
val vrf: Real = 0.0
val tetaf: Real = 0.0
val vl: Real = sqrt ( (G * Mt) / R)
val vlrad: Real = vl / r0
val vtetaf: Real = 1.1 * vlrad
val u1_im1: Real = r0
val u2_im1: Real = vr0
val u3_im1: Real = teta0
val u4_im1: Real = vteta0
val w1_im1: Real = rf
val w2_im1: Real = vrf
val w3_im1: Real = tetaf
val w4_im1: Real = vtetaf
val i: Real = 1.0
val mf_im1: Real = Mf
val t_im1: Real = 0.0
if (mf_im1 > 0.0){
val u1_i: Real = (u2_im1 * dt) + u1_im1
val u3_i: Real = (u4_im1 * dt) + u3_im1
val w1_i: Real = (w2_im1 * dt) + w1_im1
val w3_i: Real = (w4_im1 * dt) + w3_im1
val u2_i: Real = -G * Mt / (u1_im1 * u1_im1) * dt + u1_im1 * u4_im1 * u4_im1 * dt + u2_im1
val u4_i: Real = -2.0 * u2_im1 * u4_im1 / u1_im1 * dt + u4_im1
val w2_i: Real = - G * Mt /(w1_im1 * w1_im1) * dt + w1_im1 * w4_im1 * w4_im1 * dt
val w4_i: Real = -2.0 * w2_im1 * w4_im1 / w1_im1 * dt + A * w4_im1 / (Mf - A * t_im1) * dt + w4_im1
val mf_i: Real = mf_im1 - A * t_im1
val t_i: Real = t_im1 + dt
}
val s: Real = (arg - (((u3_i * u3_i)* u3_i)/6.0)) + (((((u3_i * u3_i)* u3_i)* u3_i)* u3_i)/120.0)
val y: Real = u1_i * s
(y)
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment