Improve trigonometric abstractions #1272

stilscher · 2023-11-23T13:39:08Z

This PR improves the abstraction of the cos function if the argument is neither nan nor inf by

storing also the inverted relationship between arguments of math functions and (assigned variable, math function) in the tmpSpecial analysis
being more precise in the abstraction of cos(x) in case one can assure that variables representing isInf(x) and isNaN are definitely false

michael-schwarz · 2023-11-23T15:21:23Z

This yields 4 more successful tasks, I'll start it on the server.

michael-schwarz · 2023-11-23T19:45:16Z

src/cdomains/floatDomain.ml

@@ -907,8 +929,16 @@ module FloatIntervalImplLifted = struct
  let acos = lift (F1.acos, F2.acos)
  let asin = lift (F1.asin, F2.asin)
  let atan = lift (F1.atan, F2.atan)
-  let cos = lift (F1.cos, F2.cos)
-  let sin = lift (F1.sin, F2.sin)
+  let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function


Suggested change

let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function

let cos ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) = function

BoolDomain.MustBool.top () is false.

michael-schwarz · 2023-11-23T19:46:01Z

src/cdomains/floatDomain.ml

+    | F64 a -> F64 (F2.cos ~asPreciseAsConcrete:true ~notInf_notNaN a)
+    | FLong a -> FLong (F2.cos ~notInf_notNaN a)
+    | FFloat128 a -> FFloat128 (F2.cos ~notInf_notNaN a)
+  let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function


Suggested change

let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function

let sin ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) = function

michael-schwarz · 2023-11-23T19:50:59Z

src/cdomains/floatDomain.ml

-    map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.cos); }
-  let sin =
-    map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sin); }
+  let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =


Suggested change

let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =

let cos ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) =

michael-schwarz · 2023-11-23T19:52:04Z

src/cdomains/floatDomain.ml

-    map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sin); }
+  let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =
+    map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.cos ~asPreciseAsConcrete ~notInf_notNaN); }
+  let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =


Suggested change

let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =

let sin ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) =

michael-schwarz · 2023-11-23T19:55:57Z

src/cdomains/floatDomain.ml

@@ -791,8 +791,30 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
  let acos = eval_unop eval_acos
  let asin = eval_unop eval_asin
  let atan = eval_unop eval_atan
-  let cos = eval_unop eval_cos
-  let sin = eval_unop eval_sin
+  let cos ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) op =


Seems like we should be able to get some reuse here for sin and cos.

michael-schwarz · 2023-11-23T20:02:59Z

src/analyses/base.ml

+                    let isNotNan = Q.MLInv.exists (fun (y, ml) -> matchnan ml && isFalse y) s in
+                    let isNotInf = Q.MLInv.exists (fun (y, ml) -> matchinf ml && isFalse y) s in
+                    isNotInf && isNotNan)


Might make sense to restructure so the lookup for isNotInf doesn't always happen.

michael-schwarz · 2023-11-23T20:05:30Z

src/analyses/base.ml

+                            match Queries.ID.to_bool v with
+                            | Some b -> not b
+                            | None -> false)


Suggested change

match Queries.ID.to_bool v with

| Some b -> not b

| None -> false)

Queries.ID.to_bool v = Some false)

michael-schwarz · 2023-11-23T20:09:29Z

src/analyses/base.ml

@@ -2355,6 +2355,40 @@ struct
          | _ -> failwith ("non-integer argument in call to function "^f.vname)
        end
      in
+      let apply_better_trig fk (float_fun : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> FD.t -> FD.t) x =


Is the type annotation needed, it looks a bit clunky.

Possibly, because the type inference of optional arguments is not principal: https://dev.realworldocaml.org/variables-and-functions.html#inference-of-labeled-and-optional-arguments.

michael-schwarz · 2023-11-23T20:14:39Z

src/analyses/tmpSpecial.ml

-          D.add (v, Offset.Exp.of_cil offs) ((ML.lift fun_args, Deps.of_list ((Lval lv)::arglist))) d
+        else (
+          if M.tracing then M.trace "tmpSpecialInv" "build tmpSpecial Entry for Lval %s\n" v.vname;
+          let d1 = MM.add (v, Offset.Exp.of_cil offs) ((ML.lift fun_args, Deps.of_list ((Lval lv)::arglist))) (fst d) in


I think some parens are unneeded here...

Also Deps.of_list ((Lval lv)::arglist)) is constructed twice here.

michael-schwarz · 2023-11-23T20:25:55Z

src/analyses/tmpSpecial.ml

+          let mlv = MInvEntrySet.fold (fun (v, ml, deps) acc -> Queries.MLInv.add (v,ml) acc) es (Queries.MLInv.empty ())
+                    |> Queries.MLInv.filter (fun (v,ml) ->
+                        match ml, v with
+                        | `Bot, _ -> false
+                        | _, `Lifted exp -> true
+                        | _ -> false) in


This way of doing looks as if it may be in a figure of speech potentially trying to achieve the goal in a way that might be described as roundabout. You might want to do the filtering right in place. 😉

michael-schwarz · 2023-11-23T20:36:44Z

src/analyses/tmpSpecial.ml

+
+  (* arg maps to (x, mathf(arg), deps) if x = mathf(arg) *)
+  module ExpFlat = Lattice.Flat (CilType.Exp) (Printable.DefaultNames)
+  module MInvEntry = Lattice.Prod3 (ExpFlat) (ML) (Deps)


Have you tried this type:

module MInvEntry = Printable.Prod3 (CilType.Exp) (LibraryDesc.MathPrintable) (SetDomain.Make(CilType.Exp))

Might make it easier on the inside to give up on the lattice structure that is unused anyway.

sim642 · 2023-11-24T08:15:44Z

Since this is still in need of refactoring/cleanup, it's too late to include for SV-COMP 2024. Four additional tasks out of ~32000 is not worth the risk for a possible regression.

michael-schwarz · 2023-11-24T08:35:43Z

Four additional tasks out of ~32000 is not worth the risk for a possible regression.

There is no regression, we ran it overnight on all tasks with full timeouts.

sim642 · 2023-11-24T09:26:35Z

It's not just about SV-COMP though. It will be the representative version of Goblint for the entire year to come. If something doesn't yet meet our own standards, then it's not ready for such release. This is just too last minute, considering the freezing deadline we set for ourselves.

michael-schwarz · 2023-11-24T09:29:27Z

Ok. I think it would've been nice for Sarah's work this past week to be reflected in that version, but I won't push too hard.

sim642 · 2023-11-27T12:45:37Z

Why is the TmpSpecialInv query needed? TmpSpecial itself already is a certain inverse (for refining the argument based on the return value), so TmpSpecialInv is some kind of inverse of the inverse. Is that not just normal forward evaluation? The new query is also used in eval not invariant.

sim642 · 2023-11-27T12:54:49Z

src/analyses/base.ml

+                    let matchinf = function
+                      | `Lifted LibraryDesc.Isnan _ -> true


Suggested change

let matchinf = function

| `Lifted LibraryDesc.Isnan _ -> true

let matchinf = function

| `Lifted LibraryDesc.Isinf _ -> true

stilscher added 6 commits November 23, 2023 14:15

better cos computation in case argument is neither inf nor nan

3087fff

fix headers in tests

a7265c8

add test case

fde7d4d

fix test

48d5f2a

improve sin as well

0107ce9

add regression test for sin

be4fdad

sim642 added feature precision labels Nov 23, 2023

michael-schwarz added this to the SV-COMP 2024 milestone Nov 23, 2023

michael-schwarz marked this pull request as ready for review November 23, 2023 15:21

sim642 self-requested a review November 23, 2023 18:40

michael-schwarz reviewed Nov 23, 2023

View reviewed changes

sim642 modified the milestones: SV-COMP 2024, v2.4.0 Nov 24, 2023

sim642 reviewed Nov 27, 2023

View reviewed changes

Merge branch 'master' into improve-trig

7784521

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve trigonometric abstractions #1272

Improve trigonometric abstractions #1272

stilscher commented Nov 23, 2023 •

edited by michael-schwarz

michael-schwarz commented Nov 23, 2023

michael-schwarz Nov 23, 2023 •

edited

michael-schwarz Nov 23, 2023 •

edited

michael-schwarz Nov 23, 2023

michael-schwarz Nov 23, 2023

michael-schwarz Nov 23, 2023

michael-schwarz Nov 23, 2023

michael-schwarz Nov 23, 2023 •

edited

michael-schwarz Nov 23, 2023

sim642 Nov 27, 2023

michael-schwarz Nov 23, 2023

michael-schwarz Nov 23, 2023

michael-schwarz Nov 23, 2023

michael-schwarz Nov 23, 2023

sim642 commented Nov 24, 2023

michael-schwarz commented Nov 24, 2023

sim642 commented Nov 24, 2023

michael-schwarz commented Nov 24, 2023

sim642 commented Nov 27, 2023

sim642 Nov 27, 2023

	let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function
	let cos ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) = function

	let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function
	let sin ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) = function

		let matchinf = function
		\| `Lifted LibraryDesc.Isnan _ -> true

Improve trigonometric abstractions #1272

Are you sure you want to change the base?

Improve trigonometric abstractions #1272

Conversation

stilscher commented Nov 23, 2023 • edited by michael-schwarz

michael-schwarz commented Nov 23, 2023

michael-schwarz Nov 23, 2023 • edited

Choose a reason for hiding this comment

michael-schwarz Nov 23, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

michael-schwarz Nov 23, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sim642 commented Nov 24, 2023

michael-schwarz commented Nov 24, 2023

sim642 commented Nov 24, 2023

michael-schwarz commented Nov 24, 2023

sim642 commented Nov 27, 2023

Choose a reason for hiding this comment

stilscher commented Nov 23, 2023 •

edited by michael-schwarz

michael-schwarz Nov 23, 2023 •

edited

michael-schwarz Nov 23, 2023 •

edited

michael-schwarz Nov 23, 2023 •

edited