[patch] 0001-src-minisat-minisat.c-update-types-to-comply-with-al.patch

0001-src-minisat-minisat.c-update-types-to-comply-with-al.patch (text/plain), 2.14 KB, created by Michael Orlitzky on 2022-08-06 01:02:39 UTC

From ddd39fedd2aa2d47599fc4e654c31109d009d02f Mon Sep 17 00:00:00 2001
From: Michael Orlitzky <[e-mail]>
Date: Fri, 5 Aug 2022 20:40:54 -0400
Subject: [PATCH 1/1] src/minisat/minisat.c: update types to comply with
 aliasing rules.

There are two macros in src/minisat/minisat.c that cast a lit* to a
float* and then dereference the result. Since "lit" is typedef'd to
int, this is undefined behavior. In this commit we change a few float*
to lit* to resolve the issue, and then updates the call sites to
accomodate the new types.
---
 src/minisat/minisat.c | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/minisat/minisat.c b/src/minisat/minisat.c
index 2432d65..7ae819d 100644
--- a/src/minisat/minisat.c
+++ b/src/minisat/minisat.c
@@ -136,10 +136,10 @@ struct clause_t
 #define clause_learnt(c) ((c)->size_learnt & 1)
 
 #define clause_activity(c) \
-    (*((float*)&(c)->lits[(c)->size_learnt>>1]))
+    (*((lit*)&(c)->lits[(c)->size_learnt>>1]))
 
 #define clause_setactivity(c, a) \
-    (void)(*((float*)&(c)->lits[(c)->size_learnt>>1]) = (a))
+    (void)(*((lit*)&(c)->lits[(c)->size_learnt>>1]) = (a))
 
 /*====================================================================*/
 /* Encode literals in clause pointers: */
@@ -313,14 +313,14 @@ static inline void act_clause_rescale(solver* s) {
     clause** cs = (clause**)vecp_begin(&s->learnts);
     int i;
     for (i = 0; i < vecp_size(&s->learnts); i++){
-        float a = clause_activity(cs[i]);
+        float a = (float)clause_activity(cs[i]);
         clause_setactivity(cs[i], a * (float)1e-20);
     }
     s->cla_inc *= (float)1e-20;
 }
 
 static inline void act_clause_bump(solver* s, clause *c) {
-    float a = clause_activity(c) + s->cla_inc;
+    float a = (float)clause_activity(c) + s->cla_inc;
     clause_setactivity(c,a);
     if (a > 1e20) act_clause_rescale(s);
 }
@@ -356,7 +356,7 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
         c->lits[i] = begin[i];
 
     if (learnt)
-        *((float*)&c->lits[size]) = 0.0;
+        *((lit*)&c->lits[size]) = 0;
 
     assert(begin[0] >= 0);
     assert(begin[0] < s->size*2);
-- 
2.35.1