Comments (2)
Here is a proof-of-concept copilot-c99
patch which causes the example above to generate a trigger function with a pointer argument:
diff --git a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
index 61bb68c..1f6d0b6 100644
--- a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
@@ -74,12 +74,16 @@ mkstep cSettings streams triggers exts =
void = C.TypeSpec C.Void
stmts = map mkexcopy exts
- ++ map mktriggercheck triggers
+ ++ triggerstmts
++ tmpassigns
++ bufferupdates
++ indexupdates
- (declns, tmpassigns, bufferupdates, indexupdates) =
+ declns = streamdeclns
+ ++ concat triggerdeclns
+ (streamdeclns, tmpassigns, bufferupdates, indexupdates) =
unzip4 $ map mkupdateglobals streams
+ (triggerdeclns, triggerstmts) =
+ unzip $ map mktriggercheck triggers
-- Write code to update global stream buffers and index.
mkupdateglobals :: Stream -> (C.Decln, C.Stmt, C.Stmt, C.Stmt)
@@ -122,12 +126,32 @@ mkstep cSettings streams triggers exts =
_ -> C.Ident cpyname C..= C.Ident name
-- Make if-statement to check the guard, call the trigger if necessary.
- mktriggercheck :: Trigger -> C.Stmt
- mktriggercheck (Trigger name guard args) = C.If guard' firetrigger where
- guard' = C.Funcall (C.Ident $ guardname name) []
- firetrigger = [C.Expr $ C.Funcall (C.Ident name) args'] where
- args' = take (length args) (map argcall (argnames name))
- argcall name = C.Funcall (C.Ident name) []
+ mktriggercheck :: Trigger -> ([C.Decln], C.Stmt)
+ mktriggercheck (Trigger name guard args) =
+ (atmpdeclns, ifstmt)
+ where
+ atmpdeclns = zipWith (\tmp_var (UExpr{uExprType = ty}) ->
+ C.VarDecln Nothing (transtype ty) tmp_var Nothing)
+ atempnames args
+
+ atempnames = take (length args) (argtempnames name)
+
+ ifstmt = C.If guard' firetrigger
+
+ guard' = C.Funcall (C.Ident $ guardname name) []
+
+ firetrigger = map C.Expr argassigns ++
+ [C.Expr $ C.Funcall (C.Ident name) (zipWith passarg atempnames args)]
+ where
+ passarg atempname (UExpr{uExprType = ty}) = case ty of
+ Struct _ -> C.UnaryOp C.Ref $ C.Ident atempname
+ _ -> C.Ident atempname
+
+ argassigns = zipWith (\atempname arg ->
+ C.AssignOp C.Assign (C.Ident atempname) arg)
+ atempnames args'
+ args' = take (length args) (map argcall (argnames name))
+ argcall name = C.Funcall (C.Ident name) []
-- Write a call to the memcpy function.
memcpy :: C.Expr -> C.Expr -> C.Expr -> C.Expr
diff --git a/copilot-c99/src/Copilot/Compile/C99/Compile/Internal.hs b/copilot-c99/src/Copilot/Compile/C99/Compile/Internal.hs
index e2e0d6f..d63212d 100644
--- a/copilot-c99/src/Copilot/Compile/C99/Compile/Internal.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/Compile/Internal.hs
@@ -142,7 +142,11 @@ compileh cSettings spec = C.TransUnit declns [] where
extfundecln (Trigger name _ args) = C.FunDecln Nothing cty name params where
cty = C.TypeSpec C.Void
params = map mkparam $ zip (argnames name) args
- mkparam (name, UExpr ty _) = C.Param (transtype ty) name
+ mkparam (name, UExpr ty _) = C.Param (mkparamty ty) name
+
+ mkparamty ty = case ty of
+ Struct _ -> C.Ptr (transtype ty)
+ _ -> transtype ty
-- Declaration for the step function.
stepdecln :: C.Decln
diff --git a/copilot-c99/src/Copilot/Compile/C99/Util.hs b/copilot-c99/src/Copilot/Compile/C99/Util.hs
index ec62ad2..67d6e4d 100644
--- a/copilot-c99/src/Copilot/Compile/C99/Util.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/Util.hs
@@ -55,10 +55,18 @@ guardname name = name ++ "_guard"
argname :: String -> Int -> String
argname name n = name ++ "_arg" ++ show n
+-- | Turn a trigger name into a name for a temporary variable for a trigger argument.
+argtempname :: String -> Int -> String
+argtempname name n = name ++ "_argtemp" ++ show n
+
-- | Enumerate all argument names based on trigger name.
argnames :: String -> [String]
argnames base = [aname | n <- [0..], let aname = argname base n]
+-- | Enumerate all temporary variable names based on trigger name.
+argtempnames :: String -> [String]
+argtempnames base = [atempname | n <- [0..], let atempname = argtempname base n]
+
-- | Define a C expression that calls a function with arguments.
funcall :: C.Ident -> [C.Expr] -> C.Expr
funcall name args = C.Funcall (C.Ident name) args
// structs.h
struct battery;
extern struct battery battery;
void testfun(struct battery * testfun_arg0);
void step(void);
// structs.c
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>
#include "structs.h"
struct battery
{ uint16_t temp;
};
static struct battery battery_cpy;
bool testfun_guard(void) {
return true;
}
struct battery testfun_arg0(void) {
return battery_cpy;
}
void step(void) {
struct battery testfun_argtemp0;
(battery_cpy) = (battery);
if ((testfun_guard)()) {
{(testfun_argtemp0) = ((testfun_arg0)());
(testfun)((&(testfun_argtemp0)));}
};
}
from copilot-verifier.
I agree our job is way simpler if we can change the generated code semantics to pass-by-reference. It would probably be more efficient for large structs too. The values should never be mutated except in the buffer update phase anyway, so that should not cause any semantic problems.
from copilot-verifier.
Related Issues (20)
- Floating-point `signum` operation fails to verify HOT 5
- `FPOps` example fails when verifying `Float`s instead of `Double`s HOT 4
- Allow verification of more programs with partial functions HOT 5
- Produce explanations of why a verified program is correct HOT 1
- Ask Copilot for the names of generated global variables
- Minor soundness issue with trigger functions HOT 1
- Can't verify trigger function using array of structs
- Add CI for `copilot-verifier`
- Display Copilot-related line number information HOT 1
- `LLVMParseError` on LLVM 14.0.0 HOT 3
- Prepare for eventual release to Hackage HOT 1
- Add CI status and Hackage badges to README
- Fix hyperlinks in `copilot-verifier` Hackage page
- Mention ICFP paper in the README
- Log when Crucible simplifies trivial proof goals HOT 1
- Make it clearer which equality-related proof goals happen before and after calling `step()`
- Release 3.19 to Hackage HOT 1
- Support struct updates
- Release 3.20
- Support array updates
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from copilot-verifier.