Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Temporary fix for generated code function selection, iFloatAbs #6

Merged
merged 2 commits into from
Nov 15, 2021
Merged

Temporary fix for generated code function selection, iFloatAbs #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c4cf3fa
Temporary fix for generated code function selection
robdockins Oct 29, 2021
63b269a
Use `iFloatAbs` instead of an explicit "if/then/else"
robdockins Oct 29, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 9 additions & 2 deletions copilot-c99/src/Copilot/Compile/C99/Translate.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,9 +56,16 @@ transexpr (Op3 op e1 e2 e3) = do
transop1 :: Op1 a b -> C.Expr -> C.Expr
transop1 op e = case op of
Not -> (C..!) e
Abs Float -> funcall "fabsf" [e]
Abs Double -> funcall "fabs" [e]
Abs _ -> funcall "abs" [e]
Sign _ -> funcall "copysign" [C.LitDouble 1.0, e]
Recip _ -> C.LitDouble 1.0 C../ e

Sign Double -> funcall "copysign" [C.LitDouble 1.0, e]
Sign Float -> funcall "fcopysign" [C.LitFloat 1.0, e]

Recip Double -> C.LitDouble 1.0 C../ e
Recip Float -> C.LitFloat 1.0 C../ e

Exp _ -> funcall "exp" [e]
Sqrt _ -> funcall "sqrt" [e]
Log _ -> funcall "log" [e]
Expand Down
7 changes: 3 additions & 4 deletions copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -508,10 +508,8 @@ translateOp1 origExpr sym op xe = case (op, xe) of
neg_e <- WI.bvSub sym zero e
WI.bvIte sym e_neg neg_e e
fpAbs :: forall fi . FPOp1 sym fi
fpAbs fiRepr e = do zero <- WFP.iFloatPZero sym fiRepr
e_neg <- WFP.iFloatLt @_ @fi sym e zero
neg_e <- WFP.iFloatSub @_ @fi sym fpRM zero e
WFP.iFloatIte @_ @fi sym e_neg neg_e e
fpAbs _fiRepr e = WFP.iFloatAbs @_ @fi sym e

(CE.Sign _, xe) -> numOp bvSign fpSign xe
where bvSign :: BVOp1 sym w
bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat)
Expand Down Expand Up @@ -676,6 +674,7 @@ translateOp2 origExpr sym op xe1 xe2 = case (op, xe1, xe2) of
(CE.Eq _, xe1, xe2) -> cmp (WI.eqPred sym) (WI.bvEq sym)
(\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatEq @_ @fi sym)
xe1 xe2
-- TODO, I think we can simplify this and pull the `not` outside
(CE.Ne _, xe1, xe2) -> cmp neqPred bvNeq fpNeq xe1 xe2
where neqPred :: BoolCmp2 sym
neqPred e1 e2 = do e <- WI.eqPred sym e1 e2
Expand Down